no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ (x : ι), x ∈ support v → p x
⊢ ∀ (a : Subtype p) (ha : a ∈ support (subtypeDomain p v)), (fun p_1 x => ↑p_1) a ha ∈ support v
simp
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ (x : ι), x ∈ support v → p x
⊢ ∀ (a : Subtype p) (ha : a ∈ support (subtypeDomain p v)),
    (fun i b => h (↑i) b) a (↑(subtypeDomain p v) a) = h ((fun p_1 x => ↑p_1) a ha) (↑v ((fun p_1 x => ↑p_1) a ha))
simp
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ (x : ι), x ∈ support v → p x
x✝¹ x✝ : Subtype p
a₀ : ι
ha₀ : p a₀
a₁ : ι
ha₁ : p a₁
⊢ ∀ (ha₁_1 : { val := a₀, property := ha₀ } ∈ support (subtypeDomain p v))
    (ha₂ : { val := a₁, property := ha₁ } ∈ support (subtypeDomain p v)),
    (fun p_1 x => ↑p_1) { val := a₀, property := ha₀ } ha₁_1 = (fun p_1 x => ↑p_1) { val := a₁, property := ha₁ } ha₂ →
      { val := a₀, property := ha₀ } = { val := a₁, property := ha₁ }
simp
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ (x : ι), x ∈ support v → p x
i : ι
hi : i ∈ support v
⊢ { val := i, property := (_ : p i) } ∈ support (subtypeDomain p v)
simpa using hi