Theorem: LO.FirstOrder.Arith.Model.bexp_graph (Arithmetization/ISigmaZero/Exponential/Log.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
⊢ y = bexp a x → ∃ l ≤ a, l = ‖a‖ ∧ (x < l → Exponential x y) ∧ (l ≤ x → y = 0)
Tactic:
rintro rfl
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
⊢ ∃ l ≤ a, l = ‖a‖ ∧ (x < l → Exponential x (bexp a x)) ∧ (l ≤ x → bexp a x = 0)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
⊢ ∃ l ≤ a, l = ‖a‖ ∧ (x < l → Exponential x (bexp a x)) ∧ (l ≤ x → bexp a x = 0)
Tactic:
exact ⟨‖a‖, by simp, rfl, exp_bexp_of_lt, bexp_eq_zero_of_le⟩
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 ⊧ₘ* 𝐈𝚫₀
a x : M
⊢ ‖a‖ ≤ a
Tactic:
simp
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 ⊧ₘ* 𝐈𝚫₀
y a x : M
⊢ (∃ l ≤ a, l = ‖a‖ ∧ (x < l → Exponential x y) ∧ (l ≤ x → y = 0)) → y = bexp a x
Tactic:
rintro ⟨_, _, rfl, hlt, hle⟩
State after:
case intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
⊢ y = bexp a x

State before:
case intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
⊢ y = bexp a x
Tactic:
rcases show x < ‖a‖ ∨ ‖a‖ ≤ x from lt_or_ge _ _ with (lt | le)
State after:
case intro.intro.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
lt : x < ‖a‖
⊢ y = bexp a x

case intro.intro.intro.intro.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
le : ‖a‖ ≤ x
⊢ y = bexp a x

State before:
case intro.intro.intro.intro.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
lt : x < ‖a‖
⊢ y = bexp a x
Tactic:
exact (hlt lt).uniq (exp_bexp_of_lt lt)
State after:
no goals

State before:
case intro.intro.intro.intro.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y a x : M
left✝ : ‖a‖ ≤ a
hlt : x < ‖a‖ → Exponential x y
hle : ‖a‖ ≤ x → y = 0
le : ‖a‖ ≤ x
⊢ y = bexp a x
Tactic:
rcases hle le
State after:
case intro.intro.intro.intro.inr.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
left✝ : ‖a‖ ≤ a
le : ‖a‖ ≤ x
hlt : x < ‖a‖ → Exponential x 0
hle : ‖a‖ ≤ x → 0 = 0
⊢ 0 = bexp a x

State before:
case intro.intro.intro.intro.inr.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a x : M
left✝ : ‖a‖ ≤ a
le : ‖a‖ ≤ x
hlt : x < ‖a‖ → Exponential x 0
hle : ‖a‖ ≤ x → 0 = 0
⊢ 0 = bexp a x
Tactic:
simp [bexp_eq_zero_of_le le]
State after:
no goals