harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_lt_logb_iff (hx : 0 < x) (hy : 0 < y) : logb b x < logb b y ↔ x < y

Proof state:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ logb b x < logb b y ↔ x < y

Tactic:
rw [logb, logb, div_lt_div_iff_of_pos_right (log_pos hb)]

Result:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y

Proof state:
b x y : ℝ
hb : 1 < b
hx : 0 < x
hy : 0 < y
⊢ log x < log y ↔ x < y

Tactic:
exact log_lt_log_iff hx hy

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_one_add' (hx : 0 ≤ x) (h : 1 + y ≠ 0) : x ^ (1 + y) = x * x ^ y

Proof state:
x y : ℝ
hx : 0 ≤ x
h : 1 + y ≠ 0
⊢ x ^ (1 + y) = x * x ^ y

Tactic:
rw [rpow_add' hx h, rpow_one]

Result:
no goals
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_add_le_add_rpow {p : ℝ} (a b : ℝ≥0∞) (hp : 0 ≤ p) (hp1 : p ≤ 1) :
    (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
have h := rpow_add_rpow_le a b hp_pos hp1

Result:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
case inl
a b : ℝ≥0∞
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
repeat' rw [ENNReal.rpow_one] at h

Result:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
rw [one_div_one, one_div] at h

Result:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
exact (ENNReal.le_rpow_inv_iff hp_pos).mp h

Result:
no goals

Proof state:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
rw [ENNReal.rpow_one] at h

Result:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
rcases hp.eq_or_lt with (rfl | hp_pos)

Result:
case inl
a b : ℝ≥0∞
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0

case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
-- Mathlib/CategoryTheory/Grothendieck.lean
theorem congr {X Y : Grothendieck F} {f g : X ⟶ Y} (h : f = g) :
    f.fiber = eqToHom (by subst h; rfl) ≫ g.fiber

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (F.map f.base).obj X.fiber = (F.map f.base).obj X.fiber

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ f.fiber = eqToHom ⋯ ≫ f.fiber

Tactic:
dsimp

Result:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ f.fiber = 𝟙 ((F.map f.base).obj X.fiber) ≫ f.fiber

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
⊢ (F.map f.base).obj X.fiber = (F.map g.base).obj X.fiber

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (F.map f.base).obj X.fiber = (F.map f.base).obj X.fiber

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ f.fiber = 𝟙 ((F.map f.base).obj X.fiber) ≫ f.fiber

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
⊢ f.fiber = eqToHom ⋯ ≫ g.fiber

Tactic:
subst h

Result:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ f.fiber = eqToHom ⋯ ≫ f.fiber
-- Mathlib/Data/Finset/Update.lean
theorem updateFinset_singleton {i y} :
    updateFinset x {i} y = Function.update x i (y ⟨i, mem_singleton_self i⟩)

Proof state:
case pos
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : { x // x ∈ {i} }) → π ↑i_1
j : ι
hj : j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

Tactic:
cases hj

Result:
case pos.refl
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : { x // x ∈ {i} }) → π ↑i_1
⊢ updateFinset x {i} y i = update x i (y ⟨i, ⋯⟩) i

Proof state:
case pos.refl
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : { x // x ∈ {i} }) → π ↑i_1
⊢ updateFinset x {i} y i = update x i (y ⟨i, ⋯⟩) i

Tactic:
simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]

Result:
no goals

Proof state:
case h
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : { x // x ∈ {i} }) → π ↑i_1
j : ι
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

Tactic:
by_cases hj : j = i

Result:
case pos
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : { x // x ∈ {i} }) → π ↑i_1
j : ι
hj : j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : { x // x ∈ {i} }) → π ↑i_1
j : ι
hj : ¬j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

Proof state:
case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : { x // x ∈ {i} }) → π ↑i_1
j : ι
hj : ¬j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

Tactic:
simp [hj, updateFinset]

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : { x // x ∈ {i} }) → π ↑i_1
⊢ updateFinset x {i} y = update x i (y ⟨i, ⋯⟩)

Tactic:
congr with j

Result:
case h
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : { x // x ∈ {i} }) → π ↑i_1
j : ι
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_dblXYZ (P : Fin 3 → R) : (W'.map f).toJacobian.dblXYZ (f ∘ P) = f ∘ dblXYZ W' P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toJacobian.dblXYZ (⇑f ∘ P) = ⇑f ∘ W'.dblXYZ P

Tactic:
simp only [dblXYZ, map_dblX, map_dblY, map_dblZ, comp_fin3]

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem gold_pow_sub_gold_pow (n : ℕ) : φ ^ (n + 2) - φ ^ (n + 1) = φ ^ n

Proof state:
n : ℕ
⊢ √5 ^ 2 * (1 / 2 + √5 * (1 / 2)) ^ n * (1 / 4) + (1 / 2 + √5 * (1 / 2)) ^ n * (-1 / 4) = (1 / 2 + √5 * (1 / 2)) ^ n

Tactic:
norm_num

Result:
n : ℕ
⊢ 5 * (1 / 2 + √5 * (1 / 2)) ^ n * (1 / 4) + -((1 / 2 + √5 * (1 / 2)) ^ n * (1 / 4)) = (1 / 2 + √5 * (1 / 2)) ^ n

Proof state:
n : ℕ
⊢ ((1 + √5) / 2) ^ (n + 2) - ((1 + √5) / 2) ^ (n + 1) = ((1 + √5) / 2) ^ n

Tactic:
ring_nf

Result:
n : ℕ
⊢ √5 ^ 2 * (1 / 2 + √5 * (1 / 2)) ^ n * (1 / 4) + (1 / 2 + √5 * (1 / 2)) ^ n * (-1 / 4) = (1 / 2 + √5 * (1 / 2)) ^ n

Proof state:
n : ℕ
⊢ 5 * (1 / 2 + √5 * (1 / 2)) ^ n * (1 / 4) + -((1 / 2 + √5 * (1 / 2)) ^ n * (1 / 4)) = (1 / 2 + √5 * (1 / 2)) ^ n

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
⊢ φ ^ (n + 2) - φ ^ (n + 1) = φ ^ n

Tactic:
rw [goldenRatio]

Result:
n : ℕ
⊢ ((1 + √5) / 2) ^ (n + 2) - ((1 + √5) / 2) ^ (n + 1) = ((1 + √5) / 2) ^ n
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem tendsto_verticalIntegral (hb : 0 < b.re) (c : ℝ) :
    Tendsto (verticalIntegral b c) atTop (𝓝 0)

Proof state:
case hf
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x => b.re * x ^ 2 - 2 * |b.im| * |c| * x) atTop atTop

Tactic:
simp_rw [sq, ← mul_assoc, ← sub_mul]

Result:
case hf
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x => (b.re * x - 2 * |b.im| * |c|) * x) atTop atTop

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ 0 = 2 * |c| * 0

Tactic:
ring

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun T => b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2) atTop atTop

Tactic:
apply tendsto_atTop_add_const_right

Result:
case hf
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x => b.re * x ^ 2 - 2 * |b.im| * |c| * x) atTop atTop

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun T => 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))) atTop (𝓝 0)

Tactic:
rw [(by ring : 0 = 2 * |c| * 0)]

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun T => 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))) atTop (𝓝 (2 * |c| * 0))

Proof state:
case hf
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (HMul.hMul b.re) atTop atTop

Tactic:
exact (tendsto_const_mul_atTop_of_pos hb).mpr tendsto_id

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun T => 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))) atTop (𝓝 (2 * |c| * 0))

Tactic:
refine (tendsto_exp_atBot.comp (tendsto_neg_atTop_atBot.comp ?_)).const_mul _

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun T => b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2) atTop atTop

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x => ‖verticalIntegral b c x‖) atTop (𝓝 0)

Tactic:
refine
  tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds ?_
    (Eventually.of_forall fun _ => norm_nonneg _)
    ((eventually_ge_atTop (0 : ℝ)).mp
      (Eventually.of_forall fun T hT => verticalIntegral_norm_le hb c hT))

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun T => 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))) atTop (𝓝 0)

Proof state:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (verticalIntegral b c) atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Result:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x => ‖verticalIntegral b c x‖) atTop (𝓝 0)

Proof state:
case hf
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x => (b.re * x - 2 * |b.im| * |c|) * x) atTop atTop

Tactic:
refine Tendsto.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_) tendsto_id

Result:
case hf
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (HMul.hMul b.re) atTop atTop
-- Mathlib/Data/Finset/Dedup.lean
theorem nodup_toList (s : Finset α) : s.toList.Nodup

Proof state:
α : Type u_1
s : Finset α
⊢ s.val.Nodup

Tactic:
exact s.nodup

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
⊢ s.toList.Nodup

Tactic:
rw [toList, ← Multiset.coe_nodup, Multiset.coe_toList]

Result:
α : Type u_1
s : Finset α
⊢ s.val.Nodup
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_const_of_zero {n : SimplexCategory} (f : ⦋0⦌ ⟶ n) :
    f = const _ n (f.toOrderHom 0)

Proof state:
case a.h.h.h
n : SimplexCategory
f : ⦋0⦌ ⟶ n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom f) x) = ↑((Hom.toOrderHom (⦋0⦌.const n ((Hom.toOrderHom f) 0))) x)

Tactic:
match x with | 0 => rfl

Result:
no goals

Proof state:
n : SimplexCategory
f : ⦋0⦌ ⟶ n
⊢ f = ⦋0⦌.const n ((Hom.toOrderHom f) 0)

Tactic:
ext x

Result:
case a.h.h.h
n : SimplexCategory
f : ⦋0⦌ ⟶ n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom f) x) = ↑((Hom.toOrderHom (⦋0⦌.const n ((Hom.toOrderHom f) 0))) x)

Proof state:
n : SimplexCategory
f : ⦋0⦌ ⟶ n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom f) 0) = ↑((Hom.toOrderHom (⦋0⦌.const n ((Hom.toOrderHom f) 0))) 0)

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_set_eq_nat_iff_finset {α} {s : Set α} {n : ℕ} :
    #s = n ↔ ∃ t : Finset α, (t : Set α) = s ∧ t.card = n

Proof state:
α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n ↔ ∃ t, ↑t = s ∧ t.card = n

Tactic:
constructor

Result:
case mp
α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n → ∃ t, ↑t = s ∧ t.card = n

case mpr
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ t.card = n) → #↑s = ↑n

Proof state:
case mpr
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ t.card = n) → #↑s = ↑n

Tactic:
rintro ⟨t, rfl, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
t : Finset α
⊢ #↑↑t = ↑t.card

Proof state:
case mp
α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n → ∃ t, ↑t = s ∧ t.card = n

Tactic:
intro h

Result:
case mp
α : Type u_1
s : Set α
n : ℕ
h : #↑s = ↑n
⊢ ∃ t, ↑t = s ∧ t.card = n

Proof state:
case mp.intro
α : Type u_1
n : ℕ
s : Finset α
h : #↑↑s = ↑n
⊢ ∃ t, ↑t = ↑s ∧ t.card = n

Tactic:
simpa using h

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_1
t : Finset α
⊢ #↑↑t = ↑t.card

Tactic:
exact mk_coe_finset

Result:
no goals

Proof state:
case mp
α : Type u_1
s : Set α
n : ℕ
h : #↑s = ↑n
⊢ ∃ t, ↑t = s ∧ t.card = n

Tactic:
lift s to Finset α using lt_aleph0_iff_set_finite.1 (h.symm ▸ nat_lt_aleph0 n)

Result:
case mp.intro
α : Type u_1
n : ℕ
s : Finset α
h : #↑↑s = ↑n
⊢ ∃ t, ↑t = ↑s ∧ t.card = n
-- Mathlib/Topology/Bases.lean
theorem exists_dense_seq [SeparableSpace α] [Nonempty α] : ∃ u : ℕ → α, DenseRange u

Proof state:
case intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : s.Countable
s_dense : Dense s
u : ℕ → α
hu : s ⊆ range u
⊢ ∃ u, DenseRange u

Tactic:
exact ⟨u, s_dense.mono hu⟩

Result:
no goals

Proof state:
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
⊢ ∃ u, DenseRange u

Tactic:
obtain ⟨s : Set α, hs, s_dense⟩ := exists_countable_dense α

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : s.Countable
s_dense : Dense s
⊢ ∃ u, DenseRange u

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : s.Countable
s_dense : Dense s
⊢ ∃ u, DenseRange u

Tactic:
obtain ⟨u, hu⟩ := Set.countable_iff_exists_subset_range.mp hs

Result:
case intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : s.Countable
s_dense : Dense s
u : ℕ → α
hu : s ⊆ range u
⊢ ∃ u, DenseRange u
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem centralizer_univ : centralizer R Set.univ = center R A :=
  SetLike.ext' <| by rw [coe_centralizer, Set.univ_union, coe_center, Set.centralizer_univ]

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ ↑(centralizer R Set.univ) = ↑(center R A)

Tactic:
rw [coe_centralizer, Set.univ_union, coe_center, Set.centralizer_univ]

Result:
no goals
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem exists_forall_hasDerivAt_Ioo_eq_of_contDiffAt (hv : ContDiffAt ℝ 1 v x₀) :
    ∃ f : ℝ → E, f t₀ = x₀ ∧
      ∃ ε > (0 : ℝ), ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t

Proof state:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
inst✝ : CompleteSpace E
hv : ContDiffAt ℝ 1 v x₀
ε : ℝ
hε : ε > 0
w✝² : ℝ≥0
w✝¹ w✝ : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ w✝² w✝¹ w✝
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ t ∈ Icc (t₀ - ε) (t₀ + ε), HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
⊢ ∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t

Tactic:
exact ⟨f, hf1, ε, hε, fun t ht =>
  (hf2 t (Ioo_subset_Icc_self ht)).hasDerivAt (Icc_mem_nhds ht.1 ht.2)⟩

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
inst✝ : CompleteSpace E
hv : ContDiffAt ℝ 1 v x₀
⊢ ∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t

Tactic:
obtain ⟨ε, hε, _, _, _, hpl⟩ := exists_isPicardLindelof_const_of_contDiffAt t₀ hv

Result:
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
inst✝ : CompleteSpace E
hv : ContDiffAt ℝ 1 v x₀
ε : ℝ
hε : ε > 0
w✝² : ℝ≥0
w✝¹ w✝ : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ w✝² w✝¹ w✝
⊢ ∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t

Proof state:
case intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
inst✝ : CompleteSpace E
hv : ContDiffAt ℝ 1 v x₀
ε : ℝ
hε : ε > 0
w✝² : ℝ≥0
w✝¹ w✝ : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ w✝² w✝¹ w✝
⊢ ∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t

Tactic:
obtain ⟨f, hf1, hf2⟩ := hpl.exists_forall_hasDerivWithinAt_Icc_eq x₀

Result:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
v : E → E
t₀ : ℝ
x₀ : E
inst✝ : CompleteSpace E
hv : ContDiffAt ℝ 1 v x₀
ε : ℝ
hε : ε > 0
w✝² : ℝ≥0
w✝¹ w✝ : ℝ
hpl : IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ w✝² w✝¹ w✝
f : ℝ → E
hf1 : f t₀ = x₀
hf2 : ∀ t ∈ Icc (t₀ - ε) (t₀ + ε), HasDerivWithinAt f (v (f t)) (Icc (t₀ - ε) (t₀ + ε)) t
⊢ ∃ f, f t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t
-- Mathlib/Order/LiminfLimsup.lean
lemma blimsup_eq_limsup {f : Filter β} {u : β → α} {p : β → Prop} :
    blimsup u f p = limsup u (f ⊓ 𝓟 {x | p x})

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup u (f ⊓ 𝓟 {x | p x})

Tactic:
simp only [blimsup_eq, limsup_eq, eventually_inf_principal, mem_setOf_eq]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_iInf_iff {f : ι → LowerSet α} : (a ∈ ⨅ i, f i) ↔ ∀ i, a ∈ f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → LowerSet α
⊢ a ∈ ⋂ i, ↑(f i) ↔ ∀ (i : ι), a ∈ f i

Tactic:
exact mem_iInter

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → LowerSet α
⊢ a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i

Tactic:
rw [← SetLike.mem_coe, coe_iInf]

Result:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → LowerSet α
⊢ a ∈ ⋂ i, ↑(f i) ↔ ∀ (i : ι), a ∈ f i
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_pi_apply (x : V) : o.rotation π x = -x

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ (o.rotation ↑π) x = -x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma stabilizer_subset_div_right (ha : a ∈ s) : ↑(stabilizer G s) ⊆ s / {a} := fun b hb ↦
  ⟨_, by rwa [← smul_eq_mul, mem_stabilizer_set.1 hb], _, mem_singleton _, mul_div_cancel_right _ _⟩

Proof state:
G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b * a ∈ s

Tactic:
rwa [← smul_eq_mul, mem_stabilizer_set.1 hb]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
@[simp] lemma invert_C (t : R) : invert (C t) = C t

Proof state:
R : Type u_3
inst✝ : CommSemiring R
t : R
⊢ invert (C t) = C t

Tactic:
ext

Result:
case h
R : Type u_3
inst✝ : CommSemiring R
t : R
a✝ : ℤ
⊢ (invert (C t)) a✝ = (C t) a✝

Proof state:
case h
R : Type u_3
inst✝ : CommSemiring R
t : R
a✝ : ℤ
⊢ (invert (C t)) a✝ = (C t) a✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sigmaToiUnion_injective (h : Pairwise (Disjoint on t)) :
    Injective (sigmaToiUnion t)
  | ⟨a₁, b₁, h₁⟩, ⟨a₂, b₂, h₂⟩, eq =>
    have b_eq : b₁ = b₂ := congr_arg Subtype.val eq
    have a_eq : a₁ = a₂ :=
      by_contradiction fun ne =>
        have : b₁ ∈ t a₁ ∩ t a₂ := ⟨h₁, b_eq.symm ▸ h₂⟩
        (h ne).le_bot this
    Sigma.eq a_eq <| Subtype.eq <| by subst b_eq; subst a_eq; rfl

Proof state:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ h₂ : b₁ ∈ t a₁
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₁, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn ⋯ ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₁, ⟨b₁, h₂⟩⟩.snd

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₂, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn a_eq ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₂, ⟨b₁, h₂⟩⟩.snd

Tactic:
subst a_eq

Result:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ h₂ : b₁ ∈ t a₁
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₁, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn ⋯ ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₁, ⟨b₁, h₂⟩⟩.snd

Proof state:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
b₂ : β
h₂ : b₂ ∈ t a₂
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₂, ⟨b₂, h₂⟩⟩
b_eq : b₁ = b₂
a_eq : a₁ = a₂
⊢ ↑(Eq.recOn a_eq ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₂, ⟨b₂, h₂⟩⟩.snd

Tactic:
subst b_eq

Result:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₂, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn a_eq ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₂, ⟨b₁, h₂⟩⟩.snd
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem map_injective_of_injective (hg : Injective g) (k : LocalizationMap (S.map g) Q) :
    Injective (map f (apply_coe_mem_map g S) k) := fun z w hizw ↦ by
  set i := map f (apply_coe_mem_map g S) k
  have ifkg (a : M) : i (f.toMap a) = k.toMap (g a) := map_eq f (apply_coe_mem_map g S) a
  let ⟨z', w', x, hxz, hxw⟩ := surj₂ f z w
  have : k.toMap (g z') = k.toMap (g w')

Proof state:
case intro.mk.intro.intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
this : k.toMap (g z') = k.toMap (g w')
c : M
hc : c ∈ ↑S
eq : c * z' = c * w'
⊢ z = w

Tactic:
rw [← (f.map_units x).mul_left_inj, hxz, hxw, f.eq_iff_exists]

Result:
case intro.mk.intro.intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Injective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z w : N
i : N →* Q := f.map ⋯ k
hizw : i z = i w
ifkg : ∀ (a : M), i (f.toMap a) = k.toMap (g a)
z' w' : M
x : ↥S
hxz : z * f.toMap ↑x = f.toMap z'
hxw : w * f.toMap ↑x = f.toMap w'
this : k.toMap (g z') = k.toMap (g w')
c : M
hc : c ∈ ↑S
eq : c * z' = c * w'
⊢ ∃ c, ↑c * z' = ↑c * w'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_add_left {a b c : Int} (H : a ∣ c) : a ∣ b + c ↔ a ∣ b :=
  ⟨fun h => by have := Int.dvd_sub h H; rwa [Int.add_sub_cancel] at this, (Int.dvd_add · H)⟩

Proof state:
a b c : Int
H : a ∣ c
h : a ∣ b + c
⊢ a ∣ b

Tactic:
have := Int.dvd_sub h H

Result:
a b c : Int
H : a ∣ c
h : a ∣ b + c
this : a ∣ b + c - c
⊢ a ∣ b

Proof state:
a b c : Int
H : a ∣ c
h : a ∣ b + c
this : a ∣ b + c - c
⊢ a ∣ b

Tactic:
rwa [Int.add_sub_cancel] at this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Char/Lemmas.lean
theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4

Proof state:
c : Char
⊢ c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4

Tactic:
have := c.utf8Size_pos

Result:
c : Char
this : 0 < c.utf8Size
⊢ c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4

Proof state:
c : Char
this : 0 < c.utf8Size
⊢ c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4

Tactic:
have := c.utf8Size_le_four

Result:
c : Char
this✝ : 0 < c.utf8Size
this : c.utf8Size ≤ 4
⊢ c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4

Proof state:
c : Char
this✝ : 0 < c.utf8Size
this : c.utf8Size ≤ 4
⊢ c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4

Tactic:
omega

Result:
no goals