harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/Quotient.lean
theorem stabilizer_quotient {G} [Group G] (H : Subgroup G) :
    MulAction.stabilizer G ((1 : G) : G ⧸ H) = H

Proof state:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : G
⊢ x✝ ∈ stabilizer G ↑1 ↔ x✝ ∈ H

Tactic:
simp [QuotientGroup.eq]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ stabilizer G ↑1 = H

Tactic:
ext

Result:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : G
⊢ x✝ ∈ stabilizer G ↑1 ↔ x✝ ∈ H
-- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
theorem evenOdd_isCompl : IsCompl (evenOdd Q 0) (evenOdd Q 1) :=
  (DirectSum.Decomposition.isInternal (evenOdd Q)).isCompl zero_ne_one <| by
    have : (Finset.univ : Finset (ZMod 2)) = {0, 1} := rfl
    simpa using congr_arg ((↑) : Finset (ZMod 2) → Set (ZMod 2)) this

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Set.univ = {0, 1}

Tactic:
have : (Finset.univ : Finset (ZMod 2)) = {0, 1} := rfl

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
this : Finset.univ = {0, 1}
⊢ Set.univ = {0, 1}

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
this : Finset.univ = {0, 1}
⊢ Set.univ = {0, 1}

Tactic:
simpa using congr_arg ((↑) : Finset (ZMod 2) → Set (ZMod 2)) this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_append_right {l₁ : Array α} l₂ (h : ∀ b ∈ l₁, ¬p b) :
    (l₁ ++ l₂).eraseP p = l₁ ++ l₂.eraseP p

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
l₁ : List α
h : ∀ (b : α), b ∈ { toList := l₁ } → ¬p b = true
l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).eraseP p = { toList := l₁ } ++ { toList := l₂ }.eraseP p

Tactic:
simpa using List.eraseP_append_right l₂ (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ : List α
h : ∀ (b : α), b ∈ { toList := l₁ } → ¬p b = true
l₂ : List α
⊢ ∀ (b : α), b ∈ l₁ → ¬p b = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : Array α
h : ∀ (b : α), b ∈ l₁ → ¬p b = true
⊢ (l₁ ++ l₂).eraseP p = l₁ ++ l₂.eraseP p

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
l₁ : List α
h : ∀ (b : α), b ∈ { toList := l₁ } → ¬p b = true
⊢ ({ toList := l₁ } ++ l₂).eraseP p = { toList := l₁ } ++ l₂.eraseP p

Proof state:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
l₁ : List α
h : ∀ (b : α), b ∈ { toList := l₁ } → ¬p b = true
⊢ ({ toList := l₁ } ++ l₂).eraseP p = { toList := l₁ } ++ l₂.eraseP p

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
p : α → Bool
l₁ : List α
h : ∀ (b : α), b ∈ { toList := l₁ } → ¬p b = true
l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).eraseP p = { toList := l₁ } ++ { toList := l₂ }.eraseP p
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_congr {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β}
    (h : ∀ᶠ a in f, u a = v a) : limsup u f = limsup v f

Proof state:
β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
x : α
hx : u x = v x
⊢ u x ≤ b ↔ v x ∈ {x | (fun n => n ≤ b) x}

Tactic:
simp [hx]

Result:
no goals

Proof state:
case e_a.h
β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
⊢ b ∈ {a | ∀ᶠ (n : α) in f, u n ≤ a} ↔ b ∈ {a | ∀ᶠ (n : β) in map v f, n ≤ a}

Tactic:
exact eventually_congr (h.mono fun x hx => by simp [hx])

Result:
no goals

Proof state:
β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ limsup u f = limsup v f

Tactic:
rw [limsup_eq]

Result:
β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f

Proof state:
β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f

Tactic:
congr with b

Result:
case e_a.h
β : Type u_2
α : Type u_6
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
⊢ b ∈ {a | ∀ᶠ (n : α) in f, u n ≤ a} ↔ b ∈ {a | ∀ᶠ (n : β) in map v f, n ≤ a}
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem sqLe_add {c d x y z w : ℕ} (xy : SqLe x c y d) (zw : SqLe z c w d) :
    SqLe (x + z) c (y + w) d

Proof state:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
xz : c * (x * z) ≤ d * (y * w)
⊢ SqLe (x + z) c (y + w) d

Tactic:
simp? [SqLe, mul_assoc] at xy zw says simp only [SqLe, mul_assoc] at xy zw

Result:
c d x y z w : ℕ
xz : c * (x * z) ≤ d * (y * w)
xy : c * (x * x) ≤ d * (y * y)
zw : c * (z * z) ≤ d * (w * w)
⊢ SqLe (x + z) c (y + w) d

Proof state:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ SqLe (x + z) c (y + w) d

Tactic:
have xz := sqLe_add_mixed xy zw

Result:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
xz : c * (x * z) ≤ d * (y * w)
⊢ SqLe (x + z) c (y + w) d

Proof state:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
xz : c * (x * z) ≤ d * (y * w)
⊢ SqLe (x + z) c (y + w) d

Tactic:
simp only [SqLe, mul_assoc] at xy zw

Result:
c d x y z w : ℕ
xz : c * (x * z) ≤ d * (y * w)
xy : c * (x * x) ≤ d * (y * y)
zw : c * (z * z) ≤ d * (w * w)
⊢ SqLe (x + z) c (y + w) d

Proof state:
c d x y z w : ℕ
xz : c * (x * z) ≤ d * (y * w)
xy : c * (x * x) ≤ d * (y * y)
zw : c * (z * z) ≤ d * (w * w)
⊢ SqLe (x + z) c (y + w) d

Tactic:
simp [SqLe, mul_add, mul_comm, mul_left_comm, add_le_add, *]

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
/-- A small family of games is bounded below. -/
lemma bddBelow_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Game.{u}) :
    BddBelow (Set.range f)

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Game
⊢ BddBelow (Set.range f)

Tactic:
obtain ⟨x, hx⟩ := PGame.bddBelow_range_of_small (Quotient.out ∘ f)

Result:
case intro
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Game
x : PGame
hx : x ∈ lowerBounds (Set.range (Quotient.out ∘ f))
⊢ BddBelow (Set.range f)

Proof state:
case intro
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Game
x : PGame
hx : x ∈ lowerBounds (Set.range (Quotient.out ∘ f))
⊢ BddBelow (Set.range f)

Tactic:
refine ⟨⟦x⟧, Set.forall_mem_range.2 fun i ↦ ?_⟩

Result:
case intro
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Game
x : PGame
hx : x ∈ lowerBounds (Set.range (Quotient.out ∘ f))
i : ι
⊢ ⟦x⟧ ≤ f i

Proof state:
case intro
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Game
x : PGame
hx : x ∈ lowerBounds (Set.range (Quotient.out ∘ f))
i : ι
⊢ ⟦x⟧ ≤ f i

Tactic:
simpa [PGame.le_iff_game_le] using hx <| Set.mem_range_self i

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem card_interedges_finpartition_right [DecidableEq β] (s : Finset α) (P : Finpartition t) :
    #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)

Tactic:
simp_rw [← P.biUnion_parts, interedges_biUnion_right, id]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(P.parts.biUnion fun b => interedges r s b) = ∑ b ∈ P.parts, #(interedges r s b)

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)

Tactic:
classical
simp_rw [← P.biUnion_parts, interedges_biUnion_right, id]
rw [card_biUnion]
exact fun x hx y hy h ↦ interedges_disjoint_right r _ (P.disjoint hx hy h)

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(P.parts.biUnion fun b => interedges r s b) = ∑ b ∈ P.parts, #(interedges r s b)

Tactic:
rw [card_biUnion]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ ∀ x ∈ P.parts, ∀ y ∈ P.parts, x ≠ y → Disjoint (interedges r s x) (interedges r s y)

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ ∀ x ∈ P.parts, ∀ y ∈ P.parts, x ≠ y → Disjoint (interedges r s x) (interedges r s y)

Tactic:
exact fun x hx y hy h ↦ interedges_disjoint_right r _ (P.disjoint hx hy h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
    k ∈ m.insertIfNew k v

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
v : β k
⊢ k ∈ m.insertIfNew k v

Tactic:
simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem HasDerivAt.le_of_lipschitz {f : 𝕜 → F} {f' : F} {x₀ : 𝕜} (hf : HasDerivAt f f' x₀)
    {C : ℝ≥0} (hlip : LipschitzWith C f) : ‖f'‖ ≤ C

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x₀ : 𝕜
hf : HasDerivAt f f' x₀
C : ℝ≥0
hlip : LipschitzWith C f
⊢ ‖f'‖ ≤ ↑C

Tactic:
simpa using HasFDerivAt.le_of_lipschitz hf.hasFDerivAt hlip

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem getLast?_enumFrom (n : Nat) (l : List α) :
    (enumFrom n l).getLast? = l.getLast?.map fun a => (n + l.length - 1, a)

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ Option.map (fun a => (n + (l.length - 1), a)) l[l.length - 1]? =
    Option.map (fun a => (n + l.length - 1, a)) l[l.length - 1]?

Tactic:
cases l <;> simp

Result:
case cons
α : Type u_1
n : Nat
head✝ : α
tail✝ : List α
⊢ n + tail✝.length = n + (tail✝.length + 1) - 1

Proof state:
case cons
α : Type u_1
n : Nat
head✝ : α
tail✝ : List α
⊢ n + tail✝.length = n + (tail✝.length + 1) - 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ (enumFrom n l).getLast? = Option.map (fun a => (n + l.length - 1, a)) l.getLast?

Tactic:
simp [getLast?_eq_getElem?]

Result:
α : Type u_1
n : Nat
l : List α
⊢ Option.map (fun a => (n + (l.length - 1), a)) l[l.length - 1]? =
    Option.map (fun a => (n + l.length - 1, a)) l[l.length - 1]?
-- Mathlib/RingTheory/Smooth/Kaehler.lean
theorem Algebra.FormallySmooth.iff_subsingleton_and_projective :
    Algebra.FormallySmooth R S ↔
        Subsingleton (Algebra.H1Cotangent R S) ∧ Module.Projective S (Ω[S⁄R])

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Function.Injective ⇑(Generators.self R S).toExtension.cotangentComplex ↔ Subsingleton (H1Cotangent R S)

Tactic:
rw [← LinearMap.ker_eq_bot, ← Submodule.subsingleton_iff_eq_bot]

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Subsingleton ↥(LinearMap.ker (Generators.self R S).toExtension.cotangentComplex) ↔ Subsingleton (H1Cotangent R S)

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Function.Injective ⇑(kerCotangentToTensor R (Generators.self R S).Ring S) ↔ Subsingleton (H1Cotangent R S)

Tactic:
show Function.Injective (Generators.self R S).toExtension.cotangentComplex ↔ _

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Function.Injective ⇑(Generators.self R S).toExtension.cotangentComplex ↔ Subsingleton (H1Cotangent R S)

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Subsingleton ↥(LinearMap.ker (Generators.self R S).toExtension.cotangentComplex) ↔ Subsingleton (H1Cotangent R S)

Tactic:
rfl

Result:
no goals

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ FormallySmooth R S ↔ Subsingleton (H1Cotangent R S) ∧ Module.Projective S (Ω[S⁄R])

Tactic:
refine (Algebra.FormallySmooth.iff_injective_and_projective
  (Generators.self R S).algebraMap_surjective).trans (and_congr ?_ Iff.rfl)

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Function.Injective ⇑(kerCotangentToTensor R (Generators.self R S).Ring S) ↔ Subsingleton (H1Cotangent R S)
-- Mathlib/Analysis/SpecialFunctions/Bernstein.lean
theorem bernstein_nonneg {n ν : ℕ} {x : I} : 0 ≤ bernstein n ν x

Proof state:
n ν : ℕ
x : ↑I
⊢ 0 ≤ ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Tactic:
have h₁ : (0 : ℝ) ≤ x := by unit_interval

Result:
n ν : ℕ
x : ↑I
h₁ : 0 ≤ ↑x
⊢ 0 ≤ ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Proof state:
n ν : ℕ
x : ↑I
⊢ 0 ≤ (bernstein n ν) x

Tactic:
simp only [bernstein_apply]

Result:
n ν : ℕ
x : ↑I
⊢ 0 ≤ ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Proof state:
n ν : ℕ
x : ↑I
⊢ 0 ≤ ↑x

Tactic:
unit_interval

Result:
no goals

Proof state:
n ν : ℕ
x : ↑I
h₁ : 0 ≤ ↑x
h₂ : 0 ≤ 1 - ↑x
⊢ 0 ≤ ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Tactic:
positivity

Result:
no goals

Proof state:
n ν : ℕ
x : ↑I
h₁ : 0 ≤ ↑x
⊢ 0 ≤ 1 - ↑x

Tactic:
unit_interval

Result:
no goals

Proof state:
n ν : ℕ
x : ↑I
h₁ : 0 ≤ ↑x
⊢ 0 ≤ ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Tactic:
have h₂ : (0 : ℝ) ≤ 1 - x := by unit_interval

Result:
n ν : ℕ
x : ↑I
h₁ : 0 ≤ ↑x
h₂ : 0 ≤ 1 - ↑x
⊢ 0 ≤ ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
lemma ae_compProd_of_ae_ae {κ : Kernel α β} {η : Kernel (α × β) γ}
    {p : β × γ → Prop} (hp : MeasurableSet {x | p x})
    (h : ∀ᵐ b ∂κ a, ∀ᵐ c ∂η (a, b), p (b, c)) :
    ∀ᵐ bc ∂(κ ⊗ₖ η) a, p bc

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ ((κ ⊗ₖ η) a) {a | ¬p a} = 0

Tactic:
rw [compProd_null]

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ (fun b => (η (a, b)) (Prod.mk b ⁻¹' {a | ¬p a})) =ᶠ[ae (κ a)] 0

case pos.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
η : Kernel (α × β) γ
p : β × γ → Prop
hp : MeasurableSet {x | p x}
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0
⊢ MeasurableSet {a | ¬p a}
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem continuous_pow (n : ℕ) : Continuous fun a : ℝ≥0∞ => a ^ n

Proof state:
case succ
n : ℕ
IH : Continuous fun a => a ^ n
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ n * a) x

Tactic:
refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_ <;> by_cases H : x = 0

Result:
case pos
n : ℕ
IH : Continuous fun a => a ^ n
x : ℝ≥0∞
H : x = 0
⊢ x ^ n ≠ 0 ∨ x ≠ ⊤

case neg
n : ℕ
IH : Continuous fun a => a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ^ n ≠ 0 ∨ x ≠ ⊤

case pos
n : ℕ
IH : Continuous fun a => a ^ n
x : ℝ≥0∞
H : x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ⊤

case neg
n : ℕ
IH : Continuous fun a => a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ⊤

Proof state:
case neg
n : ℕ
IH : Continuous fun a => a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ⊤

Tactic:
simp only [H, true_or, Ne, not_false_iff]

Result:
no goals

Proof state:
case succ
n : ℕ
IH : Continuous fun a => a ^ n
⊢ Continuous fun a => a ^ (n + 1)

Tactic:
simp_rw [pow_add, pow_one, continuous_iff_continuousAt]

Result:
case succ
n : ℕ
IH : Continuous fun a => a ^ n
⊢ ∀ (x : ℝ≥0∞), ContinuousAt (fun a => a ^ n * a) x

Proof state:
case succ
n : ℕ
IH : Continuous fun a => a ^ n
⊢ ∀ (x : ℝ≥0∞), ContinuousAt (fun a => a ^ n * a) x

Tactic:
intro x

Result:
case succ
n : ℕ
IH : Continuous fun a => a ^ n
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ n * a) x

Proof state:
case pos
n : ℕ
IH : Continuous fun a => a ^ n
x : ℝ≥0∞
H : x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ⊤

Tactic:
simp only [H, pow_eq_top_iff, zero_ne_top, false_or, eq_self_iff_true, not_true, Ne,
  not_false_iff, false_and]

Result:
no goals

Proof state:
case zero

⊢ Continuous fun a => a ^ 0

Tactic:
simp [continuous_const]

Result:
no goals

Proof state:
case pos
n : ℕ
IH : Continuous fun a => a ^ n
x : ℝ≥0∞
H : x = 0
⊢ x ^ n ≠ 0 ∨ x ≠ ⊤

Tactic:
simp only [H, zero_ne_top, Ne, or_true, not_false_iff]

Result:
no goals

Proof state:
case neg
n : ℕ
IH : Continuous fun a => a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ^ n ≠ 0 ∨ x ≠ ⊤

Tactic:
exact Or.inl fun h => H (pow_eq_zero h)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem prev_of_valid' (cs cs' : List Char) :
    prev ⟨cs ++ cs'⟩ ⟨utf8Len cs⟩ = ⟨utf8Len cs.dropLast⟩

Proof state:
cs cs' : List Char
⊢ { data := [] ++ cs' }.prev { byteIdx := utf8Len [] } = { byteIdx := utf8Len [].dropLast }

Tactic:
rfl

Result:
no goals

Proof state:
cs cs' : List Char
⊢ { data := cs ++ cs' }.prev { byteIdx := utf8Len cs } = { byteIdx := utf8Len cs.dropLast }

Tactic:
match cs, cs.eq_nil_or_concat with
| _, .inl rfl => rfl
| _, .inr ⟨cs, c, rfl⟩ => simp [prev_of_valid]

Result:
no goals

Proof state:
cs✝ cs' cs : List Char
c : Char
⊢ { data := cs.concat c ++ cs' }.prev { byteIdx := utf8Len (cs.concat c) } =
    { byteIdx := utf8Len (cs.concat c).dropLast }

Tactic:
simp [prev_of_valid]

Result:
no goals
-- Mathlib/Data/NNReal/Basic.lean
theorem le_iInf_add_iInf {ι ι' : Sort*} [Nonempty ι] [Nonempty ι'] {f : ι → ℝ≥0} {g : ι' → ℝ≥0}
    {a : ℝ≥0} (h : ∀ i j, a ≤ f i + g j) : a ≤ (⨅ i, f i) + ⨅ j, g j

Proof state:
ι : Sort u_2
ι' : Sort u_3
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0
g : ι' → ℝ≥0
a : ℝ≥0
h : ∀ (i : ι) (j : ι'), a ≤ f i + g j
⊢ a ≤ (⨅ i, f i) + ⨅ j, g j

Tactic:
rw [← NNReal.coe_le_coe, NNReal.coe_add, coe_iInf, coe_iInf]

Result:
ι : Sort u_2
ι' : Sort u_3
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0
g : ι' → ℝ≥0
a : ℝ≥0
h : ∀ (i : ι) (j : ι'), a ≤ f i + g j
⊢ ↑a ≤ (⨅ i, ↑(f i)) + ⨅ i, ↑(g i)

Proof state:
ι : Sort u_2
ι' : Sort u_3
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0
g : ι' → ℝ≥0
a : ℝ≥0
h : ∀ (i : ι) (j : ι'), a ≤ f i + g j
⊢ ↑a ≤ (⨅ i, ↑(f i)) + ⨅ i, ↑(g i)

Tactic:
exact le_ciInf_add_ciInf h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_then_not_self {p : Prop} [Decidable p] {q : Prop} : (if p then ¬p else q) ↔ ¬p ∧ q

Proof state:
p : Prop
inst✝ : Decidable p
q : Prop
⊢ (if p then ¬p else q) ↔ ¬p ∧ q

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_reverse (l : List α) : l.reverse.head? = l.getLast?

Proof state:
α : Type u_1
l : List α
⊢ l.reverse.head? = l.getLast?

Tactic:
rw [← getLast?_reverse, reverse_reverse]

Result:
no goals
-- Mathlib/Order/Cofinal.lean
theorem IsCofinal.mono {s t : Set α} (h : s ⊆ t) (hs : IsCofinal s) : IsCofinal t

Proof state:
case intro.intro
α : Type u_1
inst✝ : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a b : α
hb : b ∈ s
hb' : a ≤ b
⊢ ∃ y ∈ t, a ≤ y

Tactic:
exact ⟨b, h hb, hb'⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a : α
⊢ ∃ y ∈ t, a ≤ y

Tactic:
obtain ⟨b, hb, hb'⟩ := hs a

Result:
case intro.intro
α : Type u_1
inst✝ : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a b : α
hb : b ∈ s
hb' : a ≤ b
⊢ ∃ y ∈ t, a ≤ y

Proof state:
α : Type u_1
inst✝ : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
⊢ IsCofinal t

Tactic:
intro a

Result:
α : Type u_1
inst✝ : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a : α
⊢ ∃ y ∈ t, a ≤ y
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[simp] lemma nnnorm_abs (r : ℝ) : ‖|r|‖₊ = ‖r‖₊

Proof state:
r : ℝ
⊢ ‖|r|‖₊ = ‖r‖₊

Tactic:
simp [nnnorm]

Result:
no goals
-- Mathlib/Data/List/Range.lean
theorem chain'_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) :
    Chain' r (range n.succ) ↔ ∀ m < n, r m m.succ

Proof state:
case zero
r : ℕ → ℕ → Prop
⊢ Chain' r (range 0 ++ [0]) ↔ ∀ (m : ℕ), m < 0 → r m m.succ

Tactic:
simp

Result:
no goals

Proof state:
case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
⊢ Chain' r (range (n + 1) ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ

Tactic:
rw [range_succ]

Result:
case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
⊢ Chain' r (range n ++ [n] ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ

Proof state:
case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
⊢ Chain' r (range n ++ [n]) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ

Tactic:
rw [hn, forall_lt_succ]

Result:
no goals

Proof state:
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain' r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
rw [range_succ]

Result:
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ

Proof state:
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
induction' n with n hn

Result:
case zero
r : ℕ → ℕ → Prop
⊢ Chain' r (range 0 ++ [0]) ↔ ∀ (m : ℕ), m < 0 → r m m.succ

case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
⊢ Chain' r (range (n + 1) ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ

Proof state:
case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
⊢ Chain' r (range n ++ [n] ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ

Tactic:
simp only [append_assoc, singleton_append, chain'_append_cons_cons, chain'_singleton, and_true]

Result:
case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : Chain' r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
⊢ Chain' r (range n ++ [n]) ∧ r n (n + 1) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attach_push {a : α} {l : Vector α n} :
    (l.push a).attach =
      (l.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩

Proof state:
α : Type ?u.14962
n : Nat
a : α
l : Vector α n
⊢ a ∈ l.push a

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
a : α
l : Array α
⊢ ({ toArray := l, size_toArray := ⋯ }.push a).attach =
    (map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          { toArray := l, size_toArray := ⋯ }.attach).push
      ⟨a, ⋯⟩

Tactic:
simp [Array.map_attachWith]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
⊢ (l.push a).attach =
    (map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          l.attach).push
      ⟨a, ⋯⟩

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
a : α
l : Array α
⊢ ({ toArray := l, size_toArray := ⋯ }.push a).attach =
    (map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          { toArray := l, size_toArray := ⋯ }.attach).push
      ⟨a, ⋯⟩