harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem tendsto_of_antitone {f : ℕ → ℝ≥0} (h_ant : Antitone f) :
    ∃ r : ℝ≥0, Tendsto f atTop (𝓝 r)

Proof state:
case intro
f : ℕ → ℝ≥0
h_ant : Antitone f
h_bdd_0 : 0 ∈ lowerBounds (range fun n => ↑(f n))
L : ℝ
hL : Tendsto (fun n => ↑(f n)) atTop (𝓝 L)
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Tactic:
have hL0 : 0 ≤ L :=
  haveI h_glb : IsGLB (Set.range fun n => (f n : ℝ)) L := isGLB_of_tendsto_atTop h_ant hL
  (le_isGLB_iff h_glb).mpr h_bdd_0

Result:
case intro
f : ℕ → ℝ≥0
h_ant : Antitone f
h_bdd_0 : 0 ∈ lowerBounds (range fun n => ↑(f n))
L : ℝ
hL : Tendsto (fun n => ↑(f n)) atTop (𝓝 L)
hL0 : 0 ≤ L
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Proof state:
f : ℕ → ℝ≥0
h_ant : Antitone f
⊢ 0 ∈ lowerBounds (range fun n => ↑(f n))

Tactic:
rintro r ⟨n, hn⟩

Result:
case intro
f : ℕ → ℝ≥0
h_ant : Antitone f
r : ℝ
n : ℕ
hn : (fun n => ↑(f n)) n = r
⊢ 0 ≤ r

Proof state:
case intro
f : ℕ → ℝ≥0
h_ant : Antitone f
r : ℝ
n : ℕ
hn : (fun n => ↑(f n)) n = r
⊢ 0 ≤ ↑(f n)

Tactic:
exact NNReal.coe_nonneg _

Result:
no goals

Proof state:
f : ℕ → ℝ≥0
h_ant : Antitone f
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Tactic:
have h_bdd_0 : (0 : ℝ) ∈ lowerBounds (Set.range fun n : ℕ => (f n : ℝ)) := by
  rintro r ⟨n, hn⟩
  simp_rw [← hn]
  exact NNReal.coe_nonneg _

Result:
f : ℕ → ℝ≥0
h_ant : Antitone f
h_bdd_0 : 0 ∈ lowerBounds (range fun n => ↑(f n))
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Proof state:
f : ℕ → ℝ≥0
h_ant : Antitone f
h_bdd_0 : 0 ∈ lowerBounds (range fun n => ↑(f n))
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Tactic:
obtain ⟨L, hL⟩ := Real.tendsto_of_bddBelow_antitone ⟨0, h_bdd_0⟩ h_ant

Result:
case intro
f : ℕ → ℝ≥0
h_ant : Antitone f
h_bdd_0 : 0 ∈ lowerBounds (range fun n => ↑(f n))
L : ℝ
hL : Tendsto (fun n => ↑(f n)) atTop (𝓝 L)
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Proof state:
case intro
f : ℕ → ℝ≥0
h_ant : Antitone f
h_bdd_0 : 0 ∈ lowerBounds (range fun n => ↑(f n))
L : ℝ
hL : Tendsto (fun n => ↑(f n)) atTop (𝓝 L)
hL0 : 0 ≤ L
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Tactic:
exact ⟨⟨L, hL0⟩, NNReal.tendsto_coe.mp hL⟩

Result:
no goals

Proof state:
case intro
f : ℕ → ℝ≥0
h_ant : Antitone f
r : ℝ
n : ℕ
hn : (fun n => ↑(f n)) n = r
⊢ 0 ≤ r

Tactic:
simp_rw [← hn]

Result:
case intro
f : ℕ → ℝ≥0
h_ant : Antitone f
r : ℝ
n : ℕ
hn : (fun n => ↑(f n)) n = r
⊢ 0 ≤ ↑(f n)
-- Mathlib/Computability/Tape.lean
theorem ListBlank.ext {Γ} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} :
    (∀ i, L₁.nth i = L₂.nth i) → L₁ = L₂

Proof state:
case inr.inr.H
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1) → l₁.length ≤ l₂.length → mk l₁ = mk l₂
h : ¬l₁.length ≤ l₂.length
h✝ : l₂.length ≤ l₁.length
⊢ ∀ (i_1 : ℕ), (mk l₂).nth i_1 = (mk l₁).nth i_1

Tactic:
intro

Result:
case inr.inr.H
Γ : Type u_1
i : Inhabited Γ
L₁ L₂ : ListBlank Γ
l₁ l₂ : List Γ
H : ∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1
this :
  ∀ {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} (l₁ l₂ : List Γ),
    (∀ (i_1 : ℕ), (mk l₁).nth i_1 = (mk l₂).nth i_1) → l₁.length ≤ l₂.length → mk l₁ = mk l₂
h : ¬l₁.length ≤ l₂.length
h✝ : l₂.length ≤ l₁.length
i✝ : ℕ
⊢ (mk l₂).nth i✝ = (mk l₁).nth i✝
-- Mathlib/Data/Nat/Hyperoperation.lean
theorem hyperoperation_ge_two_eq_self (n m : ℕ) : hyperoperation (n + 2) m 1 = m

Proof state:
case zero
m : ℕ
⊢ hyperoperation (0 + 2) m 1 = m

Tactic:
rw [hyperoperation_two]

Result:
case zero
m : ℕ
⊢ (fun x1 x2 => x1 * x2) m 1 = m

Proof state:
case zero
m : ℕ
⊢ (fun x1 x2 => x1 * x2) m 1 = m

Tactic:
ring

Result:
no goals

Proof state:
case succ
m nn : ℕ
nih : hyperoperation (nn + 2) m 1 = m
⊢ hyperoperation (nn + 1 + 2) m 1 = m

Tactic:
rw [hyperoperation_recursion, hyperoperation_ge_three_eq_one, nih]

Result:
no goals

Proof state:
n m : ℕ
⊢ hyperoperation (n + 2) m 1 = m

Tactic:
induction' n with nn nih

Result:
case zero
m : ℕ
⊢ hyperoperation (0 + 2) m 1 = m

case succ
m nn : ℕ
nih : hyperoperation (nn + 2) m 1 = m
⊢ hyperoperation (nn + 1 + 2) m 1 = m
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
lemma auxbound1 {c : ℝ} (d : ℝ) (hc : 1 ≤ c ^ 2) : r z ≤ ‖c * (z : ℂ) + d‖

Proof state:
case mk
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ r ⟨z, hz⟩ ≤ ‖↑c * ↑⟨z, hz⟩ + ↑d‖

Tactic:
have H1 : z.im ≤ √((c * z.re + d) ^ 2 + (c * z).im ^ 2) := by
  rw [Real.le_sqrt' hz, im_ofReal_mul, mul_pow]
  exact (le_mul_of_one_le_left (sq_nonneg _) hc).trans <| le_add_of_nonneg_left (sq_nonneg _)

Result:
case mk
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
H1 : z.im ≤ √((c * z.re + d) ^ 2 + (↑c * z).im ^ 2)
⊢ r ⟨z, hz⟩ ≤ ‖↑c * ↑⟨z, hz⟩ + ↑d‖

Proof state:
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ z.im ^ 2 ≤ (c * z.re + d) ^ 2 + c ^ 2 * z.im ^ 2

Tactic:
exact (le_mul_of_one_le_left (sq_nonneg _) hc).trans <| le_add_of_nonneg_left (sq_nonneg _)

Result:
no goals

Proof state:
case mk
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
H1 : z.im ≤ √((c * z.re + d) ^ 2 + (↑c * z).im ^ 2)
⊢ r ⟨z, hz⟩ ≤ ‖↑c * ↑⟨z, hz⟩ + ↑d‖

Tactic:
simpa only [r, norm_def, normSq_apply, add_re, re_ofReal_mul, coe_re, ← pow_two, add_im, mul_im,
  coe_im, ofReal_im, zero_mul, add_zero, min_le_iff] using Or.inl H1

Result:
no goals

Proof state:
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ z.im ≤ √((c * z.re + d) ^ 2 + (↑c * z).im ^ 2)

Tactic:
rw [Real.le_sqrt' hz, im_ofReal_mul, mul_pow]

Result:
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ z.im ^ 2 ≤ (c * z.re + d) ^ 2 + c ^ 2 * z.im ^ 2

Proof state:
z : ℍ
c d : ℝ
hc : 1 ≤ c ^ 2
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Tactic:
rcases z with ⟨z, hz⟩

Result:
case mk
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ r ⟨z, hz⟩ ≤ ‖↑c * ↑⟨z, hz⟩ + ↑d‖
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) (h₁ : k ∈ m) (h₂ : (f (m.get? k)).isNone)  :
    (m.alter k f).size = m.size - 1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ m.contains k = true → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size - 1

Tactic:
simp_to_raw using Raw₀.size_alter_eq_sub_one

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
h₁ : k ∈ m
h₂ : (f (m.get? k)).isNone = true
⊢ (m.alter k f).size = m.size - 1

Tactic:
revert h₁ h₂

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ k ∈ m → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size - 1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ k ∈ m → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size - 1

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ m.contains k = true → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size - 1
-- Mathlib/Data/List/Basic.lean
theorem idxOf_eq_length_iff {a : α} {l : List α} : idxOf a l = length l ↔ a ∉ l

Proof state:
case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
h : ¬b = a
⊢ idxOf a l + 1 = l.length + 1 ↔ ¬(a = b ∨ a ∈ l)

Tactic:
simp only [Ne.symm h, false_or]

Result:
case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
h : ¬b = a
⊢ idxOf a l + 1 = l.length + 1 ↔ ¬a ∈ l

Proof state:
case nil
α : Type u
inst✝ : DecidableEq α
a : α
⊢ idxOf a [] = [].length ↔ ¬a ∈ []

Tactic:
exact iff_of_true rfl (not_mem_nil _)

Result:
no goals

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
⊢ idxOf a (b :: l) = (b :: l).length ↔ ¬a ∈ b :: l

Tactic:
simp only [length, mem_cons, idxOf_cons, eq_comm]

Result:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
⊢ (bif b == a then 0 else idxOf a l + 1) = l.length + 1 ↔ ¬(a = b ∨ a ∈ l)

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
⊢ (if (b == a) = true then 0 else idxOf a l + 1) = l.length + 1 ↔ ¬(a = b ∨ a ∈ l)

Tactic:
split_ifs with h <;> simp at h

Result:
case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
h : b = a
⊢ False ↔ ¬(a = b ∨ a ∈ l)

case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
h : ¬b = a
⊢ idxOf a l + 1 = l.length + 1 ↔ ¬(a = b ∨ a ∈ l)

Proof state:
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
h : b = a
⊢ ¬False

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
h : b = a
⊢ False ↔ ¬(a = b ∨ a ∈ l)

Tactic:
exact iff_of_false (by rintro ⟨⟩) fun H => H <| Or.inl h.symm

Result:
no goals

Proof state:
case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
h : ¬b = a
⊢ idxOf a l + 1 = l.length + 1 ↔ idxOf a l = l.length

Tactic:
exact succ_inj'

Result:
no goals

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
⊢ (bif b == a then 0 else idxOf a l + 1) = l.length + 1 ↔ ¬(a = b ∨ a ∈ l)

Tactic:
rw [cond_eq_if]

Result:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
⊢ (if (b == a) = true then 0 else idxOf a l + 1) = l.length + 1 ↔ ¬(a = b ∨ a ∈ l)

Proof state:
case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
h : ¬b = a
⊢ idxOf a l + 1 = l.length + 1 ↔ ¬a ∈ l

Tactic:
rw [← ih]

Result:
case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l = l.length ↔ ¬a ∈ l
h : ¬b = a
⊢ idxOf a l + 1 = l.length + 1 ↔ idxOf a l = l.length
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem supSpanSingleton_apply_mk (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x ∉ f.domain) (x' : E)
    (hx' : x' ∈ f.domain) (c : K) :
    f.supSpanSingleton x y hx
        ⟨x' + c • x, mem_sup.2 ⟨x', hx', _, mem_span_singleton.2 ⟨c, rfl⟩, rfl⟩⟩ =
      f ⟨x', hx'⟩ + c • y

Proof state:
case h
E : Type u_2
inst✝⁴ : AddCommGroup E
F : Type u_3
inst✝³ : AddCommGroup F
K : Type u_5
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ c • x ∈ (mkSpanSingleton' x y ⋯).domain

Tactic:
exact mem_span_singleton.2 ⟨c, rfl⟩

Result:
no goals

Proof state:
case hz
E : Type u_2
inst✝⁴ : AddCommGroup E
F : Type u_3
inst✝³ : AddCommGroup F
K : Type u_5
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑⟨x', hx'⟩ + ↑⟨c • x, ⋯⟩ = ↑⟨x' + c • x, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_2
inst✝⁴ : AddCommGroup E
F : Type u_3
inst✝³ : AddCommGroup F
K : Type u_5
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑(f.supSpanSingleton x y hx) ⟨x' + c • x, ⋯⟩ = ↑f ⟨x', hx'⟩ + c • y

Tactic:
erw [sup_apply _ ⟨x', hx'⟩ ⟨c • x, _⟩, mkSpanSingleton'_apply]

Result:
case h
E : Type u_2
inst✝⁴ : AddCommGroup E
F : Type u_3
inst✝³ : AddCommGroup F
K : Type u_5
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ c • x ∈ (mkSpanSingleton' x y ⋯).domain

case hz
E : Type u_2
inst✝⁴ : AddCommGroup E
F : Type u_3
inst✝³ : AddCommGroup F
K : Type u_5
inst✝² : DivisionRing K
inst✝¹ : Module K E
inst✝ : Module K F
f : E →ₗ.[K] F
x : E
y : F
hx : x ∉ f.domain
x' : E
hx' : x' ∈ f.domain
c : K
⊢ ↑⟨x', hx'⟩ + ↑⟨c • x, ?h⟩ = ↑⟨x' + c • x, ⋯⟩
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem ofFinsupp_pow (a) (n : ℕ) : (⟨a ^ n⟩ : R[X]) = ⟨a⟩ ^ n

Proof state:
case succ
R : Type u
inst✝ : Semiring R
a : R[ℕ]
n : ℕ
n_ih : { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := a ^ (n + 1) } = npowRec (n + 1) { toFinsupp := a }

Tactic:
simp [npowRec, n_ih, pow_succ]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
a : R[ℕ]
n : ℕ
⊢ { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }

Tactic:
induction n with
| zero        => simp [npowRec]
| succ n n_ih => simp [npowRec, n_ih, pow_succ]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ { toFinsupp := a ^ 0 } = npowRec 0 { toFinsupp := a }

Tactic:
simp [npowRec]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
a : R[ℕ]
n : ℕ
⊢ { toFinsupp := a ^ n } = { toFinsupp := a } ^ n

Tactic:
change _ = npowRec n _

Result:
R : Type u
inst✝ : Semiring R
a : R[ℕ]
n : ℕ
⊢ { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
-- Mathlib/Topology/Sober.lean
theorem disjoint_iff (h : IsGenericPoint x S) (hU : IsOpen U) : Disjoint S U ↔ x ∉ U

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S U : Set α
h : IsGenericPoint x S
hU : IsOpen U
⊢ Disjoint S U ↔ x ∉ U

Tactic:
rw [h.mem_open_set_iff hU, ← not_disjoint_iff_nonempty_inter, Classical.not_not]

Result:
no goals
-- Mathlib/Topology/Order/Compact.lean
lemma CompactIccSpace.mk' [TopologicalSpace α] [Preorder α]
    (h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)) : CompactIccSpace α where
  isCompact_Icc {a b}

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact ∅

Tactic:
exact isCompact_empty

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact (Icc a b)

Tactic:
rw [Icc_eq_empty hab]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact ∅
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem haarContent_self {K₀ : PositiveCompacts G} : haarContent K₀ K₀.toCompacts = 1

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ ⟨1, ⋯⟩ = 1

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ (haarContent K₀) K₀.toCompacts = 1

Tactic:
simp_rw [← ENNReal.coe_one, haarContent_apply, ENNReal.coe_inj, chaar_self]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ ⟨1, ⋯⟩ = 1
-- Mathlib/Topology/Order.lean
theorem denseRange_discrete {ι : Type*} {f : ι → α} : DenseRange f ↔ Surjective f

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ι : Type u_3
f : ι → α
⊢ DenseRange f ↔ Surjective f

Tactic:
rw [DenseRange, dense_discrete, range_eq_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem smul_tmul_smul (r s : R) (m : M) (n : N) : (r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
r s : R
m : M
n : N
⊢ (r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n

Tactic:
simp_rw [smul_tmul, tmul_smul, mul_smul]

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem diag_mem_sym2_mem_iff : (∀ b, b ∈ Sym2.diag a → b ∈ s) ↔ a ∈ s

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ (∀ b ∈ Sym2.diag a, b ∈ s) ↔ a ∈ s

Tactic:
rw [← mem_sym2_iff]

Result:
α : Type u_1
s : Finset α
a : α
⊢ Sym2.diag a ∈ s.sym2 ↔ a ∈ s

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ Sym2.diag a ∈ s.sym2 ↔ a ∈ s

Tactic:
exact mk_mem_sym2_iff.trans <| and_self_iff

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem eq_mul_inverse_iff_mul_eq (x y z : M₀) (h : IsUnit z) : x = y * inverse z ↔ x * z = y :=
  ⟨fun h1 => by rw [h1, inverse_mul_cancel_right _ _ h],
  fun h1 => by rw [← h1, mul_inverse_cancel_right _ _ h]⟩

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x * z = y
⊢ x = y * inverse z

Tactic:
rw [← h1, mul_inverse_cancel_right _ _ h]

Result:
no goals

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x = y * inverse z
⊢ x * z = y

Tactic:
rw [h1, inverse_mul_cancel_right _ _ h]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem exists_blsub_cof (o : Ordinal) :
    ∃ f : ∀ a < (cof o).ord, Ordinal, blsub.{u, u} _ f = o

Proof state:
o : Ordinal.{u}
⊢ ∃ f, o.cof.ord.blsub f = o

Tactic:
rcases exists_lsub_cof o with ⟨ι, f, hf, hι⟩

Result:
case intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
⊢ ∃ f, o.cof.ord.blsub f = o

Proof state:
case intro.intro.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, o.cof.ord.blsub f = o

Tactic:
rw [← hι, hι']

Result:
case intro.intro.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, (type r).blsub f = o

Proof state:
case intro.intro.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, (type r).blsub f = o

Tactic:
exact ⟨_, hf⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : (#ι).ord = type r
⊢ ∃ f, o.cof.ord.blsub f = o

Tactic:
rw [← @blsub_eq_lsub' ι r hr] at hf

Result:
case intro.intro.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ f, o.cof.ord.blsub f = o

Proof state:
case intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
⊢ ∃ f, o.cof.ord.blsub f = o

Tactic:
rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩

Result:
case intro.intro.intro.intro.intro
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : (#ι).ord = type r
⊢ ∃ f, o.cof.ord.blsub f = o
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
private lemma toAffine_addX_of_eq {P : Fin 3 → F} (hPz : P z ≠ 0) {n d : F} (hd : d ≠ 0) :
    W.toAffine.addX (P x / P z ^ 2) (P x / P z ^ 2) (-n / (P z * d)) =
      (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) / (P z * d) ^ 2

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (((n ^ 2 * (P z * d) + -((toAffine W).a₁ * n * (P z * d) ^ 2) - (P z * d) ^ 2 * (P z * d) * (toAffine W).a₂) *
              P z ^ 2 -
            (P z * d) ^ 2 * (P z * d) * P x) *
          P z ^ 2 -
        (P z * d) ^ 2 * (P z * d) * P z ^ 2 * P x) *
      (P z * d) ^ 2 =
    (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) *
      ((P z * d) ^ 2 * (P z * d) * P z ^ 2 * P z ^ 2)

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (toAffine W).addX (P x / P z ^ 2) (P x / P z ^ 2) (-n / (P z * d)) =
    (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) / (P z * d) ^ 2

Tactic:
field_simp [mul_ne_zero hPz hd]

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (((n ^ 2 * (P z * d) + -((toAffine W).a₁ * n * (P z * d) ^ 2) - (P z * d) ^ 2 * (P z * d) * (toAffine W).a₂) *
              P z ^ 2 -
            (P z * d) ^ 2 * (P z * d) * P x) *
          P z ^ 2 -
        (P z * d) ^ 2 * (P z * d) * P z ^ 2 * P x) *
      (P z * d) ^ 2 =
    (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) *
      ((P z * d) ^ 2 * (P z * d) * P z ^ 2 * P z ^ 2)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem gcd_dvd (xs : IntList) {a : Int} (m : a ∈ xs) : (xs.gcd : Int) ∣ a

Proof state:
case tail
xs : IntList
a b : Int
as✝ : List Int
m : List.Mem a as✝
ih : gcd as✝ ∣ a.natAbs
⊢ gcd (b :: as✝) ∣ a.natAbs

Tactic:
simp only [gcd_cons]

Result:
case tail
xs : IntList
a b : Int
as✝ : List Int
m : List.Mem a as✝
ih : gcd as✝ ∣ a.natAbs
⊢ b.natAbs.gcd (gcd as✝) ∣ a.natAbs

Proof state:
case head
xs : IntList
a : Int
as✝ : List Int
⊢ a.natAbs.gcd (gcd as✝) ∣ a.natAbs

Tactic:
apply Nat.gcd_dvd_left

Result:
no goals

Proof state:
case head
xs : IntList
a : Int
as✝ : List Int
⊢ gcd (a :: as✝) ∣ a.natAbs

Tactic:
simp only [gcd_cons]

Result:
case head
xs : IntList
a : Int
as✝ : List Int
⊢ a.natAbs.gcd (gcd as✝) ∣ a.natAbs

Proof state:
xs : IntList
a : Int
m : a ∈ xs
⊢ ↑xs.gcd ∣ a

Tactic:
rw [Int.ofNat_dvd_left]

Result:
xs : IntList
a : Int
m : a ∈ xs
⊢ xs.gcd ∣ a.natAbs

Proof state:
xs : IntList
a : Int
m : a ∈ xs
⊢ xs.gcd ∣ a.natAbs

Tactic:
induction m with
| head =>
  simp only [gcd_cons]
  apply Nat.gcd_dvd_left
| tail b m ih =>   simp only [gcd_cons]
  exact Nat.dvd_trans (Nat.gcd_dvd_right _ _) ih

Result:
no goals

Proof state:
case tail
xs : IntList
a b : Int
as✝ : List Int
m : List.Mem a as✝
ih : gcd as✝ ∣ a.natAbs
⊢ b.natAbs.gcd (gcd as✝) ∣ a.natAbs

Tactic:
exact Nat.dvd_trans (Nat.gcd_dvd_right _ _) ih

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem exists_coprime (m n : Nat) :
    ∃ m' n', Coprime m' n' ∧ m = m' * gcd m n ∧ n = n' * gcd m n

Proof state:
case inl
m n : Nat
h0 : m.gcd n = 0
⊢ ∃ m' n', m'.Coprime n' ∧ m = m' * m.gcd n ∧ n = n' * m.gcd n

Tactic:
rw [gcd_eq_zero_iff] at h0

Result:
case inl
m n : Nat
h0 : m = 0 ∧ n = 0
⊢ ∃ m' n', m'.Coprime n' ∧ m = m' * m.gcd n ∧ n = n' * m.gcd n

Proof state:
m n : Nat
⊢ ∃ m' n', m'.Coprime n' ∧ m = m' * m.gcd n ∧ n = n' * m.gcd n

Tactic:
cases eq_zero_or_pos (gcd m n) with
| inl h0 =>
  rw [gcd_eq_zero_iff] at h0
  refine ⟨1, 1, gcd_one_left 1, ?_⟩
  simp [h0]
| inr hpos =>
  exact ⟨_, _, coprime_div_gcd_div_gcd hpos,
    (Nat.div_mul_cancel (gcd_dvd_left m n)).symm,
    (Nat.div_mul_cancel (gcd_dvd_right m n)).symm⟩

Result:
no goals

Proof state:
case inl
m n : Nat
h0 : m = 0 ∧ n = 0
⊢ m = 1 * m.gcd n ∧ n = 1 * m.gcd n

Tactic:
simp [h0]

Result:
no goals

Proof state:
case inl
m n : Nat
h0 : m = 0 ∧ n = 0
⊢ ∃ m' n', m'.Coprime n' ∧ m = m' * m.gcd n ∧ n = n' * m.gcd n

Tactic:
refine ⟨1, 1, gcd_one_left 1, ?_⟩

Result:
case inl
m n : Nat
h0 : m = 0 ∧ n = 0
⊢ m = 1 * m.gcd n ∧ n = 1 * m.gcd n

Proof state:
case inr
m n : Nat
hpos : m.gcd n > 0
⊢ ∃ m' n', m'.Coprime n' ∧ m = m' * m.gcd n ∧ n = n' * m.gcd n

Tactic:
exact ⟨_, _, coprime_div_gcd_div_gcd hpos,
  (Nat.div_mul_cancel (gcd_dvd_left m n)).symm,
  (Nat.div_mul_cancel (gcd_dvd_right m n)).symm⟩

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem map_mul_left_nhds_one (x : G) : map (x * ·) (𝓝 1) = 𝓝 x

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
⊢ map (fun x_1 => x * x_1) (𝓝 1) = 𝓝 x

Tactic:
simp

Result:
no goals