Theorem: Finsupp.mul_single_eq_zero (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ single i₁ x * single i₂ y = 0
Tactic:
classical
rw [Finsupp.mul_eq_zero_of_disjoint_support]
simp_rw [Finset.disjoint_iff_ne, Finsupp.mem_support_single]
simp_rw [and_imp, forall_eq]
intros
exact hi
State after:
no goals

State before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ single i₁ x * single i₂ y = 0
Tactic:
rw [Finsupp.mul_eq_zero_of_disjoint_support]
State after:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ Disjoint (single i₁ x).support (single i₂ y).support

State before:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ Disjoint (single i₁ x).support (single i₂ y).support
Tactic:
simp_rw [Finset.disjoint_iff_ne, Finsupp.mem_support_single]
State after:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ ∀ (a : ι), a = i₁ ∧ x ≠ 0 → ∀ (b : ι), b = i₂ ∧ y ≠ 0 → a ≠ b

State before:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ ∀ (a : ι), a = i₁ ∧ x ≠ 0 → ∀ (b : ι), b = i₂ ∧ y ≠ 0 → a ≠ b
Tactic:
simp_rw [and_imp, forall_eq]
State after:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ x ≠ 0 → y ≠ 0 → i₁ ≠ i₂

State before:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
⊢ x ≠ 0 → y ≠ 0 → i₁ ≠ i₂
Tactic:
intros
State after:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
a✝¹ : x ≠ 0
a✝ : y ≠ 0
⊢ i₁ ≠ i₂

State before:
case h
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
β : Type u_2
inst✝ : MulZeroClass β
i₁ i₂ : ι
hi : i₁ ≠ i₂
x y : β
a✝¹ : x ≠ 0
a✝ : y ≠ 0
⊢ i₁ ≠ i₂
Tactic:
exact hi
State after:
no goals