harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/ExtremallyDisconnected.lean
/-- Lemma 2.4 in [Gleason, *Projective topological spaces*][gleason1958]:
a continuous surjection $\pi$ from a compact space $D$ to a Fréchet space $A$ restricts to
a compact subset $E$ of $D$, such that $\pi$ maps $E$ onto $A$ and satisfies the
"Zorn subset condition", where $\pi(E_0) \ne A$ for any proper closed subset $E_0 \subsetneq E$. -/
lemma exists_compact_surjective_zorn_subset [T1Space A] [CompactSpace D] {π : D → A}
    (π_cont : Continuous π) (π_surj : π.Surjective) : ∃ E : Set D, CompactSpace E ∧ π '' E = univ ∧
    ∀ E₀ : Set E, E₀ ≠ univ → IsClosed E₀ → E.restrict π '' E₀ ≠ univ

Proof state:
case intro.intro
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ C ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x => x ∈ S) E
E_closed : IsClosed E
E_surj : π '' E = univ
⊢ ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π '' E₀ ≠ univ

Tactic:
intro E₀ E₀_min E₀_closed

Result:
case intro.intro
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
this : ∀ C ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
E : Set D
E_min : Minimal (fun x => x ∈ S) E
E_closed : IsClosed E
E_surj : π '' E = univ
E₀ : Set ↑E
E₀_min : E₀ ≠ univ
E₀_closed : IsClosed E₀
⊢ E.restrict π '' E₀ ≠ univ

Proof state:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 => x1 ⊆ x2) C
⊢ ∃ s ∈ S, ∀ c ∈ C, s ⊆ c

Tactic:
refine ⟨iInter (fun c : C => c), ⟨isClosed_iInter fun ⟨_, h⟩ => (C_sub h).left, ?_⟩,
  fun c hc _ h => mem_iInter.mp h ⟨c, hc⟩⟩

Result:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 => x1 ⊆ x2) C
⊢ π '' ⋂ c, ↑c = univ

Proof state:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
⊢ ∀ C ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c

Tactic:
intro C C_sub C_chain

Result:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
π : D → A
π_cont : Continuous π
π_surj : Surjective π
S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
C_chain : IsChain (fun x1 x2 => x1 ⊆ x2) C
⊢ ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
-- Mathlib/Data/Nat/Totient.lean
theorem totient_eq_card_lt_and_coprime (n : ℕ) : φ n = Nat.card { m | m < n ∧ n.Coprime m }

Proof state:
n : ℕ
e : ↑{m | m < n ∧ n.Coprime m} ≃ { x // x ∈ filter (fun x => n.Coprime x) (range n) } :=
  { toFun := fun m => ⟨↑m, ⋯⟩, invFun := fun m => ⟨↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}

Tactic:
rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]

Result:
no goals

Proof state:
n : ℕ
m : ↑{m | m < n ∧ n.Coprime m}
⊢ (fun m => ⟨↑m, ⋯⟩) ((fun m => ⟨↑m, ⋯⟩) m) = m

Tactic:
simp only [Subtype.coe_mk, Subtype.coe_eta]

Result:
no goals

Proof state:
n : ℕ
m : { x // x ∈ filter (fun x => n.Coprime x) (range n) }
⊢ ↑m ∈ {m | m < n ∧ n.Coprime m}

Tactic:
simpa only [Finset.mem_filter, Finset.mem_range] using m.property

Result:
no goals

Proof state:
n : ℕ
m : { x // x ∈ filter (fun x => n.Coprime x) (range n) }
⊢ (fun m => ⟨↑m, ⋯⟩) ((fun m => ⟨↑m, ⋯⟩) m) = m

Tactic:
simp only [Subtype.coe_mk, Subtype.coe_eta]

Result:
no goals

Proof state:
n : ℕ
m : ↑{m | m < n ∧ n.Coprime m}
⊢ ↑m ∈ filter (fun x => n.Coprime x) (range n)

Tactic:
simpa only [Finset.mem_filter, Finset.mem_range] using m.property

Result:
no goals

Proof state:
n : ℕ
⊢ φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}

Tactic:
let e : { m | m < n ∧ n.Coprime m } ≃ {x ∈ range n | n.Coprime x} :=
  { toFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
    invFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
    left_inv := fun m => by simp only [Subtype.coe_mk, Subtype.coe_eta]
    right_inv := fun m => by simp only [Subtype.coe_mk, Subtype.coe_eta] }

Result:
n : ℕ
e : ↑{m | m < n ∧ n.Coprime m} ≃ { x // x ∈ filter (fun x => n.Coprime x) (range n) } :=
  { toFun := fun m => ⟨↑m, ⋯⟩, invFun := fun m => ⟨↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}
-- Mathlib/Data/List/Basic.lean
lemma filter_comm (q) (l : List α) : filter p (filter q l) = filter q (filter p l)

Proof state:
α : Type u
p q : α → Bool
l : List α
⊢ filter p (filter q l) = filter q (filter p l)

Tactic:
simp [Bool.and_comm]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem wellFoundedOn_sdiff_singleton : WellFoundedOn (s \ {a}) r ↔ WellFoundedOn s r

Proof state:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
a : α
⊢ (s \ {a}).WellFoundedOn r ↔ s.WellFoundedOn r

Tactic:
simp only [← wellFoundedOn_insert (a := a), insert_diff_singleton, mem_insert_iff, true_or,
  insert_eq_of_mem]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem condition (b) : K.ι (J.fst b) ≫ I.fst b = K.ι (J.snd b) ≫ I.snd b

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.ι (J.fst b) ≫ I.fst b = K.ι (J.snd b) ≫ I.snd b

Tactic:
rw [← app_right_eq_ι_comp_fst, ← app_right_eq_ι_comp_snd]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem ideal_isMaximal_iff (I : Ideal C(X, 𝕜)) [hI : IsClosed (I : Set C(X, 𝕜))] :
    I.IsMaximal ↔ ∃ x : X, idealOfSet 𝕜 {x}ᶜ = I

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
⊢ I.IsMaximal ↔ ∃ x, idealOfSet 𝕜 {x}ᶜ = I

Tactic:
refine
  ⟨?_, fun h =>
    let ⟨x, hx⟩ := h
    hx ▸ idealOf_compl_singleton_isMaximal 𝕜 x⟩

Result:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
⊢ I.IsMaximal → ∃ x, idealOfSet 𝕜 {x}ᶜ = I

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
hI' : I.IsMaximal
⊢ ∃ x, idealOfSet 𝕜 {x}ᶜ = I

Tactic:
obtain ⟨x, hx⟩ := setOfIdeal_eq_compl_singleton I

Result:
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
hI' : I.IsMaximal
x : X
hx : setOfIdeal I = {x}ᶜ
⊢ ∃ x, idealOfSet 𝕜 {x}ᶜ = I

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
⊢ I.IsMaximal → ∃ x, idealOfSet 𝕜 {x}ᶜ = I

Tactic:
intro hI'

Result:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
hI' : I.IsMaximal
⊢ ∃ x, idealOfSet 𝕜 {x}ᶜ = I

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
hI' : I.IsMaximal
x : X
hx : setOfIdeal I = {x}ᶜ
⊢ idealOfSet 𝕜 {x}ᶜ = I

Tactic:
simpa only [idealOfSet_ofIdeal_eq_closure, I.closure_eq_of_isClosed hI] using
  congr_arg (idealOfSet 𝕜) hx.symm

Result:
no goals

Proof state:
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : IsClosed ↑I
hI' : I.IsMaximal
x : X
hx : setOfIdeal I = {x}ᶜ
⊢ ∃ x, idealOfSet 𝕜 {x}ᶜ = I

Tactic:
exact
  ⟨x, by
    simpa only [idealOfSet_ofIdeal_eq_closure, I.closure_eq_of_isClosed hI] using
      congr_arg (idealOfSet 𝕜) hx.symm⟩

Result:
no goals
-- Mathlib/Probability/Variance.lean
theorem evariance_lt_top [IsFiniteMeasure μ] (hX : MemLp X 2 μ) : evariance X μ < ∞

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] < ⊤

Tactic:
have := ENNReal.pow_lt_top (hX.sub <| memLp_const <| μ[X]).2 2

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : eLpNorm (X - fun x => ∫ (x : Ω), X x ∂μ) 2 μ ^ 2 < ⊤
⊢ eVar[X; μ] < ⊤

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2 < ⊤
⊢ eVar[X; μ] < ⊤

Tactic:
rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_one] at this

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ < ⊤
⊢ eVar[X; μ] < ⊤

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ((∫⁻ (x : Ω), ‖(X - fun x => ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2)) ^ 2 < ⊤
⊢ eVar[X; μ] < ⊤

Tactic:
simp only [ENNReal.toReal_ofNat, Pi.sub_apply, ENNReal.one_toReal, one_div] at this

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2 < ⊤
⊢ eVar[X; μ] < ⊤

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ < ⊤
⊢ eVar[X; μ] < ⊤

Tactic:
exact this

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : eLpNorm (X - fun x => ∫ (x : Ω), X x ∂μ) 2 μ ^ 2 < ⊤
⊢ eVar[X; μ] < ⊤

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm two_ne_zero ENNReal.ofNat_ne_top, ← ENNReal.rpow_two] at this

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ((∫⁻ (x : Ω), ‖(X - fun x => ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2)) ^ 2 < ⊤
⊢ eVar[X; μ] < ⊤
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem two_mul_le_exp {x : ℝ} : 2 * x ≤ exp x

Proof state:
x : ℝ
hx0 : ¬x < 0
this : 1 + 1 ≤ rexp 1
⊢ 2 ≤ rexp 1

Tactic:
rwa [one_add_one_eq_two] at this

Result:
no goals

Proof state:
x : ℝ
hx0 : ¬x < 0
⊢ 2 ≤ rexp 1

Tactic:
have := Real.add_one_le_exp 1

Result:
x : ℝ
hx0 : ¬x < 0
this : 1 + 1 ≤ rexp 1
⊢ 2 ≤ rexp 1

Proof state:
case neg
x : ℝ
hx0 : ¬x < 0
⊢ 2 * x ≤ rexp x

Tactic:
apply le_trans (mul_le_mul_of_nonneg_right _ (le_of_not_lt hx0)) exp_one_mul_le_exp

Result:
x : ℝ
hx0 : ¬x < 0
⊢ 2 ≤ rexp 1

Proof state:
case pos
x : ℝ
hx0 : x < 0
⊢ 2 * x ≤ rexp x

Tactic:
exact le_trans (mul_nonpos_of_nonneg_of_nonpos (by simp only [Nat.ofNat_nonneg]) hx0.le)
  (exp_nonneg x)

Result:
no goals

Proof state:
x : ℝ
⊢ 2 * x ≤ rexp x

Tactic:
by_cases hx0 : x < 0

Result:
case pos
x : ℝ
hx0 : x < 0
⊢ 2 * x ≤ rexp x

case neg
x : ℝ
hx0 : ¬x < 0
⊢ 2 * x ≤ rexp x

Proof state:
x : ℝ
hx0 : x < 0
⊢ 0 ≤ 2

Tactic:
simp only [Nat.ofNat_nonneg]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Basic.lean
theorem map_natCast' {A} [AddMonoidWithOne A] [FunLike F A B] [AddMonoidHomClass F A B]
    (f : F) (h : f 1 = 1) :
    ∀ n : ℕ, f n = n :=
  eq_natCast' ((f : A →+ B).comp <| Nat.castAddMonoidHom _) (by simpa)

Proof state:
B : Type u_4
F : Type u_5
inst✝³ : AddMonoidWithOne B
A : Type u_6
inst✝² : AddMonoidWithOne A
inst✝¹ : FunLike F A B
inst✝ : AddMonoidHomClass F A B
f : F
h : f 1 = 1
⊢ ((↑f).comp (Nat.castAddMonoidHom A)) 1 = 1

Tactic:
simpa

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
theorem differentiableAt_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) :
    DifferentiableAt ℂ jacobiTheta τ

Proof state:
τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ jacobiTheta τ

Tactic:
simp_rw [funext jacobiTheta_eq_jacobiTheta₂]

Result:
τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ (jacobiTheta₂ 0) τ

Proof state:
τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ (jacobiTheta₂ 0) τ

Tactic:
exact differentiableAt_jacobiTheta₂_snd 0 hτ

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem orderTop_sub {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R}
    (hxy : x.orderTop < y.orderTop) : (x - y).orderTop = x.orderTop

Proof state:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).orderTop = x.orderTop

Tactic:
exact orderTop_add_eq_left hxy

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
⊢ (x - y).orderTop = x.orderTop

Tactic:
rw [sub_eq_add_neg]

Result:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
⊢ (x + -y).orderTop = x.orderTop

Proof state:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
⊢ (x + -y).orderTop = x.orderTop

Tactic:
rw [← orderTop_neg (x := y)] at hxy

Result:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).orderTop = x.orderTop
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Icc (x y : ℝ) : Real.toEReal ⁻¹' Icc x y = Icc x y

Proof state:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iic ↑y) = Ici x ∩ Iic y

Tactic:
simp

Result:
no goals

Proof state:
x y : ℝ
⊢ Real.toEReal ⁻¹' Icc ↑x ↑y = Icc x y

Tactic:
simp_rw [← Ici_inter_Iic]

Result:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iic ↑y) = Ici x ∩ Iic y
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem Nonempty.eq_univ [Subsingleton α] : s.Nonempty → s = univ

Proof state:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
⊢ s.Nonempty → s = univ

Tactic:
rintro ⟨x, hx⟩

Result:
case intro
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ

Proof state:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ y ∈ s

Tactic:
rwa [Subsingleton.elim y x]

Result:
no goals

Proof state:
case intro
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ

Tactic:
exact eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem leftpad_eq_leftpadTR : @leftpad = @leftpadTR

Proof state:
⊢ @leftpad = @leftpadTR

Tactic:
repeat (apply funext; intro)

Result:
case h.h.h.h
x✝³ : Type u_1
x✝² : Nat
x✝¹ : x✝³
x✝ : List x✝³
⊢ leftpad x✝² x✝¹ x✝ = leftpadTR x✝² x✝¹ x✝

Proof state:
case h.h.h.h
x✝² : Type u_1
x✝¹ : Nat
x✝ : x✝²
⊢ ∀ (x : List x✝²), leftpad x✝¹ x✝ x = leftpadTR x✝¹ x✝ x

Tactic:
intro

Result:
case h.h.h.h
x✝³ : Type u_1
x✝² : Nat
x✝¹ : x✝³
x✝ : List x✝³
⊢ leftpad x✝² x✝¹ x✝ = leftpadTR x✝² x✝¹ x✝

Proof state:
case h.h.h
x✝² : Type u_1
x✝¹ : Nat
x✝ : x✝²
⊢ leftpad x✝¹ x✝ = leftpadTR x✝¹ x✝

Tactic:
apply funext

Result:
case h.h.h.h
x✝² : Type u_1
x✝¹ : Nat
x✝ : x✝²
⊢ ∀ (x : List x✝²), leftpad x✝¹ x✝ x = leftpadTR x✝¹ x✝ x

Proof state:
case h.h.h.h
x✝³ : Type u_1
x✝² : Nat
x✝¹ : x✝³
x✝ : List x✝³
⊢ leftpad x✝² x✝¹ x✝ = leftpadTR x✝² x✝¹ x✝

Tactic:
simp [leftpad, leftpadTR, replicateTR_loop_eq]

Result:
no goals

Proof state:
case h.h.h
x✝² : Type u_1
x✝¹ : Nat
x✝ : x✝²
⊢ leftpad x✝¹ x✝ = leftpadTR x✝¹ x✝

Tactic:
(apply funext; intro)

Result:
case h.h.h.h
x✝³ : Type u_1
x✝² : Nat
x✝¹ : x✝³
x✝ : List x✝³
⊢ leftpad x✝² x✝¹ x✝ = leftpadTR x✝² x✝¹ x✝
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem mem_periodicOrbit_iff (hx : x ∈ periodicPts f) :
    y ∈ periodicOrbit f x ↔ ∃ n, f^[n] x = y

Proof state:
α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
⊢ (∃ a < minimalPeriod f x, f^[a] x = y) ↔ ∃ n, f^[n] x = y

Tactic:
use fun ⟨a, _, ha'⟩ => ⟨a, ha'⟩

Result:
case mpr
α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
⊢ (∃ n, f^[n] x = y) → ∃ a < minimalPeriod f x, f^[a] x = y

Proof state:
case mpr.intro
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ ∃ a < minimalPeriod f x, f^[a] x = f^[n] x

Tactic:
use n % minimalPeriod f x, mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx)

Result:
case right
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n % minimalPeriod f x] x = f^[n] x

Proof state:
α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
⊢ y ∈ periodicOrbit f x ↔ ∃ n, f^[n] x = y

Tactic:
simp only [periodicOrbit, Cycle.mem_coe_iff, List.mem_map, List.mem_range]

Result:
α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
⊢ (∃ a < minimalPeriod f x, f^[a] x = y) ↔ ∃ n, f^[n] x = y

Proof state:
case mpr
α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
⊢ (∃ n, f^[n] x = y) → ∃ a < minimalPeriod f x, f^[a] x = y

Tactic:
rintro ⟨n, rfl⟩

Result:
case mpr.intro
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ ∃ a < minimalPeriod f x, f^[a] x = f^[n] x

Proof state:
case right
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n % minimalPeriod f x] x = f^[n] x

Tactic:
rw [iterate_mod_minimalPeriod_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem isOrtho_flip {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M} {x y} : B.IsOrtho x y ↔ B.flip.IsOrtho y x

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
x y : M₁
⊢ B.IsOrtho x y ↔ B.flip.IsOrtho y x

Tactic:
simp_rw [isOrtho_def, flip_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem trinomial_middle_coeff (hkm : k < m) (hmn : m < n) :
    (trinomial k m n u v w).coeff m = v

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (trinomial k m n u v w).coeff m = v

Tactic:
rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
  if_neg hkm.ne', if_pos rfl, if_neg hmn.ne, zero_add, add_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_le_one {x : ℝ≥0∞} {z : ℝ} (hx : x ≤ 1) (hz : 0 ≤ z) : x ^ z ≤ 1

Proof state:
case intro
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : x ≤ 1
⊢ ↑x ^ z ≤ 1

Tactic:
simp [← coe_rpow_of_nonneg _ hz, NNReal.rpow_le_one hx hz]

Result:
no goals

Proof state:
case intro
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : ↑x ≤ 1
⊢ ↑x ^ z ≤ 1

Tactic:
simp only [coe_le_one_iff] at hx

Result:
case intro
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : x ≤ 1
⊢ ↑x ^ z ≤ 1

Proof state:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx coe_lt_top)

Result:
case intro
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : ↑x ≤ 1
⊢ ↑x ^ z ≤ 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_sub_sub_add_right (n m k l : Nat) :
    (n + l) - m - (k + l) = n - m - k

Proof state:
n m k l : Nat
⊢ n + l - m - (k + l) = n - m - k

Tactic:
rw [Nat.sub_sub, Nat.sub_sub, ←Nat.add_assoc, Nat.add_sub_add_right]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
/-- If `F` is full, and naturally isomorphic to some `F'`, then `F'` is also full. -/
lemma Full.of_iso [Full F] (α : F ≅ F') : Full F' where
  map_surjective {X Y} f :=
    ⟨F.preimage ((α.app X).hom ≫ f ≫ (α.app Y).inv), by simp [← NatIso.naturality_1 α]⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F F' : C ⥤ D
inst✝ : F.Full
α : F ≅ F'
X Y : C
f : F'.obj X ⟶ F'.obj Y
⊢ F'.map (F.preimage ((α.app X).hom ≫ f ≫ (α.app Y).inv)) = f

Tactic:
simp [← NatIso.naturality_1 α]

Result:
no goals
-- Mathlib/Analysis/Calculus/FirstDerivativeTest.lean
/-- The First-Derivative Test from calculus, minima version. -/
lemma isLocalMin_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ}
    (g₀ : a < b) (g₁ : b < c) (h : ContinuousAt f b)
    (hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
    (h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0)
    (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) : IsLocalMin f b

Proof state:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : b < c
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ IsLocalMin f b

Tactic:
have := isLocalMax_of_deriv_Ioo (f := -f) g₀ g₁
  (by simp_all) hd₀.neg hd₁.neg
  (fun x hx => deriv.neg (f := f) ▸ Left.nonneg_neg_iff.mpr <|h₀ x hx)
  (fun x hx => deriv.neg (f := f) ▸ Left.neg_nonpos_iff.mpr <|h₁ x hx)

Result:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : b < c
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
this : IsLocalMax (-f) b
⊢ IsLocalMin f b

Proof state:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : b < c
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
this : IsLocalMax (-f) b
⊢ IsLocalMin f b

Tactic:
exact (neg_neg f) ▸ IsLocalMax.neg this

Result:
no goals

Proof state:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : b < c
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ ContinuousAt (-f) b

Tactic:
simp_all

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Continuum.lean
theorem lift_continuum : lift.{v} 𝔠 = 𝔠

Proof state:
⊢ lift.{v, u_1} 𝔠 = 𝔠

Tactic:
rw [← two_power_aleph0, lift_two_power, lift_aleph0, two_power_aleph0]

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
theorem coe_piFinset (t : ∀ a, Finset (δ a)) :
    (piFinset t : Set (∀ a, δ a)) = Set.pi Set.univ fun a => t a :=
  Set.ext fun x => by
    rw [Set.mem_univ_pi]
    exact Fintype.mem_piFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)

Tactic:
exact Fintype.mem_piFinset

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ x ∈ Set.univ.pi fun a => ↑(t a)

Tactic:
rw [Set.mem_univ_pi]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)
-- Mathlib/ModelTheory/Complexity.lean
theorem not_all_isQF (φ : L.BoundedFormula α (n + 1)) : ¬φ.all.IsQF := fun con => by
  obtain - | con := con
  exact φ.not_all_isAtomic con

Proof state:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀'φ).IsQF
⊢ False

Tactic:
obtain - | con := con

Result:
case of_isAtomic
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀'φ).IsAtomic
⊢ False

Proof state:
case of_isAtomic
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀'φ).IsAtomic
⊢ False

Tactic:
exact φ.not_all_isAtomic con

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem associator_inv_naturality_right (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
    f ◁ g ◁ η ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η

Tactic:
simp

Result:
no goals