harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finmap.lean
theorem insert_toFinmap (a : α) (b : β a) (s : AList β) :
    insert a b (AList.toFinmap s) = AList.toFinmap (s.insert a b)

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ insert a b ⟦s⟧ = ⟦AList.insert a b s⟧

Tactic:
simp [insert]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem edist_le_Ico_sum_edist (f : ℕ → α) {m n} (h : m ≤ n) :
    edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))

Tactic:
induction n, h using Nat.le_induction with
| base => rw [Finset.Ico_self, Finset.sum_empty, edist_self]
| succ n hle ihn =>
  calc
    edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _
    _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
    _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
    { rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]; simp }

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), edist (f i) (f (i + 1))

Tactic:
rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Proof state:
case base
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, edist (f i) (f (i + 1))

Tactic:
rw [Finset.Ico_self, Finset.sum_empty, edist_self]

Result:
no goals

Proof state:
case succ
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m (n + 1), edist (f i) (f (i + 1))

Tactic:
calc
  edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _
  _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
  _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
  { rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]; simp }

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem isLimit_mul_left {a b : Ordinal} (l : IsLimit a) (b0 : 0 < b) : IsLimit (a * b)

Proof state:
case inl
a : Ordinal.{u_4}
l : a.IsLimit
b0 : 0 < 0
⊢ (a * 0).IsLimit

Tactic:
exact b0.false.elim

Result:
no goals

Proof state:
case inr.inl.intro
a : Ordinal.{u_4}
l : a.IsLimit
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ (a * b + a).IsLimit

Tactic:
exact isLimit_add _ l

Result:
no goals

Proof state:
case inr.inr
a b : Ordinal.{u_4}
l : a.IsLimit
b0 : 0 < b
lb : b.IsLimit
⊢ (a * b).IsLimit

Tactic:
exact isLimit_mul l.pos lb

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
l : a.IsLimit
b0 : 0 < b
⊢ (a * b).IsLimit

Tactic:
rcases zero_or_succ_or_limit b with (rfl | ⟨b, rfl⟩ | lb)

Result:
case inl
a : Ordinal.{u_4}
l : a.IsLimit
b0 : 0 < 0
⊢ (a * 0).IsLimit

case inr.inl.intro
a : Ordinal.{u_4}
l : a.IsLimit
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ (a * succ b).IsLimit

case inr.inr
a b : Ordinal.{u_4}
l : a.IsLimit
b0 : 0 < b
lb : b.IsLimit
⊢ (a * b).IsLimit

Proof state:
case inr.inl.intro
a : Ordinal.{u_4}
l : a.IsLimit
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ (a * succ b).IsLimit

Tactic:
rw [mul_succ]

Result:
case inr.inl.intro
a : Ordinal.{u_4}
l : a.IsLimit
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ (a * b + a).IsLimit
-- Mathlib/Data/Sym/Sym2.lean
@[simp]
lemma pmap_subtype_map_subtypeVal {P : α → Prop} (s : Sym2 α) (h : ∀ a ∈ s, P a) :
    (s.pmap Subtype.mk h).map Subtype.val = s

Proof state:
α : Type u_1
P : α → Prop
s : Sym2 α
h : ∀ a ∈ s, P a
⊢ map Subtype.val (pmap Subtype.mk s h) = s

Tactic:
induction' s with x y

Result:
case h
α : Type u_1
P : α → Prop
x y : α
h : ∀ a ∈ s(x, y), P a
⊢ map Subtype.val (pmap Subtype.mk s(x, y) h) = s(x, y)

Proof state:
case h
α : Type u_1
P : α → Prop
x y : α
h : ∀ a ∈ s(x, y), P a
⊢ map Subtype.val (pmap Subtype.mk s(x, y) h) = s(x, y)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem coe_lowerCentralSeries_eq_int [LieModule R L M] (k : ℕ) :
    (lowerCentralSeries R L M k : Set M) = (lowerCentralSeries ℤ L M k : Set M)

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Tactic:
simp only [LieSubmodule.mem_top, ih, true_and]

Result:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Proof state:
case succ.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x}) ≤
    ↑(Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Tactic:
simp only [← ih]

Result:
case succ.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) ≤
    ↑(Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x})
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
theorem sub_one_pow_totient_le_cyclotomic_eval {q : ℝ} (hq' : 1 < q) :
    ∀ n, (q - 1) ^ totient n ≤ (cyclotomic n ℝ).eval q
  | 0 => by simp only [totient_zero, _root_.pow_zero, cyclotomic_zero, eval_one, le_refl]
  | 1 => by simp only [totient_one, pow_one, cyclotomic_one, eval_sub, eval_X, eval_one, le_refl]
  | _ + 2 => (sub_one_pow_totient_lt_cyclotomic_eval le_add_self hq').le

Proof state:
q : ℝ
hq' : 1 < q
⊢ (q - 1) ^ φ 1 ≤ eval q (cyclotomic 1 ℝ)

Tactic:
simp only [totient_one, pow_one, cyclotomic_one, eval_sub, eval_X, eval_one, le_refl]

Result:
no goals

Proof state:
q : ℝ
hq' : 1 < q
⊢ (q - 1) ^ φ 0 ≤ eval q (cyclotomic 0 ℝ)

Tactic:
simp only [totient_zero, _root_.pow_zero, cyclotomic_zero, eval_one, le_refl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_of_getElem {l : List α} {i : Nat} {h} {a : α} (e : l[i] = a) : a ∈ l

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ l[i] ∈ l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.length
a : α
e : l[i] = a
⊢ a ∈ l

Tactic:
subst e

Result:
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ l[i] ∈ l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0

Proof state:
n : Nat
k : Fin (n + 1)
⊢ k * 0 = 0

Tactic:
simp [Fin.ext_iff, mul_def]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem LiftRel.refl (R : α → α → Prop) (H : Reflexive R) : Reflexive (LiftRel R) := fun s => by
  refine ⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩
  rw [← h]
  apply Computation.LiftRel.refl
  intro a
  rcases a with - | a
  · simp
  · cases a
    simp only [LiftRelO, and_true]
    apply H

Proof state:
case H.some.mk
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
fst✝ : α
snd✝ : WSeq α
⊢ LiftRelO R (fun x1 x2 => x1 = x2) (some (fst✝, snd✝)) (some (fst✝, snd✝))

Tactic:
simp only [LiftRelO, and_true]

Result:
case H.some.mk
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
fst✝ : α
snd✝ : WSeq α
⊢ R fst✝ fst✝

Proof state:
case H
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
a : Option (α × WSeq α)
⊢ LiftRelO R (fun x1 x2 => x1 = x2) a a

Tactic:
rcases a with - | a

Result:
case H.none
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ LiftRelO R (fun x1 x2 => x1 = x2) none none

case H.some
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
a : α × WSeq α
⊢ LiftRelO R (fun x1 x2 => x1 = x2) (some a) (some a)

Proof state:
case H.some
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
a : α × WSeq α
⊢ LiftRelO R (fun x1 x2 => x1 = x2) (some a) (some a)

Tactic:
cases a

Result:
case H.some.mk
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
fst✝ : α
snd✝ : WSeq α
⊢ LiftRelO R (fun x1 x2 => x1 = x2) (some (fst✝, snd✝)) (some (fst✝, snd✝))

Proof state:
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x1 x2 => x1 = x2) s.destruct t.destruct

Tactic:
rw [← h]

Result:
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x1 x2 => x1 = x2) s.destruct s.destruct

Proof state:
case H.some.mk
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
fst✝ : α
snd✝ : WSeq α
⊢ R fst✝ fst✝

Tactic:
apply H

Result:
no goals

Proof state:
case H.none
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ LiftRelO R (fun x1 x2 => x1 = x2) none none

Tactic:
simp

Result:
no goals

Proof state:
case H
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ Reflexive (LiftRelO R fun x1 x2 => x1 = x2)

Tactic:
intro a

Result:
case H
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
a : Option (α × WSeq α)
⊢ LiftRelO R (fun x1 x2 => x1 = x2) a a

Proof state:
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x1 x2 => x1 = x2) s.destruct s.destruct

Tactic:
apply Computation.LiftRel.refl

Result:
case H
α : Type u
R : α → α → Prop
H : Reflexive R
s✝ s t : WSeq α
h : s = t
⊢ Reflexive (LiftRelO R fun x1 x2 => x1 = x2)
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_Ico [DivisionRing α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) :
    ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)

Proof state:
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)

Tactic:
simp only [sum_Ico_eq_sub _ hmn, geom_sum_eq hx, div_sub_div_same, sub_sub_sub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem toFinset_prod_dvd_prod [CommMonoid α] (S : Multiset α) : S.toFinset.prod id ∣ S.prod

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
S : Multiset α
⊢ (map id S.toFinset.val).prod ∣ S.prod

Tactic:
refine Multiset.prod_dvd_prod_of_le ?_

Result:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
S : Multiset α
⊢ map id S.toFinset.val ≤ S

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
S : Multiset α
⊢ S.toFinset.prod id ∣ S.prod

Tactic:
rw [Finset.prod_eq_multiset_prod]

Result:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
S : Multiset α
⊢ (map id S.toFinset.val).prod ∣ S.prod

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
S : Multiset α
⊢ map id S.toFinset.val ≤ S

Tactic:
simp [Multiset.dedup_le S]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dense_compl_of_dimH_lt_finrank {s : Set E} (hs : dimH s < finrank ℝ E) : Dense sᶜ

Proof state:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ⊆ s
⊢ dimH t ≤ dimH s

Tactic:
exact dimH_mono he

Result:
no goals

Proof state:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : dimH s < ↑(finrank ℝ E)
⊢ Dense sᶜ

Tactic:
refine fun x => mem_closure_iff_nhds.2 fun t ht => nonempty_iff_ne_empty.2 fun he => hs.not_le ?_

Result:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ∩ sᶜ = ∅
⊢ ↑(finrank ℝ E) ≤ dimH s

Proof state:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ∩ sᶜ = ∅
⊢ ↑(finrank ℝ E) ≤ dimH s

Tactic:
rw [← diff_eq, diff_eq_empty] at he

Result:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ⊆ s
⊢ ↑(finrank ℝ E) ≤ dimH s

Proof state:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ⊆ s
⊢ ↑(finrank ℝ E) ≤ dimH s

Tactic:
rw [← Real.dimH_of_mem_nhds ht]

Result:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ⊆ s
⊢ dimH t ≤ dimH s
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.1 ≠ 0) :
    ContinuousAt (fun p : ℝ × ℝ => p.1 ^ p.2) p

Proof state:
case inl
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun p => p.1 ^ p.2) p

Tactic:
rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]

Result:
case inl
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x => rexp (log x.1 * x.2) * cos (x.2 * π)) p

Proof state:
case inl.refine_1
p : ℝ × ℝ
hp : p.1 < 0
⊢ p.1 ≠ 0

Tactic:
exact hp.ne

Result:
no goals

Proof state:
case inr
p : ℝ × ℝ
hp : p.1 > 0
⊢ ContinuousAt (fun p => p.1 ^ p.2) p

Tactic:
rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]

Result:
case inr
p : ℝ × ℝ
hp : p.1 > 0
⊢ ContinuousAt (fun x => rexp (log x.1 * x.2)) p

Proof state:
p : ℝ × ℝ
hp : p.1 ≠ 0
⊢ ContinuousAt (fun p => p.1 ^ p.2) p

Tactic:
rw [ne_iff_lt_or_gt] at hp

Result:
p : ℝ × ℝ
hp : p.1 < 0 ∨ p.1 > 0
⊢ ContinuousAt (fun p => p.1 ^ p.2) p

Proof state:
case inr
p : ℝ × ℝ
hp : p.1 > 0
⊢ ContinuousAt (fun x => rexp (log x.1 * x.2)) p

Tactic:
refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)

Result:
case inr
p : ℝ × ℝ
hp : p.1 > 0
⊢ ContinuousAt (fun x => log x.1) p

Proof state:
case inl
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x => rexp (log x.1 * x.2) * cos (x.2 * π)) p

Tactic:
refine ContinuousAt.mul ?_ (continuous_cos.continuousAt.comp ?_)

Result:
case inl.refine_1
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x => rexp (log x.1 * x.2)) p

case inl.refine_2
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x => x.2 * π) p

Proof state:
case inl.refine_1
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x => log x.1) p

Tactic:
refine (continuousAt_log ?_).comp continuous_fst.continuousAt

Result:
case inl.refine_1
p : ℝ × ℝ
hp : p.1 < 0
⊢ p.1 ≠ 0

Proof state:
case inr
p : ℝ × ℝ
hp : p.1 > 0
⊢ p.1 ≠ 0

Tactic:
exact hp.lt.ne.symm

Result:
no goals

Proof state:
case inl.refine_1
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x => rexp (log x.1 * x.2)) p

Tactic:
refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)

Result:
case inl.refine_1
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x => log x.1) p

Proof state:
case inl.refine_2
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x => x.2 * π) p

Tactic:
exact continuous_snd.continuousAt.mul continuousAt_const

Result:
no goals

Proof state:
case inr
p : ℝ × ℝ
hp : p.1 > 0
⊢ ContinuousAt (fun x => log x.1) p

Tactic:
refine (continuousAt_log ?_).comp continuous_fst.continuousAt

Result:
case inr
p : ℝ × ℝ
hp : p.1 > 0
⊢ p.1 ≠ 0
-- Mathlib/Data/Finset/Density.lean
lemma dens_lt_dens (h : s ⊂ t) : dens s < dens t :=
  div_lt_div_of_pos_right (mod_cast card_strictMono h) <| by
    cases isEmpty_or_nonempty α
    · simp [Subsingleton.elim s t, ssubset_irrfl] at h
    · exact mod_cast Fintype.card_pos

Proof state:
case inl
α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : s ⊂ t
h✝ : IsEmpty α
⊢ 0 < ↑(Fintype.card α)

Tactic:
simp [Subsingleton.elim s t, ssubset_irrfl] at h

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : s ⊂ t
⊢ 0 < ↑(Fintype.card α)

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : s ⊂ t
h✝ : IsEmpty α
⊢ 0 < ↑(Fintype.card α)

case inr
α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : s ⊂ t
h✝ : Nonempty α
⊢ 0 < ↑(Fintype.card α)

Proof state:
case inr
α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : s ⊂ t
h✝ : Nonempty α
⊢ 0 < ↑(Fintype.card α)

Tactic:
exact mod_cast Fintype.card_pos

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_congr (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₁ =O[l] g₁ ↔ f₂ =O[l] g₂

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =O[l] g₁ ↔ f₂ =O[l] g₂

Tactic:
simp only [IsBigO_def]

Result:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∃ c, IsBigOWith c l f₁ g₁) ↔ ∃ c, IsBigOWith c l f₂ g₂

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∃ c, IsBigOWith c l f₁ g₁) ↔ ∃ c, IsBigOWith c l f₂ g₂

Tactic:
exact exists_congr fun c => isBigOWith_congr rfl hf hg

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd'_add_zero_inv_app (a : A) (X : C) :
    (shiftFunctorAdd' C a 0 a (add_zero a)).inv.app X =
    (shiftFunctorZero C A).hom.app (X⟦a⟧)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd' C a 0 a ⋯).inv.app X = (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X)

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd'_add_zero C a)) X

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem contDiffWithinAt_prod {t : Finset ι} {f : ι → E → 𝔸'}
    (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) :
    ContDiffWithinAt 𝕜 n (fun y => ∏ i ∈ t, f i y) s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
x : E
n : WithTop ℕ∞
𝔸' : Type u_4
ι : Type u_5
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
t : Finset ι
f : ι → E → 𝔸'
h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x
⊢ ContDiffWithinAt 𝕜 n (fun y => ∏ i ∈ t, f i y) s x

Tactic:
simpa only [← Finset.prod_apply] using contDiffWithinAt_prod' h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_le_length_insertListConst [BEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} :
    l.length ≤ (insertListConst l toInsert).length

Proof state:
case nil
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
⊢ l.length ≤ (insertListConst l []).length

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
inst✝ : BEq α
hd : α × β
tl : List (α × β)
ih : ∀ {l : List ((_ : α) × β)}, l.length ≤ (insertListConst l tl).length
l : List ((_ : α) × β)
⊢ l.length ≤ (insertListConst l (hd :: tl)).length

Tactic:
exact Nat.le_trans length_le_length_insertEntry ih

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ l.length ≤ (insertListConst l toInsert).length

Tactic:
induction toInsert generalizing l with
| nil => apply Nat.le_refl
| cons hd tl ih => exact Nat.le_trans length_le_length_insertEntry ih

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/LazyList.lean
theorem append_assoc {α} (xs ys zs : LazyList α) :
    (xs.append ys).append zs = xs.append (ys.append zs)

Proof state:
α : Type u_1
xs ys zs : LazyList α
⊢ (xs.append { fn := fun x => ys }).append { fn := fun x => zs } =
    xs.append { fn := fun x => ys.append { fn := fun x => zs } }

Tactic:
induction xs using LazyList.rec with
| nil => simp only [append, Thunk.get]
| cons _ _ => simpa only [append, cons.injEq, true_and]
| mk _ ih => ext; apply ih

Result:
no goals

Proof state:
case cons
α : Type u_1
xs ys zs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.45254 tl✝
⊢ ((cons hd✝ tl✝).append { fn := fun x => ys }).append { fn := fun x => zs } =
    (cons hd✝ tl✝).append { fn := fun x => ys.append { fn := fun x => zs } }

Tactic:
simpa only [append, cons.injEq, true_and]

Result:
no goals

Proof state:
case mk.a
α : Type u_1
ys zs : LazyList α
fn✝ : Unit → LazyList α
ih :
  ∀ (a : Unit),
    ((fn✝ a).append { fn := fun x => ys }).append { fn := fun x => zs } =
      (fn✝ a).append { fn := fun x => ys.append { fn := fun x => zs } }
⊢ {
        fn := fun x =>
          { fn := fun x => { fn := fn✝ }.get.append { fn := fun x => ys } }.get.append { fn := fun x => zs } }.get =
    { fn := fun x => { fn := fn✝ }.get.append { fn := fun x => ys.append { fn := fun x => zs } } }.get

Tactic:
apply ih

Result:
no goals

Proof state:
case nil
α : Type u_1
ys zs : LazyList α
⊢ (nil.append { fn := fun x => ys }).append { fn := fun x => zs } =
    nil.append { fn := fun x => ys.append { fn := fun x => zs } }

Tactic:
simp only [append, Thunk.get]

Result:
no goals

Proof state:
case mk
α : Type u_1
ys zs : LazyList α
fn✝ : Unit → LazyList α
ih :
  ∀ (a : Unit),
    ((fn✝ a).append { fn := fun x => ys }).append { fn := fun x => zs } =
      (fn✝ a).append { fn := fun x => ys.append { fn := fun x => zs } }
⊢ {
      fn := fun x =>
        { fn := fun x => { fn := fn✝ }.get.append { fn := fun x => ys } }.get.append { fn := fun x => zs } } =
    { fn := fun x => { fn := fn✝ }.get.append { fn := fun x => ys.append { fn := fun x => zs } } }

Tactic:
ext

Result:
case mk.a
α : Type u_1
ys zs : LazyList α
fn✝ : Unit → LazyList α
ih :
  ∀ (a : Unit),
    ((fn✝ a).append { fn := fun x => ys }).append { fn := fun x => zs } =
      (fn✝ a).append { fn := fun x => ys.append { fn := fun x => zs } }
⊢ {
        fn := fun x =>
          { fn := fun x => { fn := fn✝ }.get.append { fn := fun x => ys } }.get.append { fn := fun x => zs } }.get =
    { fn := fun x => { fn := fn✝ }.get.append { fn := fun x => ys.append { fn := fun x => zs } } }.get
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma ι_comp_colimitOpIsoOpLimit_hom (F : J ⥤ C) [HasLimit F] (j : Jᵒᵖ) :
    colimit.ι F.op j ≫ (colimitOpIsoOpLimit F).hom = (limit.π F j.unop).op

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ C
inst✝ : HasLimit F
j : Jᵒᵖ
⊢ colimit.ι F.op j ≫ (colimitOpIsoOpLimit F).hom = (limit.π F (unop j)).op

Tactic:
simp [colimitOpIsoOpLimit]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n)

Proof state:
s n : Nat
⊢ range' s n = map (fun x => s + x) (range n)

Tactic:
rw [range_eq_range', map_add_range']

Result:
s n : Nat
⊢ range' s n = range' (s + 0) n

Proof state:
s n : Nat
⊢ range' s n = range' (s + 0) n

Tactic:
rfl

Result:
no goals