harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
theorem sub_one_pow_totient_lt_natAbs_cyclotomic_eval {n : ℕ} {q : ℕ} (hn' : 1 < n) (hq : q ≠ 1) :
    (q - 1) ^ totient n < ((cyclotomic n ℤ).eval ↑q).natAbs

Proof state:
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (q - 1) ^ φ n < (eval (↑q) (cyclotomic n ℤ)).natAbs

Tactic:
rw [← @Nat.cast_lt ℝ, Nat.cast_pow, Nat.cast_sub hq'.le, Nat.cast_one, Int.cast_natAbs]

Result:
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (↑q - 1) ^ φ n < ↑|eval (↑q) (cyclotomic n ℤ)|

Proof state:
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ eval (↑q) (cyclotomic n ℝ) ≤ ↑|eval (↑q) (cyclotomic n ℤ)|

Tactic:
convert (cyclotomic.eval_apply (q : ℤ) n (algebraMap ℤ ℝ)).trans_le (le_abs_self _)

Result:
case h.e'_4
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ ↑|eval (↑q) (cyclotomic n ℤ)| = |(algebraMap ℤ ℝ) (eval (↑q) (cyclotomic n ℤ))|

Proof state:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
⊢ (q - 1) ^ φ n < (eval (↑q) (cyclotomic n ℤ)).natAbs

Tactic:
rcases hq.lt_or_lt.imp_left Nat.lt_one_iff.mp with (rfl | hq')

Result:
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ (0 - 1) ^ φ n < (eval (↑0) (cyclotomic n ℤ)).natAbs

case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (q - 1) ^ φ n < (eval (↑q) (cyclotomic n ℤ)).natAbs

Proof state:
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ (0 - 1) ^ φ n < (eval (↑0) (cyclotomic n ℤ)).natAbs

Tactic:
rw [zero_tsub, zero_pow (Nat.totient_pos.2 (pos_of_gt hn')).ne', pos_iff_ne_zero,
  Int.natAbs_ne_zero, Nat.cast_zero, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hn']

Result:
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ 1 ≠ 0

Proof state:
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (↑q - 1) ^ φ n < ↑|eval (↑q) (cyclotomic n ℤ)|

Tactic:
refine (sub_one_pow_totient_lt_cyclotomic_eval hn' (Nat.one_lt_cast.2 hq')).trans_le ?_

Result:
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ eval (↑q) (cyclotomic n ℝ) ≤ ↑|eval (↑q) (cyclotomic n ℤ)|

Proof state:
case h.e'_4
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ ↑|eval (↑q) (cyclotomic n ℤ)| = |(algebraMap ℤ ℝ) (eval (↑q) (cyclotomic n ℤ))|

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_lt_of_mem_smul (x : E) (ε : ℝ) (hε : 0 < ε) (hs₂ : IsOpen s) (hx : x ∈ ε • s) :
    gauge s x < ε

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen s
hx : x ∈ ε • s
⊢ ε⁻¹ • x ∈ s

Tactic:
rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne']

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : gauge s (ε⁻¹ • x) < 1
⊢ gauge s x < ε

Tactic:
rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff₀ hε, mul_one]
  at h_gauge_lt

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen s
hx : x ∈ ε • s
⊢ gauge s x < ε

Tactic:
have : ε⁻¹ • x ∈ s := by rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne']

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
⊢ gauge s x < ε

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
⊢ gauge s x < ε

Tactic:
have h_gauge_lt := gauge_lt_one_of_mem_of_isOpen hs₂ this

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : gauge s (ε⁻¹ • x) < 1
⊢ gauge s x < ε
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem mem_range_lift_of_card_le {a : Cardinal.{u}} {b : Ordinal.{max u v}}
    (h : card b ≤ Cardinal.lift.{v, u} a) : b ∈ Set.range lift.{v, u}

Proof state:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b.card ≤ Cardinal.lift.{v, u} a
⊢ b ∈ range lift.{v, u}

Tactic:
rw [card_le_iff, ← lift_succ, ← lift_ord] at h

Result:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < lift.{v, u} (succ a).ord
⊢ b ∈ range lift.{v, u}

Proof state:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < lift.{v, u} (succ a).ord
⊢ b ∈ range lift.{v, u}

Tactic:
exact mem_range_lift_of_le h.le

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
lemma ofDigits_inj_of_len_eq {b : ℕ} (hb : 1 < b) {L1 L2 : List ℕ}
    (len : L1.length = L2.length) (w1 : ∀ l ∈ L1, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L1 = ofDigits b L2) : L1 = L2

Proof state:
case cons.intro.intro
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : ofDigits b (D :: L) = ofDigits b (d :: l)
len : L.length = l.length
⊢ D :: L = d :: l

Tactic:
simp only [ofDigits_cons] at h

Result:
case cons.intro.intro
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
⊢ D :: L = d :: l
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasStrictFDerivAt_finset_prod [DecidableEq ι] [Fintype ι] {x : ι → 𝔸'} :
    HasStrictFDerivAt (𝕜 := 𝕜) (∏ i ∈ u, · i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • proj i) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
u : Finset ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ι → 𝔸'
⊢ HasStrictFDerivAt (fun x => ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • proj i) x

Tactic:
simp only [Finset.sum_eq_multiset_sum, Finset.prod_eq_multiset_prod]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
u : Finset ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ι → 𝔸'
⊢ HasStrictFDerivAt (fun x => (Multiset.map x u.val).prod)
    (Multiset.map (fun x_1 => (Multiset.map x (u.erase x_1).val).prod • proj x_1) u.val).sum x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
u : Finset ι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ι → 𝔸'
⊢ HasStrictFDerivAt (fun x => (Multiset.map x u.val).prod)
    (Multiset.map (fun x_1 => (Multiset.map x (u.erase x_1).val).prod • proj x_1) u.val).sum x

Tactic:
exact hasStrictFDerivAt_multiset_prod

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_lemma (s : Finset α) (f : α → β)
    (comm : (s : Set α).Pairwise (Commute on f)) :
    Set.Pairwise { x | x ∈ Multiset.map f s.val } Commute

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
⊢ {x | ∃ a ∈ s.val, f a = x}.Pairwise Commute

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ _

Result:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
a : α
ha : a ∈ s.val
b : α
hb : b ∈ s.val
a✝ : f a ≠ f b
⊢ Commute (f a) (f b)

Proof state:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
a : α
ha : a ∈ s.val
b : α
hb : b ∈ s.val
a✝ : f a ≠ f b
⊢ Commute (f a) (f b)

Tactic:
exact comm.of_refl ha hb

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
⊢ {x | x ∈ Multiset.map f s.val}.Pairwise Commute

Tactic:
simp_rw [Multiset.mem_map]

Result:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
⊢ {x | ∃ a ∈ s.val, f a = x}.Pairwise Commute
-- Mathlib/LinearAlgebra/Dimension/Localization.lean
theorem rank_quotient_add_rank_of_isDomain [IsDomain R] (M' : Submodule R M) :
    Module.rank R (M ⧸ M') + Module.rank R M' = Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
M' : Submodule R M
⊢ Module.rank R (M ⧸ M') + Module.rank R ↥M' = Module.rank R M

Tactic:
apply lift_injective.{max u v}

Result:
case a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
M' : Submodule R M
⊢ lift.{max u v, v} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max u v, v} (Module.rank R M)

Proof state:
case a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
M' : Submodule R M
⊢ lift.{max u v, v} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max u v, v} (Module.rank R M)

Tactic:
rw [lift_add, ← IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (M'.toLocalized R⁰) le_rfl,
  ← IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl,
  ← IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (M'.toLocalizedQuotient R⁰) le_rfl,
  ← lift_add, rank_quotient_add_rank_of_divisionRing]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
    l.idxOf? a = none ↔ a ∉ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (∀ (x : α), x ∈ l → ¬x = a) ↔ ¬a ∈ l

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (∀ (x : α), x ∈ l → ¬x = a) → ¬a ∈ l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ ¬a ∈ l → ∀ (x : α), x ∈ l → ¬x = a

Proof state:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
w : ¬a = a
⊢ False

Tactic:
simp at w

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ ¬a ∈ l → ∀ (x : α), x ∈ l → ¬x = a

Tactic:
rintro w x h rfl

Result:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
x : α
h : x ∈ l
w : ¬x ∈ l
⊢ False

Proof state:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (∀ (x : α), x ∈ l → ¬x = a) → ¬a ∈ l

Tactic:
intro w h

Result:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
w : ∀ (x : α), x ∈ l → ¬x = a
h : a ∈ l
⊢ False

Proof state:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
w : ∀ (x : α), x ∈ l → ¬x = a
h : a ∈ l
⊢ False

Tactic:
specialize w _ h

Result:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
w : ¬a = a
⊢ False

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ idxOf? a l = none ↔ ¬a ∈ l

Tactic:
simp only [idxOf?, findIdx?_eq_none_iff, beq_eq_false_iff_ne, ne_eq]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (∀ (x : α), x ∈ l → ¬x = a) ↔ ¬a ∈ l

Proof state:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
x : α
h : x ∈ l
w : ¬x ∈ l
⊢ False

Tactic:
contradiction

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_sub_right_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.cos (o.oangle y (y - x)) = ‖y‖ / ‖y - x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).cos = ‖y‖ / ‖y - x‖

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).cos = ‖y‖ / ‖y - x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).cos = ‖y‖ / ‖y - x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.cos_angle_sub_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

Tactic:
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i

Proof state:
case a.h
a i : Nat
h : i < a
⊢ ?a.b✝ < a - i

case a.b
a i : Nat
h : i < a
⊢ Nat

Tactic:
apply Nat.zero_lt_sub_of_lt

Result:
case a.h.h
a i : Nat
h : i < a
⊢ i < a

Proof state:
a i : Nat
h : i < a
⊢ a - (i + 1) < a - i

Tactic:
rw [Nat.add_succ, Nat.sub_succ]

Result:
a i : Nat
h : i < a
⊢ (a - i).pred < a - i

Proof state:
a i : Nat
h : i < a
⊢ (a - i).pred < a - i

Tactic:
apply Nat.pred_lt

Result:
case a
a i : Nat
h : i < a
⊢ a - i ≠ 0

Proof state:
case a
a i : Nat
h : i < a
⊢ a - i ≠ 0

Tactic:
apply Nat.not_eq_zero_of_lt

Result:
case a.h
a i : Nat
h : i < a
⊢ ?a.b✝ < a - i

case a.b
a i : Nat
h : i < a
⊢ Nat

Proof state:
case a.h.h
a i : Nat
h : i < a
⊢ i < a

Tactic:
assumption

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem lxor_bit (a m b n) : Int.xor (bit a m) (bit b n) = bit (xor a b) (Int.xor m n)

Proof state:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).xor (bit b n) = bit (a ^^ b) (m.xor n)

Tactic:
rw [← bitwise_xor, bitwise_bit]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Bool.lean
theorem Bool.and_right (lhs rhs : Bool) (h : (lhs && rhs) = true) : rhs = true

Proof state:
⊢ ∀ (lhs rhs : Bool), (lhs && rhs) = true → rhs = true

Tactic:
decide

Result:
no goals

Proof state:
lhs rhs : Bool
h : (lhs && rhs) = true
⊢ rhs = true

Tactic:
revert lhs rhs

Result:
⊢ ∀ (lhs rhs : Bool), (lhs && rhs) = true → rhs = true
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_unitOfList
    {l : List α} {k : α} {fallback : Unit} :
    getD (unitOfList l) k fallback = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
l : List α
k : α
fallback : Unit
⊢ getD (unitOfList l) k fallback = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
lemma cos_half {x : ℝ} (hl : -π ≤ x) (hr : x ≤ π) : cos (x / 2) = sqrt ((1 + cos x) / 2)

Proof state:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ x / 2 ∈ Icc (-(π / 2)) (π / 2)

Tactic:
constructor <;> linarith

Result:
no goals

Proof state:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
this : 0 ≤ cos (x / 2)
⊢ cos (x / 2) = √((1 + cos x) / 2)

Tactic:
rw [← sqrt_sq this, cos_sq, add_div, two_mul, add_halves]

Result:
no goals

Proof state:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ cos (x / 2) = √((1 + cos x) / 2)

Tactic:
have : 0 ≤ cos (x / 2) := cos_nonneg_of_mem_Icc <| by constructor <;> linarith

Result:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
this : 0 ≤ cos (x / 2)
⊢ cos (x / 2) = √((1 + cos x) / 2)
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isLittleO_smoothingFn_one : ε =o[atTop] (fun _ => (1 : ℝ))

Proof state:
⊢ (fun n => 1 / log n) =o[atTop] fun x => 1

Tactic:
refine isLittleO_of_tendsto (fun _ h => False.elim <| one_ne_zero h) ?_

Result:
⊢ Tendsto (fun x => 1 / log x / 1) atTop (𝓝 0)

Proof state:
⊢ Tendsto (fun x => 1 / log x / 1) atTop (𝓝 0)

Tactic:
simp only [one_div, div_one]

Result:
⊢ Tendsto (fun x => (log x)⁻¹) atTop (𝓝 0)

Proof state:
⊢ ε =o[atTop] fun x => 1

Tactic:
unfold smoothingFn

Result:
⊢ (fun n => 1 / log n) =o[atTop] fun x => 1

Proof state:
⊢ Tendsto (fun x => (log x)⁻¹) atTop (𝓝 0)

Tactic:
exact Tendsto.inv_tendsto_atTop Real.tendsto_log_atTop

Result:
no goals
-- Mathlib/CategoryTheory/ObjectProperty/EpiMono.lean
lemma prop_X₃_of_shortExact [HasZeroMorphisms C] {S : ShortComplex C} (hS : S.ShortExact)
    (h₂ : P S.X₂) : P S.X₃

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderQuotients
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
⊢ P S.X₃

Tactic:
have := hS.epi_g

Result:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderQuotients
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
this : Epi S.g
⊢ P S.X₃

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderQuotients
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
this : Epi S.g
⊢ P S.X₃

Tactic:
exact P.prop_of_epi S.g h₂

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma tendsto_integral_density_of_antitone (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α)
    (seq : ℕ → Set β) (hseq : Antitone seq) (hseq_iInter : ⋂ i, seq i = ∅)
    (hseq_meas : ∀ m, MeasurableSet (seq m)) :
    Tendsto (fun m ↦ ∫ x, density κ ν a x (seq m) ∂(ν a)) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto (fun m => ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 0)

Tactic:
simp_rw [integral_density hκν a (hseq_meas _)]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto (fun m => ((κ a) (univ ×ˢ seq m)).toReal) atTop (𝓝 0)

Proof state:
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ ∀ (i : ℕ), NullMeasurableSet (univ ×ˢ seq i) (κ a)

Tactic:
measurability

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem cmp_compares : ∀ a b : NONote, (cmp a b).Compares a b
  | ⟨a, ha⟩, ⟨b, hb⟩ => by
    dsimp [cmp]
    have := ONote.cmp_compares a b
    cases h : ONote.cmp a b <;> simp only [h] at this <;> try exact this
    exact Subtype.mk_eq_mk.2 this

Proof state:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
⊢ (a.cmp b).Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
have := ONote.cmp_compares a b

Result:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
⊢ (a.cmp b).Compares ⟨a, ha⟩ ⟨b, hb⟩

Proof state:
case gt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.gt
this : Ordering.gt.Compares a b
⊢ Ordering.gt.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
exact this

Result:
no goals

Proof state:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
⊢ (cmp ⟨a, ha⟩ ⟨b, hb⟩).Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
dsimp [cmp]

Result:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
⊢ (a.cmp b).Compares ⟨a, ha⟩ ⟨b, hb⟩

Proof state:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
⊢ (a.cmp b).Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
cases h : ONote.cmp a b <;> simp only [h] at this <;> try exact this

Result:
case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩

Proof state:
case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
exact Subtype.mk_eq_mk.2 this

Result:
no goals
-- Mathlib/Topology/SeparatedMap.lean
theorem isSeparatedMap_iff_isClosedEmbedding {f : X → Y} :
    IsSeparatedMap f ↔ IsClosedEmbedding (toPullbackDiag f)

Proof state:
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsSeparatedMap f ↔ IsClosedEmbedding (toPullbackDiag f)

Tactic:
rw [isSeparatedMap_iff_isClosed_diagonal, ← range_toPullbackDiag]

Result:
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsClosed (Set.range (toPullbackDiag f)) ↔ IsClosedEmbedding (toPullbackDiag f)

Proof state:
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsClosed (Set.range (toPullbackDiag f)) ↔ IsClosedEmbedding (toPullbackDiag f)

Tactic:
exact ⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isClosed_range⟩

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coeff_zero_of_lt_valuation {n D : ℤ} {f : K⸨X⸩}
    (H : Valued.v f ≤ Multiplicative.ofAdd (-D)) : n < D → f.coeff n = 0

Proof state:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
⊢ n < D → f.coeff n = 0

Tactic:
intro hnd

Result:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
⊢ f.coeff n = 0