Theorem: LO.FirstOrder.Arith.Model.Exponential.add_mul (Arithmetization/ISigmaZero/Exponential/Exp.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
wlog hy : y₁ ≥ y₂
State after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {x₁ x₂ y₁ y₂ : M},
    Exponential x₁ y₁ → Exponential x₂ y₂ → y₁ ≥ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
hy : ¬y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
hy : y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
hy : y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
revert y₂
State after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ : M
h₁ : Exponential x₁ y₁
⊢ ∀ {y₂ : M}, Exponential x₂ y₂ → y₁ ≥ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ : M
h₁ : Exponential x₁ y₁
⊢ ∀ {y₂ : M}, Exponential x₂ y₂ → y₁ ≥ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
suffices ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂) by
  intro y₂ h₂ hy; exact this y₂ hy h₂
State after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ : M
h₁ : Exponential x₁ y₁
⊢ ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ : M
h₁ : Exponential x₁ y₁
⊢ ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
induction x₂ using induction_iSigmaZero
State after:
case hP
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
⊢ 𝚺₀-Predicate fun {x₂} => ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)

case zero
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
⊢ ∀ y₂ ≤ y₁, Exponential 0 y₂ → Exponential (x₁ + 0) (y₁ * y₂)

case succ
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
x✝ : M
a✝ : ∀ y₂ ≤ y₁, Exponential x✝ y₂ → Exponential (x₁ + x✝) (y₁ * y₂)
⊢ ∀ y₂ ≤ y₁, Exponential (x✝ + 1) y₂ → Exponential (x₁ + (x✝ + 1)) (y₁ * y₂)

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
⊢ ∀ y₂ ≤ y₁, Exponential 0 y₂ → Exponential (x₁ + 0) (y₁ * y₂)
Tactic:
case zero =>
  intro y₂ _ h₂
  simpa [show y₂ = 1 from h₂.zero_uniq] using h₁
State after:
no goals

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
x₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
⊢ ∀ y₂ ≤ y₁, Exponential (x₂ + 1) y₂ → Exponential (x₁ + (x₂ + 1)) (y₁ * y₂)
Tactic:
case succ x₂ IH =>
  intro y₂ hy h₂
  rcases exponential_succ.mp h₂ with ⟨y₂, rfl, H₂⟩
  have : Exponential (x₁ + x₂) (y₁ * y₂) := IH y₂ (le_trans (by simp) hy) H₂
  simpa [←add_assoc, mul_left_comm y₁ 2 y₂] using this.succ
State after:
no goals

State before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ y₂ : M
h₁ : Exponential x₁ y₁
h₂ : Exponential x₂ y₂
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {x₁ x₂ y₁ y₂ : M},
    Exponential x₁ y₁ → Exponential x₂ y₂ → y₁ ≥ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
hy : ¬y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
simpa [add_comm, mul_comm] using this h₂ h₁ (le_of_not_ge hy)
State after:
no goals

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ : M
h₁ : Exponential x₁ y₁
this : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
⊢ ∀ {y₂ : M}, Exponential x₂ y₂ → y₁ ≥ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
intro y₂ h₂ hy
State after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ : M
h₁ : Exponential x₁ y₁
this : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
h₂ : Exponential x₂ y₂
hy : y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ x₂ y₁ : M
h₁ : Exponential x₁ y₁
this : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
h₂ : Exponential x₂ y₂
hy : y₁ ≥ y₂
⊢ Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
exact this y₂ hy h₂
State after:
no goals

State before:
case hP
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
⊢ 𝚺₀-Predicate fun {x₂} => ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
Tactic:
definability
State after:
no goals

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
⊢ ∀ y₂ ≤ y₁, Exponential 0 y₂ → Exponential (x₁ + 0) (y₁ * y₂)
Tactic:
intro y₂ _ h₂
State after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
y₂ : M
a✝ : y₂ ≤ y₁
h₂ : Exponential 0 y₂
⊢ Exponential (x₁ + 0) (y₁ * y₂)

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
y₂ : M
a✝ : y₂ ≤ y₁
h₂ : Exponential 0 y₂
⊢ Exponential (x₁ + 0) (y₁ * y₂)
Tactic:
simpa [show y₂ = 1 from h₂.zero_uniq] using h₁
State after:
no goals

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
x₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
⊢ ∀ y₂ ≤ y₁, Exponential (x₂ + 1) y₂ → Exponential (x₁ + (x₂ + 1)) (y₁ * y₂)
Tactic:
intro y₂ hy h₂
State after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
x₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
hy : y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) y₂
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * y₂)

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
x₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
hy : y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) y₂
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * y₂)
Tactic:
rcases exponential_succ.mp h₂ with ⟨y₂, rfl, H₂⟩
State after:
case intro.intro
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
x₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
H₂ : Exponential x₂ y₂
hy : 2 * y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) (2 * y₂)
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * (2 * y₂))

State before:
case intro.intro
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
x₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
H₂ : Exponential x₂ y₂
hy : 2 * y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) (2 * y₂)
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * (2 * y₂))
Tactic:
have : Exponential (x₁ + x₂) (y₁ * y₂) := IH y₂ (le_trans (by simp) hy) H₂
State after:
case intro.intro
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
x₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
H₂ : Exponential x₂ y₂
hy : 2 * y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) (2 * y₂)
this : Exponential (x₁ + x₂) (y₁ * y₂)
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * (2 * y₂))

State before:
case intro.intro
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
x₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
H₂ : Exponential x₂ y₂
hy : 2 * y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) (2 * y₂)
this : Exponential (x₁ + x₂) (y₁ * y₂)
⊢ Exponential (x₁ + (x₂ + 1)) (y₁ * (2 * y₂))
Tactic:
simpa [←add_assoc, mul_left_comm y₁ 2 y₂] using this.succ
State after:
no goals

State before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x₁ y₁ : M
h₁ : Exponential x₁ y₁
x₂ : M
IH : ∀ y₂ ≤ y₁, Exponential x₂ y₂ → Exponential (x₁ + x₂) (y₁ * y₂)
y₂ : M
H₂ : Exponential x₂ y₂
hy : 2 * y₂ ≤ y₁
h₂ : Exponential (x₂ + 1) (2 * y₂)
⊢ y₂ ≤ 2 * y₂
Tactic:
simp
State after:
no goals