harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/CharP/Basic.lean
lemma natCast_eq_natCast' (h : a ≡ b [MOD p]) : (a : R) = b

Proof state:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
⊢ ↑a = ↑b

Tactic:
wlog hle : a ≤ b

Result:
case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [inst_1 : CharP R p] {a b : ℕ}, a ≡ b [MOD p] → a ≤ b → ↑a = ↑b
hle : ¬a ≤ b
⊢ ↑a = ↑b

R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
hle : a ≤ b
⊢ ↑a = ↑b

Proof state:
R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : p ∣ b - a
hle : a ≤ b
⊢ ↑a = ↑b

Tactic:
rw [← Nat.sub_add_cancel hle, Nat.cast_add, (cast_eq_zero_iff R p _).mpr h, zero_add]

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [inst_1 : CharP R p] {a b : ℕ}, a ≡ b [MOD p] → a ≤ b → ↑a = ↑b
hle : ¬a ≤ b
⊢ ↑a = ↑b

Tactic:
exact (this R p h.symm (le_of_not_le hle)).symm

Result:
no goals

Proof state:
R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
hle : a ≤ b
⊢ ↑a = ↑b

Tactic:
rw [Nat.modEq_iff_dvd' hle] at h

Result:
R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : p ∣ b - a
hle : a ≤ b
⊢ ↑a = ↑b
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two (x y : E) :
    re ⟪x, y⟫ = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫_𝕜 = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2

Tactic:
rw [@norm_add_mul_self 𝕜]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2
-- Mathlib/Data/Finset/Dedup.lean
theorem toFinset_surj_on : Set.SurjOn toFinset { l : List α | l.Nodup } Set.univ

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ Set.SurjOn toFinset {l | l.Nodup} Set.univ

Tactic:
rintro ⟨⟨l⟩, hl⟩ _

Result:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
val✝ : Multiset α
l : List α
hl : Multiset.Nodup (Quot.mk (⇑(isSetoid α)) l)
a✝ : { val := Quot.mk (⇑(isSetoid α)) l, nodup := hl } ∈ Set.univ
⊢ { val := Quot.mk (⇑(isSetoid α)) l, nodup := hl } ∈ toFinset '' {l | l.Nodup}

Proof state:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
val✝ : Multiset α
l : List α
hl : Multiset.Nodup (Quot.mk (⇑(isSetoid α)) l)
a✝ : { val := Quot.mk (⇑(isSetoid α)) l, nodup := hl } ∈ Set.univ
⊢ { val := Quot.mk (⇑(isSetoid α)) l, nodup := hl } ∈ toFinset '' {l | l.Nodup}

Tactic:
exact ⟨l, hl, (toFinset_eq hl).symm⟩

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.prime_span_singleton_iff {a : A} : Prime (Ideal.span {a}) ↔ Prime a

Proof state:
case inl
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
⊢ ¬Prime 0 ↔ ¬Prime 0

Tactic:
simp only [not_prime_zero, not_false_eq_true]

Result:
no goals

Proof state:
case inr
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
⊢ Prime (span {a}) ↔ Prime a

Tactic:
have ha' : span {a} ≠ ⊥ := by simpa only [ne_eq, span_singleton_eq_bot] using ha

Result:
case inr
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
ha' : span {a} ≠ ⊥
⊢ Prime (span {a}) ↔ Prime a

Proof state:
case inl
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
⊢ Prime (span {0}) ↔ Prime 0

Tactic:
rw [Set.singleton_zero, span_zero, ← Ideal.zero_eq_bot, ← not_iff_not]

Result:
case inl
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
⊢ ¬Prime 0 ↔ ¬Prime 0

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
⊢ span {a} ≠ ⊥

Tactic:
simpa only [ne_eq, span_singleton_eq_bot] using ha

Result:
no goals

Proof state:
case inr
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
ha' : span {a} ≠ ⊥
⊢ Prime (span {a}) ↔ Prime a

Tactic:
rw [Ideal.prime_iff_isPrime ha', Ideal.span_singleton_prime ha]

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
⊢ Prime (span {a}) ↔ Prime a

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Result:
case inl
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
⊢ Prime (span {0}) ↔ Prime 0

case inr
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
⊢ Prime (span {a}) ↔ Prime a
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem mul_aux_right (x y1 y2 : ℕ × K) (H : R K p y1 y2) :
    mk K p (x.1 + y1.1, (frobenius K p)^[y1.1] x.2 * (frobenius K p)^[x.1] y1.2) =
      mk K p (x.1 + y2.1, (frobenius K p)^[y2.1] x.2 * (frobenius K p)^[x.1] y2.2) :=
  match y1, y2, H with
  | _, _, R.intro n y =>
    Quot.sound <| by
      rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_mul]
      apply R.intro

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 * (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1,
      (⇑(frobenius K p))^[(n + 1, (frobenius K p) y).1] x.2 * (⇑(frobenius K p))^[x.1] (n + 1, (frobenius K p) y).2)

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_mul]

Result:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 * (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1, (frobenius K p) ((⇑(frobenius K p))^[n] x.2 * (⇑(frobenius K p))^[x.1] y))

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 * (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1, (frobenius K p) ((⇑(frobenius K p))^[n] x.2 * (⇑(frobenius K p))^[x.1] y))

Tactic:
apply R.intro

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem Finite.eq_of_subset_of_encard_le (ht : t.Finite) (hst : s ⊆ t) (hts : t.encard ≤ s.encard) :
    s = t

Proof state:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : t.encard ≤ s.encard
⊢ s = t

Tactic:
rw [← zero_add (a := encard s), ← encard_diff_add_encard_of_subset hst] at hts

Result:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
⊢ s = t

Proof state:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
⊢ s = t

Tactic:
have hdiff := WithTop.le_of_add_le_add_right (ht.subset hst).encard_lt_top.ne hts

Result:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : (t \ s).encard ≤ 0
⊢ s = t

Proof state:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : t ⊆ s
⊢ s = t

Tactic:
exact hst.antisymm hdiff

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : (t \ s).encard ≤ 0
⊢ s = t

Tactic:
rw [nonpos_iff_eq_zero, encard_eq_zero, diff_eq_empty] at hdiff

Result:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : t ⊆ s
⊢ s = t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_getDM (o : Option α) (y : γ → m α) (hmono : monotone y) :
    monotone (fun x => o.getDM (y x))

Proof state:
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : (α : Type u) → PartialOrder (m α)
α : Type u
γ : Type w
inst✝ : PartialOrder γ
o : Option α
y : γ → m α
hmono : monotone y
⊢ monotone fun x => o.getDM (y x)

Tactic:
cases o

Result:
case none
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : (α : Type u) → PartialOrder (m α)
α : Type u
γ : Type w
inst✝ : PartialOrder γ
y : γ → m α
hmono : monotone y
⊢ monotone fun x => none.getDM (y x)

case some
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : (α : Type u) → PartialOrder (m α)
α : Type u
γ : Type w
inst✝ : PartialOrder γ
y : γ → m α
hmono : monotone y
val✝ : α
⊢ monotone fun x => (some val✝).getDM (y x)

Proof state:
case some
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : (α : Type u) → PartialOrder (m α)
α : Type u
γ : Type w
inst✝ : PartialOrder γ
y : γ → m α
hmono : monotone y
val✝ : α
⊢ monotone fun x => (some val✝).getDM (y x)

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case none
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : (α : Type u) → PartialOrder (m α)
α : Type u
γ : Type w
inst✝ : PartialOrder γ
y : γ → m α
hmono : monotone y
⊢ monotone fun x => none.getDM (y x)

Tactic:
apply hmono

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma integrable_exp_mul_of_le_of_le {a b : ℝ}
    (ha : Integrable (fun ω ↦ exp (a * X ω)) μ) (hb : Integrable (fun ω ↦ exp (b * X ω)) μ)
    (hat : a ≤ t) (htb : t ≤ b) :
    Integrable (fun ω ↦ exp (t * X ω)) μ

Proof state:
case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : X ω ≤ 0
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

Tactic:
calc exp (t * X ω)
_ ≤ exp (a * X ω) := exp_le_exp.mpr (mul_le_mul_of_nonpos_right hat h)
_ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_right (exp_nonneg _)

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
⊢ rexp (t * X ω) ≤ |rexp (a * X ω) + rexp (b * X ω)|

Tactic:
conv_rhs => rw [abs_of_nonneg (by positivity)]

Result:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : ¬a = 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul ha_zero ha.1.aemeasurable

Result:
no goals

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
⊢ AEMeasurable X μ

Tactic:
by_cases ha_zero : a = 0

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : a = 0
⊢ AEMeasurable X μ

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
ha_zero : ¬a = 0
⊢ AEMeasurable X μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω => rexp (a * X ω)) μ
hb : Integrable (fun ω => rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
⊢ 0 ≤ rexp (a * X ω) + rexp (b * X ω)

Tactic:
positivity

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem mem_map (f : α → β) {a} {s : Computation α} (m : a ∈ s) : f a ∈ map f s

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ (pure ∘ f) a

Tactic:
apply ret_mem

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ s.bind (pure ∘ f)

Tactic:
apply mem_bind m

Result:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ (pure ∘ f) a

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ map f s

Tactic:
rw [← bind_pure]

Result:
α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ s.bind (pure ∘ f)
-- Mathlib/Data/List/Infix.lean
lemma isPrefix_append_of_length (h : l₁.length ≤ l₂.length) : l₁ <+: l₂ ++ l₃ ↔ l₁ <+: l₂ :=
  ⟨fun h ↦ by rw [prefix_iff_eq_take] at *; nth_rw 1 [h, take_eq_left_iff]; tauto,
   fun h ↦ h.trans <| l₂.prefix_append l₃⟩

Proof state:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₃ = [] ∨ l₁.length ≤ l₂.length

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₁ = take l₁.length l₂

Tactic:
nth_rw 1 [h, take_eq_left_iff]

Result:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₃ = [] ∨ l₁.length ≤ l₂.length

Proof state:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ <+: l₂ ++ l₃
⊢ l₁ <+: l₂

Tactic:
rw [prefix_iff_eq_take] at *

Result:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₁ = take l₁.length l₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Lemmas.lean
theorem div_mul_self_eq_mod_sub_self {x k : Nat} : (x / k) * k = x - (x % k)

Proof state:
x k : Nat
this✝ : x % k = x - x / k * k
this : x / k * k ≤ x
⊢ x / k * k = x - x % k

Tactic:
omega

Result:
no goals

Proof state:
x k : Nat
this : x % k = x - x / k * k
⊢ x / k * k = x - x % k

Tactic:
have := div_mul_le_self x k

Result:
x k : Nat
this✝ : x % k = x - x / k * k
this : x / k * k ≤ x
⊢ x / k * k = x - x % k

Proof state:
x k : Nat
⊢ x / k * k = x - x % k

Tactic:
have := mod_eq_sub_div_mul (x := x) (k := k)

Result:
x k : Nat
this : x % k = x - x / k * k
⊢ x / k * k = x - x % k
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
/-- A variant of `eq_inv_mul_iff_mul_eq₀` that moves the nonzero hypothesis to another variable. -/
lemma mul_eq_of_eq_inv_mul₀ (hb : b ≠ 0) (h : b = a⁻¹ * c) : a * b = c

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
b c : G₀
hb : b ≠ 0
h : b = 0⁻¹ * c
⊢ False

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
b c : G₀
hb : b ≠ 0
h : b = 0⁻¹ * c
⊢ False

Tactic:
simp [hb] at h

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a * b = c

Tactic:
rwa [← eq_inv_mul_iff_mul_eq₀]

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a ≠ 0
-- Mathlib/NumberTheory/Bertrand.lean
theorem bertrand_main_inequality {n : ℕ} (n_large : 512 ≤ n) :
    n * (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n

Proof state:
case h₂.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n / 3) ≤ 2 * ↑n / 3

Tactic:
exact cast_div_le.trans (by norm_cast)

Result:
no goals

Proof state:
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n) / ↑3 ≤ 2 * ↑n / 3

Tactic:
norm_cast

Result:
no goals

Proof state:
n : ℕ
n_large : 512 ≤ n
⊢ ↑(n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ ↑(4 ^ n)

Tactic:
simp only [cast_add, cast_one, cast_mul, cast_pow, ← Real.rpow_natCast]

Result:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑4 ^ ↑n

Proof state:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑4 ^ ↑n

Tactic:
refine _root_.trans ?_ (Bertrand.real_main_inequality (by exact_mod_cast n_large))

Result:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑n * (2 * ↑n) ^ √(2 * ↑n) * 4 ^ (2 * ↑n / 3)

Proof state:
case h₁.h.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n).sqrt ≤ √(2 * ↑n)

Tactic:
exact_mod_cast Real.nat_sqrt_le_real_sqrt

Result:
no goals

Proof state:
n : ℕ
n_large : 512 ≤ n
⊢ 0 < 2 * n

Tactic:
positivity

Result:
no goals

Proof state:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
n2_pos : 0 < 2 * n
⊢ 1 ≤ ↑2 * ↑n

Tactic:
exact mod_cast n2_pos

Result:
no goals

Proof state:
n : ℕ
n_large : 512 ≤ n
⊢ 512 ≤ ↑n

Tactic:
exact_mod_cast n_large

Result:
no goals

Proof state:
case h₂.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑4

Tactic:
norm_num1

Result:
no goals

Proof state:
n : ℕ
n_large : 512 ≤ n
⊢ n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n

Tactic:
rw [← @cast_le ℝ]

Result:
n : ℕ
n_large : 512 ≤ n
⊢ ↑(n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ ↑(4 ^ n)

Proof state:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑2 * ↑n

Tactic:
have n2_pos : 0 < 2 * n := by positivity

Result:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
n2_pos : 0 < 2 * n
⊢ 1 ≤ ↑2 * ↑n

Proof state:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑n * (2 * ↑n) ^ √(2 * ↑n) * 4 ^ (2 * ↑n / 3)

Tactic:
gcongr

Result:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑2 * ↑n

case h₁.h.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n).sqrt ≤ √(2 * ↑n)

case h₂.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑4

case h₂.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n / 3) ≤ 2 * ↑n / 3
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_comp_apply (x : N ⊗[R] M) :
    (g.comp f).rTensor M x = (g.rTensor M) ((f.rTensor M) x)

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : N ⊗[R] M
⊢ (⇑(rTensor M g) ∘ ⇑(rTensor M f)) x = (rTensor M g) ((rTensor M f) x)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : N ⊗[R] M
⊢ (rTensor M (g ∘ₗ f)) x = (rTensor M g) ((rTensor M f) x)

Tactic:
rw [rTensor_comp, coe_comp]

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : N ⊗[R] M
⊢ (⇑(rTensor M g) ∘ ⇑(rTensor M f)) x = (rTensor M g) ((rTensor M f) x)
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma pow_sub_of_lt (a : G₀) (h : n < m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ m ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
exact pow_sub₀ _ ha <| Nat.le_of_lt h

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ 0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹

case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Proof state:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ 0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹

Tactic:
rw [zero_pow (Nat.ne_of_gt <| Nat.sub_pos_of_lt h), zero_pow (by omega), zero_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem tail_suffix (l : List α) : tail l <:+ l

Proof state:
α : Type u_1
l : List α
⊢ l.tail <:+ l

Tactic:
rw [← drop_one]

Result:
α : Type u_1
l : List α
⊢ drop 1 l <:+ l

Proof state:
α : Type u_1
l : List α
⊢ drop 1 l <:+ l

Tactic:
apply drop_suffix

Result:
no goals
-- Mathlib/Topology/Algebra/Module/CharacterSpace.lean
theorem union_zero :
    characterSpace 𝕜 A ∪ {0} = {φ : WeakDual 𝕜 A | ∀ x y : A, φ (x * y) = φ x * φ y} :=
  le_antisymm (by
      rintro φ (hφ | rfl)
      · exact hφ.2
      · exact fun _ _ => by exact (zero_mul (0 : 𝕜)).symm)
    fun φ hφ => Or.elim (em <| φ = 0) Or.inr fun h₀ => Or.inl ⟨h₀, hφ⟩

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
x✝¹ x✝ : A
⊢ 0 (x✝¹ * x✝) = 0 x✝¹ * 0 x✝

Tactic:
exact (zero_mul (0 : 𝕜)).symm

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
⊢ characterSpace 𝕜 A ∪ {0} ≤ {φ | ∀ (x y : A), φ (x * y) = φ x * φ y}

Tactic:
rintro φ (hφ | rfl)

Result:
case inl
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ φ ∈ {φ | ∀ (x y : A), φ (x * y) = φ x * φ y}

case inr
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
⊢ 0 ∈ {φ | ∀ (x y : A), φ (x * y) = φ x * φ y}

Proof state:
case inl
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ φ ∈ {φ | ∀ (x y : A), φ (x * y) = φ x * φ y}

Tactic:
exact hφ.2

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
⊢ 0 ∈ {φ | ∀ (x y : A), φ (x * y) = φ x * φ y}

Tactic:
exact fun _ _ => by exact (zero_mul (0 : 𝕜)).symm

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem single_eq_update [DecidableEq α] (a : α) (b : M) :
    ⇑(single a b) = Function.update (0 : _) a b

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
b : M
⊢ ⇑(single a b) = update 0 a b

Tactic:
classical rw [single_eq_set_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
b : M
⊢ ⇑(single a b) = update 0 a b

Tactic:
rw [single_eq_set_indicator, ← Set.piecewise_eq_indicator, Set.piecewise_singleton]

Result:
no goals