-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem eq_zero_or_eq_zero_of_mul_eq_zero [NoZeroDivisors R] (φ ψ : R⟦X⟧) (h : φ * ψ = 0) :
    φ = 0 ∨ ψ = 0

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
⊢ φ = 0 ∨ ψ = 0

Tactic:
rw [or_iff_not_imp_left]

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
⊢ ¬φ = 0 → ψ = 0

Proof state:
case h.h.h₁
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
⊢ (coeff R (m, n).1) φ * (coeff R (m, n).2) ψ ≠ 0 → (m, n) ∈ antidiagonal (m + n)

Tactic:
intro

Result:
case h.h.h₁
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
a✝ : (coeff R (m, n).1) φ * (coeff R (m, n).2) ψ ≠ 0
⊢ (m, n) ∈ antidiagonal (m + n)

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
H : ¬φ = 0
⊢ ∃ m, (coeff R m) φ ≠ 0

Tactic:
contrapose! H

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
H : ∀ (m : ℕ), (coeff R m) φ = 0
⊢ φ = 0

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
⊢ ψ = 0

Tactic:
let m := Nat.find ex

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
⊢ ψ = 0

Proof state:
case h.h.h₁
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
a✝ : (coeff R (m, n).1) φ * (coeff R (m, n).2) ψ ≠ 0
⊢ (m, n) ∈ antidiagonal (m + n)

Tactic:
rw [mem_antidiagonal]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j).1 + (i, j).2 = m + n
hne : (i, j) ≠ (m, n)
hi : m ≤ i
hj : n ≤ j
⊢ m < i

Tactic:
contrapose! hne

Result:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j).1 + (i, j).2 = m + n
hi : m ≤ i
hj : n ≤ j
hne : i ≤ m
⊢ (i, j) = (m, n)

Proof state:
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
⊢ (coeff R n) ψ = 0

Tactic:
replace h := congr_arg (coeff R (m + n)) h

Result:
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : (coeff R (m + n)) (φ * ψ) = (coeff R (m + n)) 0
⊢ (coeff R n) ψ = 0

Proof state:
case h.h
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ¬(coeff R (m, n).1) φ = 0 → (coeff R (m, n).2) ψ = 0
⊢ (coeff R n) ψ = 0

Tactic:
exact h hm₁

Result:
no goals

Proof state:
case h.h.h₀.mk
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j) ∈ antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
by_cases hj : j < n

Result:
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j) ∈ antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : j < n
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j) ∈ antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j).1 + (i, j).2 = m + n
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : ¬i < m
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
push_neg at hi hj

Result:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j).1 + (i, j).2 = m + n
hne : (i, j) ≠ (m, n)
hi : m ≤ i
hj : n ≤ j
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Proof state:
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j) ∈ antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : i < m
hm₂ : (coeff R i) φ = 0
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
rw [hm₂, zero_mul]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j) ∈ antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : i < m
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Tactic:
specialize hm₂ _ hi

Result:
case pos
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j) ∈ antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
hj : ¬j < n
hi : i < m
hm₂ : ¬(coeff R i) φ ≠ 0
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0