Theorem: PolynomialMap.zero_pow_add_zero_pow (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
⊢ 0 ^ a + 0 ^ b = 1
Tactic:
suffices (a = 1 ∧ b = 0) ∨ (a = 0 ∧ b = 1) by
  cases this with
  | inl h => rw [h.1, h.2, pow_one, pow_zero, zero_add]
  | inr h => rw [h.1, h.2, pow_one, pow_zero, add_zero]
State after:
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1

State before:
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
Tactic:
by_cases ha : a = 0
State after:
case pos
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha : a = 0
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1

case neg
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha : ¬a = 0
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1

State before:
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
this : a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
⊢ 0 ^ a + 0 ^ b = 1
Tactic:
cases this with
| inl h => rw [h.1, h.2, pow_one, pow_zero, zero_add]
| inr h => rw [h.1, h.2, pow_one, pow_zero, add_zero]
State after:
no goals

State before:
case inl
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h✝ : a + b = 1
h : a = 1 ∧ b = 0
⊢ 0 ^ a + 0 ^ b = 1
Tactic:
rw [h.1, h.2, pow_one, pow_zero, zero_add]
State after:
no goals

State before:
case inr
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h✝ : a + b = 1
h : a = 0 ∧ b = 1
⊢ 0 ^ a + 0 ^ b = 1
Tactic:
rw [h.1, h.2, pow_one, pow_zero, add_zero]
State after:
no goals

State before:
case pos
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha : a = 0
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
Tactic:
exact Or.inr ⟨ha, by simpa [ha, zero_add] using h⟩
State after:
no goals

State before:
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha : a = 0
⊢ b = 1
Tactic:
simpa [ha, zero_add] using h
State after:
no goals

State before:
case neg
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha : ¬a = 0
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
Tactic:
have ha : a = 1 := le_antisymm (h ▸  Nat.le_add_right a b) (Nat.pos_of_ne_zero ha)
State after:
case neg
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha✝ : ¬a = 0
ha : a = 1
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1

State before:
case neg
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha✝ : ¬a = 0
ha : a = 1
⊢ a = 1 ∧ b = 0 ∨ a = 0 ∧ b = 1
Tactic:
exact Or.inl ⟨ha, by simpa [ha, add_right_eq_self] using h⟩
State after:
no goals

State before:
R✝ : Type u
inst✝⁹ : CommRing R✝
M✝ : Type u_1
N✝ : Type u_2
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : AddCommGroup N✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : Module R✝ N✝
R : Type u
inst✝⁴ : CommRing R
M : Type ?u.366545
N : Type ?u.366548
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
a b : ℕ
h : a + b = 1
ha✝ : ¬a = 0
ha : a = 1
⊢ b = 0
Tactic:
simpa [ha, add_right_eq_self] using h
State after:
no goals