Theorem: PowerSeries.ne_zero_of_mul_ne_zero (DividedPowers/ExponentialModule/Basic.lean)

State before:
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0
Tactic:
constructor
State after:
case left
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
⊢ a ≠ 0

case right
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
⊢ b ≠ 0

State before:
case left
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
⊢ a ≠ 0
Tactic:
intro ha
State after:
case left
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
ha : a = 0
⊢ False

State before:
case left
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
ha : a = 0
⊢ False
Tactic:
apply h
State after:
case left
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
ha : a = 0
⊢ a * b = 0

State before:
case left
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
ha : a = 0
⊢ a * b = 0
Tactic:
rw [ha, zero_mul]
State after:
no goals

State before:
case right
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
⊢ b ≠ 0
Tactic:
intro hb
State after:
case right
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
hb : b = 0
⊢ False

State before:
case right
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
hb : b = 0
⊢ False
Tactic:
apply h
State after:
case right
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
hb : b = 0
⊢ a * b = 0

State before:
case right
A : Type u_1
inst✝⁵ : CommRing A
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra A R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra A S
M : Type u_4
inst✝ : MonoidWithZero M
a b : M
h : a * b ≠ 0
hb : b = 0
⊢ a * b = 0
Tactic:
rw [hb, mul_zero]
State after:
no goals