harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem fin_two_exists_eq_mk_of_apply_zero_one_eq_zero {R : Type*} [Field R] (g : SL(2, R))
    (hg : g 1 0 = 0) :
    ∃ (a b : R) (h : a ≠ 0), g = (⟨!![a, b; 0, a⁻¹], by simp [h]⟩ : SL(2, R))

Proof state:
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 = 0
⊢ c = 0

Tactic:
simpa using hg

Result:
no goals

Proof state:
case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ∃ a_1 b_1, ∃ (h : a_1 ≠ 0), ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a_1, b_1; 0, a_1⁻¹], ⋯⟩

Tactic:
refine ⟨a, b, left_ne_zero_of_mul_eq_one had, ?_⟩

Result:
case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a, b; 0, a⁻¹], ⋯⟩

Proof state:
case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 = 0
⊢ ∃ a_1 b_1, ∃ (h : a_1 ≠ 0), ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a_1, b_1; 0, a_1⁻¹], ⋯⟩

Tactic:
replace hg : c = 0 := by simpa using hg

Result:
case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ ∃ a_1 b_1, ∃ (h : a_1 ≠ 0), ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a_1, b_1; 0, a_1⁻¹], ⋯⟩

Proof state:
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg : ↑g 1 0 = 0
a b : R
h : a ≠ 0
⊢ !![a, b; 0, a⁻¹].det = 1

Tactic:
simp [h]

Result:
no goals

Proof state:
case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a, b; 0, a⁻¹], ⋯⟩

Tactic:
simp_rw [eq_inv_of_mul_eq_one_right had, hg]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ a * d = 1

Tactic:
rwa [hg, mul_zero, sub_zero] at h_det

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg : ↑g 1 0 = 0
⊢ ∃ a b, ∃ (h : a ≠ 0), g = ⟨!![a, b; 0, a⁻¹], ⋯⟩

Tactic:
induction g using Matrix.SpecialLinearGroup.fin_two_induction with | h a b c d h_det =>
replace hg : c = 0 := by simpa using hg
have had : a * d = 1 := by rwa [hg, mul_zero, sub_zero] at h_det
refine ⟨a, b, left_ne_zero_of_mul_eq_one had, ?_⟩
simp_rw [eq_inv_of_mul_eq_one_right had, hg]

Result:
no goals

Proof state:
case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ ∃ a_1 b_1, ∃ (h : a_1 ≠ 0), ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a_1, b_1; 0, a_1⁻¹], ⋯⟩

Tactic:
have had : a * d = 1 := by rwa [hg, mul_zero, sub_zero] at h_det

Result:
case h
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
had : a * d = 1
⊢ ∃ a_1 b_1, ∃ (h : a_1 ≠ 0), ⟨!![a, b; c, d], ⋯⟩ = ⟨!![a_1, b_1; 0, a_1⁻¹], ⋯⟩
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prodComparison_comp :
    prodComparison (F ⋙ G) A B =
      G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd) =
    G.map (prod.lift (F.map prod.fst) (F.map prod.snd)) ≫ prod.lift (G.map prod.fst) (G.map prod.snd)

Tactic:
ext <;> simp <;> rw [← G.map_comp] <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B)

Tactic:
unfold prodComparison

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd) =
    G.map (prod.lift (F.map prod.fst) (F.map prod.snd)) ≫ prod.lift (G.map prod.fst) (G.map prod.snd)
-- Mathlib/Data/Quot.lean
@[simp]
lemma Equivalence.quot_mk_eq_iff {α : Type*} {r : α → α → Prop} (h : Equivalence r) (x y : α) :
    Quot.mk r x = Quot.mk r y ↔ r x y

Proof state:
case mp.trans
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y x✝ y✝ z✝ : α
a✝¹ : Relation.EqvGen r x✝ y✝
a✝ : Relation.EqvGen r y✝ z✝
h₁₂ : r x✝ y✝
h₂₃ : r y✝ z✝
⊢ r x✝ z✝

Tactic:
exact h.trans h₁₂ h₂₃

Result:
no goals

Proof state:
case mp.symm
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y x✝ y✝ : α
a✝ : Relation.EqvGen r x✝ y✝
H : r x✝ y✝
⊢ r y✝ x✝

Tactic:
exact h.symm H

Result:
no goals

Proof state:
case mp
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y : α
⊢ Relation.EqvGen r x y → r x y

Tactic:
intro hxy

Result:
case mp
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y : α
hxy : Relation.EqvGen r x y
⊢ r x y

Proof state:
case mp
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y : α
hxy : Relation.EqvGen r x y
⊢ r x y

Tactic:
induction hxy with
| rel _ _ H => exact H
| refl _ => exact h.refl _
| symm _ _ _ H => exact h.symm H
| trans _ _ _ _ _ h₁₂ h₂₃ => exact h.trans h₁₂ h₂₃

Result:
no goals

Proof state:
case mp
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y : α
⊢ Quot.mk r x = Quot.mk r y → r x y

Tactic:
rw [Quot.eq]

Result:
case mp
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y : α
⊢ Relation.EqvGen r x y → r x y

Proof state:
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y : α
⊢ Quot.mk r x = Quot.mk r y ↔ r x y

Tactic:
constructor

Result:
case mp
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y : α
⊢ Quot.mk r x = Quot.mk r y → r x y

case mpr
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y : α
⊢ r x y → Quot.mk r x = Quot.mk r y

Proof state:
case mp.rel
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y x✝ y✝ : α
H : r x✝ y✝
⊢ r x✝ y✝

Tactic:
exact H

Result:
no goals

Proof state:
case mp.refl
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y x✝ : α
⊢ r x✝ x✝

Tactic:
exact h.refl _

Result:
no goals

Proof state:
case mpr
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y : α
⊢ r x y → Quot.mk r x = Quot.mk r y

Tactic:
exact Quot.sound

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_nonpos_of_nonneg_of_nonpos (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b⁻¹ ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a / b ≤ 0

Tactic:
rw [div_eq_mul_inv]

Result:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b⁻¹ ≤ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem exists_bool' {p : Bool → Prop} (b : Bool) : (∃ x, p x) ↔ p b ∨ p !b :=
  ⟨fun ⟨x, hx⟩ ↦ by cases x <;> cases b <;> first | exact .inl ‹_› | exact .inr ‹_›,
    fun h ↦ by cases h <;> exact ⟨_, ‹_›⟩⟩

Proof state:
case true.true
p : Bool → Prop
x✝ : ∃ x, p x
hx : p true
⊢ p true ∨ p !true

Tactic:
exact .inl ‹_›

Result:
no goals

Proof state:
p : Bool → Prop
b : Bool
h : p b ∨ p !b
⊢ ∃ x, p x

Tactic:
cases h <;> exact ⟨_, ‹_›⟩

Result:
no goals

Proof state:
p : Bool → Prop
b : Bool
x✝ : ∃ x, p x
x : Bool
hx : p x
⊢ p b ∨ p !b

Tactic:
cases x <;> cases b <;> first | exact .inl ‹_› | exact .inr ‹_›

Result:
no goals

Proof state:
case true.false
p : Bool → Prop
x✝ : ∃ x, p x
hx : p true
⊢ p false ∨ p !false

Tactic:
exact .inr ‹_›

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem isReal_of_mk_isReal {φ : K →+* ℂ} (h : IsReal (mk φ)) :
    ComplexEmbedding.IsReal φ

Proof state:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ (mk φ).IsComplex

Tactic:
exact ⟨φ, h, rfl⟩

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
h : (mk φ).IsReal
⊢ ComplexEmbedding.IsReal φ

Tactic:
contrapose! h

Result:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ ¬(mk φ).IsReal

Proof state:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ ¬(mk φ).IsReal

Tactic:
rw [not_isReal_iff_isComplex]

Result:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ (mk φ).IsComplex
-- Mathlib/Algebra/Module/Submodule/LinearMap.lean
theorem subtype_comp_inclusion (p q : Submodule R M) (h : p ≤ q) :
    q.subtype.comp (inclusion h) = p.subtype

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ q.subtype ∘ₗ inclusion h = p.subtype

Tactic:
ext ⟨b, hb⟩

Result:
case h.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
b : M
hb : b ∈ p
⊢ (q.subtype ∘ₗ inclusion h) ⟨b, hb⟩ = p.subtype ⟨b, hb⟩

Proof state:
case h.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
b : M
hb : b ∈ p
⊢ (q.subtype ∘ₗ inclusion h) ⟨b, hb⟩ = p.subtype ⟨b, hb⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem hasDerivAt_mulExpNegMulSq (y : ℝ) :
    HasDerivAt (mulExpNegMulSq ε)
    (exp (- (ε * y * y)) + y * (exp (- (ε * y * y)) * (-2 * ε * y))) y

Proof state:
ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y

Tactic:
nth_rw 1 [← one_mul (exp (- (ε * y * y)))]

Result:
ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (1 * rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y

Proof state:
ε y : ℝ
⊢ HasDerivAt (fun y => rexp (-(ε * y * y))) (rexp (-(ε * y * y)) * (-2 * ε * y)) y

Tactic:
apply HasDerivAt.exp (HasDerivAt.congr_deriv (HasDerivAt.neg
  (HasDerivAt.mul (HasDerivAt.const_mul ε (hasDerivAt_id' y)) (hasDerivAt_id' y))) (by ring))

Result:
no goals

Proof state:
ε y : ℝ
⊢ -(ε * 1 * y + ε * y * 1) = -2 * ε * y

Tactic:
ring

Result:
no goals

Proof state:
ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (1 * rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y

Tactic:
apply HasDerivAt.mul (hasDerivAt_id' y)

Result:
ε y : ℝ
⊢ HasDerivAt (fun y => rexp (-(ε * y * y))) (rexp (-(ε * y * y)) * (-2 * ε * y)) y
-- Mathlib/Data/Matroid/Restrict.lean
theorem restrict_eq_self_iff : M ↾ R = M ↔ R = M.E :=
  ⟨fun h ↦ by rw [← h]; rfl, fun h ↦ by simp [h]⟩

Proof state:
α : Type u_1
M : Matroid α
R : Set α
h : R = M.E
⊢ M ↾ R = M

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = M.E

Tactic:
rw [← h]

Result:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = (M ↾ R).E

Proof state:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = (M ↾ R).E

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
lemma injective_germ_basicOpen (U : X.Opens) (hU : IsAffineOpen U)
    (x : X) (hx : x ∈ U) (f : Γ(X, U))
    (hf : x ∈ X.basicOpen f)
    (H : Function.Injective (X.presheaf.germ U x hx)) :
    Function.Injective (X.presheaf.germ (X.basicOpen f) x hf)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
t : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
ht : (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) t = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ t = 0

Tactic:
obtain ⟨t, s, rfl⟩ := IsLocalization.mk'_surjective (.powers f) t

Result:
case intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
      (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s) =
    0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

Proof state:
case intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht : (ConcreteCategory.hom (X.presheaf.germ U x ⋯)) t = 0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

Tactic:
rw [H _ ht, IsLocalization.mk'_zero]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem ne_zero_of_mem_integerSet (a : integerSet K) : (a : mixedSpace K) ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
this : ↑a = 0
⊢ False

Tactic:
exact a.prop.1.2 (this.symm ▸ mixedEmbedding.norm.map_zero')

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ ↑a ≠ 0

Tactic:
by_contra!

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
this : ↑a = 0
⊢ False
-- Mathlib/Algebra/GeomSum.lean
theorem Nat.geom_sum_Ico_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
    ∑ i ∈ Ico 1 n, a / b ^ i ≤ a / (b - 1)

Proof state:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)

Tactic:
calc
  (a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by
    rw [pow_zero, Nat.div_one]
  _ = ∑ i ∈ range n.succ, a / b ^ i := by
    rw [range_eq_Ico, ← Nat.Ico_insert_succ_left (Nat.succ_pos _), sum_insert]
    exact fun h => zero_lt_one.not_le (mem_Ico.1 h).1
  _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
  _ = (a * 1 + a * (b - 1)) / (b - 1) := by
    rw [← mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)]
  _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]

Result:
no goals

Proof state:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ range n.succ, a / b ^ i

Tactic:
rw [range_eq_Ico, ← Nat.Ico_insert_succ_left (Nat.succ_pos _), sum_insert]

Result:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 0 ∉ Ico (succ 0) n.succ

Proof state:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 0 ∉ Ico (succ 0) n.succ

Tactic:
exact fun h => zero_lt_one.not_le (mem_Ico.1 h).1

Result:
no goals

Proof state:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ Ico 1 n, a / b ^ i ≤ a / (b - 1)

Tactic:
rcases n with - | n

Result:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ ∑ i ∈ Ico 1 0, a / b ^ i ≤ a / (b - 1)

case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a / (b - 1)

Proof state:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a / (b - 1)

Tactic:
rw [← add_le_add_iff_left a]

Result:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)

Proof state:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)

Tactic:
rw [← mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)]

Result:
no goals

Proof state:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)

Tactic:
rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]

Result:
no goals

Proof state:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ ∑ i ∈ Ico 1 0, a / b ^ i ≤ a / (b - 1)

Tactic:
rw [Ico_eq_empty_of_le (zero_le_one' ℕ), sum_empty]

Result:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)

Proof state:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i

Tactic:
rw [pow_zero, Nat.div_one]

Result:
no goals

Proof state:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)

Tactic:
exact Nat.zero_le _

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
theorem mul_eq_add : p * q = p + q

Proof state:
p q : ℝ
h : p.IsConjExponent q
⊢ p * q = p + q

Tactic:
simpa only [sub_mul, sub_eq_iff_eq_add, one_mul] using h.sub_one_mul_conj

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
theorem jacobiTheta₂_functional_equation (z τ : ℂ) : jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Proof state:
case e_a.e_f.h.e_z
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑π * (↑n + I * (I * z)) ^ 2 * (τ * τ) =
    (-(↑π * I * z ^ 2 * τ) + (2 * ↑π * I * ↑n * z + -(↑π * I * ↑n ^ 2)) * τ) * (I * τ)

Tactic:
ring_nf

Result:
case e_a.e_f.h.e_z
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑π * ↑n * I ^ 2 * z * τ ^ 2 * 2 + ↑π * ↑n ^ 2 * τ ^ 2 + ↑π * I ^ 4 * z ^ 2 * τ ^ 2 =
    ↑π * ↑n * I ^ 2 * z * τ ^ 2 * 2 + (-(↑π * ↑n ^ 2 * I ^ 2 * τ ^ 2) - ↑π * I ^ 2 * z ^ 2 * τ ^ 2)

Proof state:
case inr
z τ : ℂ
hτ : 0 < τ.im
⊢ ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Tactic:
have h0 : τ ≠ 0 := by contrapose! hτ; rw [hτ, zero_im]

Result:
case inr
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
⊢ ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Proof state:
case e_a.e_f.h.e_z
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑π * ↑n * I ^ 2 * z * τ ^ 2 * 2 + ↑π * ↑n ^ 2 * τ ^ 2 + ↑π * I ^ 4 * z ^ 2 * τ ^ 2 =
    ↑π * ↑n * I ^ 2 * z * τ ^ 2 * 2 + (-(↑π * ↑n ^ 2 * I ^ 2 * τ ^ 2) - ↑π * I ^ 2 * z ^ 2 * τ ^ 2)

Tactic:
simp_rw [I_sq, I_pow_four]

Result:
case e_a.e_f.h.e_z
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑π * ↑n * -1 * z * τ ^ 2 * 2 + ↑π * ↑n ^ 2 * τ ^ 2 + ↑π * 1 * z ^ 2 * τ ^ 2 =
    ↑π * ↑n * -1 * z * τ ^ 2 * 2 + (-(↑π * ↑n ^ 2 * -1 * τ ^ 2) - ↑π * -1 * z ^ 2 * τ ^ 2)
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem haarMeasure_unique (μ : Measure G) [SigmaFinite μ] [IsMulLeftInvariant μ]
    (K₀ : PositiveCompacts G) : μ = μ K₀ • haarMeasure K₀

Proof state:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
A : (interior (closure ↑K₀)).Nonempty
⊢ μ = μ ↑K₀ • haarMeasure K₀

Tactic:
have := measure_eq_div_smul μ (haarMeasure K₀)
  (measure_pos_of_nonempty_interior _ A).ne' K₀.isCompact.closure.measure_ne_top

Result:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
A : (interior (closure ↑K₀)).Nonempty
this : μ = (μ (closure ↑K₀) / (haarMeasure K₀) (closure ↑K₀)) • haarMeasure K₀
⊢ μ = μ ↑K₀ • haarMeasure K₀

Proof state:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
⊢ μ = μ ↑K₀ • haarMeasure K₀

Tactic:
have A : Set.Nonempty (interior (closure (K₀ : Set G))) :=
  K₀.interior_nonempty.mono (interior_mono subset_closure)

Result:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
A : (interior (closure ↑K₀)).Nonempty
⊢ μ = μ ↑K₀ • haarMeasure K₀

Proof state:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
A : (interior (closure ↑K₀)).Nonempty
this : μ = (μ (closure ↑K₀) / (haarMeasure K₀) (closure ↑K₀)) • haarMeasure K₀
⊢ μ = μ ↑K₀ • haarMeasure K₀

Tactic:
rwa [haarMeasure_closure_self, div_one, K₀.isCompact.measure_closure] at this

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.equicontinuousWithinAt_iff_left {p : κ → Prop} {s : κ → Set X}
    {F : ι → X → α} {S : Set X} {x₀ : X} (hX : (𝓝[S] x₀).HasBasis p s) :
    EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ i, (F i x₀, F i x) ∈ U

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α ib}) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p s
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
  hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]

Result:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α ib}) ↔
    ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U