harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem polynomial_comp_attachBound (A : Subalgebra ℝ C(X, ℝ)) (f : A) (g : ℝ[X]) :
    (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (f : C(X, ℝ)).attachBound =
      Polynomial.aeval f g

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
a✝ : X
⊢ ((g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound) a✝ = ↑((Polynomial.aeval f) g) a✝

Tactic:
simp only [Polynomial.aeval_subalgebra_coe, Polynomial.aeval_continuousMap_apply]

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
a✝ : X
⊢ ((g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound) a✝ = Polynomial.eval (↑f a✝) g

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
⊢ (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound = ↑((Polynomial.aeval f) g)

Tactic:
ext

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
a✝ : X
⊢ ((g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound) a✝ = ↑((Polynomial.aeval f) g) a✝

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
a✝ : X
⊢ ((g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound) a✝ = Polynomial.eval (↑f a✝) g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toNNReal_lt_toNNReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toNNReal < b.toNNReal ↔ a < b :=
  ⟨fun h => by rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_lt_coe], toNNReal_strict_mono hb⟩

Proof state:
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ ⊤
h : a.toNNReal < b.toNNReal
⊢ a < b

Tactic:
rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_lt_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) (h') :
    (modify f m l)[n] = l[n]'(by simpa using h')

Proof state:
α : Type u_1
f : α → α
m n : Nat
l : List α
h : m ≠ n
h' : n < (modify f m l).length
⊢ (modify f m l)[n] = l[n]

Tactic:
simp [getElem_modify, h]

Result:
no goals

Proof state:
α : Type ?u.25079
f : α → α
m n : Nat
l : List α
h : m ≠ n
h' : n < (modify f m l).length
⊢ n < l.length

Tactic:
simpa using h'

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_bitm1 [AddGroupWithOne α] (n : ZNum) : (n.bitm1 : α) = (n : α) + n - 1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(- -n).bitm1 = ↑n + ↑n - 1

Tactic:
rw [← zneg_bit1, cast_zneg, cast_bit1]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ -(↑(-n) + ↑(-n) + 1) = ↑n + ↑n - 1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)

Tactic:
simp [add_comm, add_left_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
this : ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)
⊢ -(↑(-n) + ↑(-n) + 1) = ↑n + ↑n - 1

Tactic:
simpa [sub_eq_add_neg] using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑n.bitm1 = ↑n + ↑n - 1

Tactic:
conv =>
  lhs
  rw [← zneg_zneg n]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(- -n).bitm1 = ↑n + ↑n - 1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ -(↑(-n) + ↑(-n) + 1) = ↑n + ↑n - 1

Tactic:
have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ) := by simp [add_comm, add_left_comm]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
this : ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)
⊢ -(↑(-n) + ↑(-n) + 1) = ↑n + ↑n - 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem mem_append_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs

Proof state:
α : Type u
a : α
as bs : List α
h : a ∈ as
⊢ a ∈ as ++ bs

Tactic:
induction h with
| head => apply Mem.head
| tail => apply Mem.tail; assumption

Result:
no goals

Proof state:
α : Type u
a : α
as bs : List α
⊢ a ∈ as → a ∈ as ++ bs

Tactic:
intro h

Result:
α : Type u
a : α
as bs : List α
h : a ∈ as
⊢ a ∈ as ++ bs

Proof state:
case tail.a
α : Type u
a : α
as bs : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
a_ih✝ : a ∈ as✝ ++ bs
⊢ Mem a (as✝.append bs)

Tactic:
assumption

Result:
no goals

Proof state:
case tail
α : Type u
a : α
as bs : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
a_ih✝ : a ∈ as✝ ++ bs
⊢ a ∈ b✝ :: as✝ ++ bs

Tactic:
apply Mem.tail

Result:
case tail.a
α : Type u
a : α
as bs : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
a_ih✝ : a ∈ as✝ ++ bs
⊢ Mem a (as✝.append bs)

Proof state:
case head
α : Type u
a : α
as bs as✝ : List α
⊢ a ∈ a :: as✝ ++ bs

Tactic:
apply Mem.head

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_replicate (a b : α) (n : Nat) : count a (replicate n b) = if b == a then n else 0

Proof state:
case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
h : ¬(b == a) = true
⊢ count a (replicate n b) = 0

Tactic:
simp only [beq_iff_eq] at h

Result:
case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
h : ¬b = a
⊢ count a (replicate n b) = 0

Proof state:
case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
h : ¬b = a
⊢ count a (replicate n b) = 0

Tactic:
exact count_eq_zero.2 <| mt eq_of_mem_replicate (Ne.symm h)

Result:
no goals

Proof state:
case isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
h : b = a
⊢ count a (replicate n b) = n

Tactic:
exact ‹b = a› ▸ count_replicate_self ..

Result:
no goals

Proof state:
case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
h✝ : ¬(b == a) = true
⊢ count a (replicate n b) = 0

Tactic:
rename_i h

Result:
case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
h : ¬(b == a) = true
⊢ count a (replicate n b) = 0

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
⊢ count a (replicate n b) = if (b == a) = true then n else 0

Tactic:
split <;> (rename_i h; simp only [beq_iff_eq] at h)

Result:
case isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
h : b = a
⊢ count a (replicate n b) = n

case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
h : ¬b = a
⊢ count a (replicate n b) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_append' [Monad m] [LawfulMonad m] (f : α → β → m β) (b) (l l' : Array α)
    (w : start = l.size + l'.size) :
    (l ++ l').foldrM f b start 0 = l'.foldrM f b >>= l.foldrM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
start : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l l' : Array α
w : start = l.size + l'.size
⊢ foldrM f b (l ++ l') start = do
    let init ← foldrM f b l'
    foldrM f init l

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l l' : Array α
⊢ foldrM f b (l ++ l') (l.size + l'.size) = do
    let init ← foldrM f b l'
    foldrM f init l

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l l' : List α
⊢ foldrM f b ({ toList := l } ++ { toList := l' }) ({ toList := l }.size + { toList := l' }.size) = do
    let init ← foldrM f b { toList := l' }
    foldrM f init { toList := l }

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l l' : Array α
⊢ foldrM f b (l ++ l') (l.size + l'.size) = do
    let init ← foldrM f b l'
    foldrM f init l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l' : Array α
l : List α
⊢ foldrM f b ({ toList := l } ++ l') ({ toList := l }.size + l'.size) = do
    let init ← foldrM f b l'
    foldrM f init { toList := l }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l' : Array α
l : List α
⊢ foldrM f b ({ toList := l } ++ l') ({ toList := l }.size + l'.size) = do
    let init ← foldrM f b l'
    foldrM f init { toList := l }

Tactic:
rcases l' with ⟨l'⟩

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l l' : List α
⊢ foldrM f b ({ toList := l } ++ { toList := l' }) ({ toList := l }.size + { toList := l' }.size) = do
    let init ← foldrM f b { toList := l' }
    foldrM f init { toList := l }
-- Mathlib/Analysis/Convex/Gauge.lean
theorem le_gauge_of_not_mem (hs₀ : StarConvex ℝ 0 s) (hs₂ : Absorbs ℝ s {x}) (hx : x ∉ a • s) :
    a ≤ gauge s x

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
r : ℝ
hr : r > 0
h : ∀ (c : ℝ), r ≤ ‖c‖ → {x} ⊆ c • s
⊢ a ≤ gauge s x

Tactic:
refine le_csInf ⟨r, hr, singleton_subset_iff.1 <| h _ (Real.norm_of_nonneg hr.le).ge⟩ ?_

Result:
case intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
r : ℝ
hr : r > 0
h : ∀ (c : ℝ), r ≤ ‖c‖ → {x} ⊆ c • s
⊢ ∀ b ∈ {r | 0 < r ∧ x ∈ r • s}, a ≤ b
-- Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
lemma wInner_cWeight_eq_zero_iff_ne [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = 0 ↔ ψ₁ ≠ ψ₂

Proof state:
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
ψ₁ ψ₂ : AddChar G R
inst✝ : Fintype G
⊢ wInner cWeight ⇑ψ₁ ⇑ψ₂ = 0 ↔ ψ₁ ≠ ψ₂

Tactic:
rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_right_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Simple.lean
theorem kernel_zero_of_nonzero_from_simple {X Y : C} [Simple X] {f : X ⟶ Y} [HasKernel f]
    (w : f ≠ 0) : kernel.ι f = 0

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
h : ¬kernel.ι f = 0
⊢ False

Tactic:
haveI := isIso_of_mono_of_nonzero h

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
h : ¬kernel.ι f = 0
this : IsIso (kernel.ι f)
⊢ False

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
h : ¬kernel.ι f = 0
this : IsIso (kernel.ι f)
⊢ False

Tactic:
exact w (eq_zero_of_epi_kernel f)

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
⊢ kernel.ι f = 0

Tactic:
classical
  by_contra h
  haveI := isIso_of_mono_of_nonzero h
  exact w (eq_zero_of_epi_kernel f)

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
⊢ kernel.ι f = 0

Tactic:
by_contra h

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
h : ¬kernel.ι f = 0
⊢ False
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Red.Step.invRev {L₁ L₂ : List (α × Bool)} (h : Red.Step L₁ L₂) :
    Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
h : Step L₁ L₂
⊢ Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)

Tactic:
obtain ⟨a, b, x, y⟩ := h

Result:
case not
α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (FreeGroup.invRev (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (FreeGroup.invRev (L₁✝ ++ L₂✝))

Proof state:
case not
α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (FreeGroup.invRev (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (FreeGroup.invRev (L₁✝ ++ L₂✝))

Tactic:
simp [FreeGroup.invRev]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem IsPrime.multiset_prod_map_le {s : Multiset ι} (f : ι → Ideal R) {P : Ideal R}
    (hp : IsPrime P) : (s.map f).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Multiset ι
f : ι → Ideal R
P : Ideal R
hp : P.IsPrime
⊢ (Multiset.map f s).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P

Tactic:
simp_rw [hp.multiset_prod_le, Multiset.mem_map, exists_exists_and_eq_and]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem range_eq_iSup {N} [Group N] (f : ∀ i, G i →* N) : (lift f).range = ⨆ i, (f i).range

Proof state:
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ ∀ (i : ι), (f i).range ≤ (lift f).range

Tactic:
rintro i _ ⟨x, rfl⟩

Result:
case intro
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
i : ι
x : G i
⊢ (f i) x ∈ (lift f).range

Proof state:
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
i : ι
x : G i
⊢ (lift f) (of x) = (f i) x

Tactic:
simp only [lift_of]

Result:
no goals

Proof state:
case intro
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
i : ι
x : G i
⊢ (f i) x ∈ (lift f).range

Tactic:
exact ⟨of x, by simp only [lift_of]⟩

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ (lift f).range = ⨆ i, (f i).range

Tactic:
apply le_antisymm (lift_range_le _ f fun i => le_iSup (fun i => MonoidHom.range (f i)) i)

Result:
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ ⨆ i, (f i).range ≤ (lift f).range

Proof state:
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ ⨆ i, (f i).range ≤ (lift f).range

Tactic:
apply iSup_le _

Result:
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ ∀ (i : ι), (f i).range ≤ (lift f).range
-- Mathlib/Tactic/Ring/Basic.lean
theorem pow_congr {b b' : ℕ} (_ : a = a') (_ : b = b')
    (_ : a' ^ b' = c) : (a ^ b : R) = c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a a' c : R
b b' : ℕ
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' ^ b' = c
⊢ a ^ b = c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a' : R
b' : ℕ
⊢ a' ^ b' = a' ^ b'

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a' : R
b' : ℕ
⊢ a' ^ b' = a' ^ b'

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/ODE/Gronwall.lean
theorem hasDerivAt_gronwallBound (δ K ε x : ℝ) :
    HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Proof state:
δ K ε x : ℝ
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Tactic:
by_cases hK : K = 0

Result:
case pos
δ K ε x : ℝ
hK : K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

case neg
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Proof state:
case neg
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Tactic:
simp only [gronwallBound_of_K_ne_0 hK]

Result:
case neg
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (fun x => δ * rexp (K * x) + ε / K * (rexp (K * x) - 1))
    (K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε) x

Proof state:
case h.e'_9
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε =
    δ * (rexp (K * id x) * (K * 1)) + ε / K * (rexp (K * id x) * (K * 1))

Tactic:
simp only [id, mul_add, (mul_assoc _ _ _).symm, mul_comm _ K, mul_div_cancel₀ _ hK]

Result:
case h.e'_9
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * δ * rexp (K * x) + ε * (rexp (K * x) - 1) + ε = K * δ * rexp (K * x) * 1 + ε * rexp (K * x) * 1

Proof state:
case pos
δ ε x : ℝ
⊢ HasDerivAt (fun x => δ + ε * x) ε x

Tactic:
convert ((hasDerivAt_id x).const_mul ε).const_add δ

Result:
case h.e'_9
δ ε x : ℝ
⊢ ε = ε * 1

Proof state:
case pos
δ K ε x : ℝ
hK : K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Tactic:
subst K

Result:
case pos
δ ε x : ℝ
⊢ HasDerivAt (gronwallBound δ 0 ε) (0 * gronwallBound δ 0 ε x + ε) x

Proof state:
case h.e'_9
δ ε x : ℝ
⊢ ε = ε * 1

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
case neg
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (fun x => δ * rexp (K * x) + ε / K * (rexp (K * x) - 1))
    (K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε) x

Tactic:
convert (((hasDerivAt_id x).const_mul K).exp.const_mul δ).add
  ((((hasDerivAt_id x).const_mul K).exp.sub_const 1).const_mul (ε / K)) using 1

Result:
case h.e'_9
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε =
    δ * (rexp (K * id x) * (K * 1)) + ε / K * (rexp (K * id x) * (K * 1))

Proof state:
case h.e'_9
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * δ * rexp (K * x) + ε * (rexp (K * x) - 1) + ε = K * δ * rexp (K * x) * 1 + ε * rexp (K * x) * 1

Tactic:
ring

Result:
no goals

Proof state:
case pos
δ ε x : ℝ
⊢ HasDerivAt (gronwallBound δ 0 ε) (0 * gronwallBound δ 0 ε x + ε) x

Tactic:
simp only [gronwallBound_K0, zero_mul, zero_add]

Result:
case pos
δ ε x : ℝ
⊢ HasDerivAt (fun x => δ + ε * x) ε x
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem edist_div_right [DivInvMonoid M] [PseudoEMetricSpace M] [IsometricSMul Mᵐᵒᵖ M]
    (a b c : M) : edist (a / c) (b / c) = edist a b

Proof state:
M : Type u
inst✝² : DivInvMonoid M
inst✝¹ : PseudoEMetricSpace M
inst✝ : IsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ edist (a / c) (b / c) = edist a b

Tactic:
simp only [div_eq_mul_inv, edist_mul_right]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
theorem universally_inf (P Q : MorphismProperty C) :
    (P ⊓ Q).universally = P.universally ⊓ Q.universally

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → (P ⊓ Q) f') ↔
    ∀ (x x_1 : C) (x_2 : x ⟶ X) (x_3 : x_1 ⟶ Y) (x_4 : x ⟶ x_1), IsPullback x_4 x_2 x_3 f → P x_4 ∧ Q x_4

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
⊢ (P ⊓ Q).universally = P.universally ⊓ Q.universally

Tactic:
ext X Y f

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (P ⊓ Q).universally f ↔ (P.universally ⊓ Q.universally) f

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (P ⊓ Q).universally f ↔ P.universally f ∧ Q.universally f

Tactic:
simp_rw [universally, ← forall_and]

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → (P ⊓ Q) f') ↔
    ∀ (x x_1 : C) (x_2 : x ⟶ X) (x_3 : x_1 ⟶ Y) (x_4 : x ⟶ x_1), IsPullback x_4 x_2 x_3 f → P x_4 ∧ Q x_4

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (P ⊓ Q).universally f ↔ (P.universally ⊓ Q.universally) f

Tactic:
show _ ↔ _ ∧ _

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (P ⊓ Q).universally f ↔ P.universally f ∧ Q.universally f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.length) :
    l.toArray.filter p 0 stop = (l.filter p).toArray

Proof state:
α : Type u_1
stop : Nat
p : α → Bool
l : List α
h : stop = l.length
⊢ filter p l.toArray 0 stop = (List.filter p l).toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
stop : Nat
p : α → Bool
l : List α
h : stop = l.length
⊢ (filter p l.toArray 0 stop).toList = (List.filter p l).toArray.toList

Proof state:
case h
α : Type u_1
stop : Nat
p : α → Bool
l : List α
h : stop = l.length
⊢ (filter p l.toArray 0 stop).toList = (List.filter p l).toArray.toList

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean
theorem PreservesEqualizer.iso_inv_ι :
    (PreservesEqualizer.iso G f g).inv ≫ G.map (equalizer.ι f g) =
      equalizer.ι (G.map f) (G.map g)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasEqualizer f g
inst✝¹ : HasEqualizer (G.map f) (G.map g)
inst✝ : PreservesLimit (parallelPair f g) G
⊢ 𝟙 (G.obj (equalizer f g)) ≫ G.map (equalizer.ι f g) = (iso G f g).hom ≫ equalizer.ι (G.map f) (G.map g)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasEqualizer f g
inst✝¹ : HasEqualizer (G.map f) (G.map g)
inst✝ : PreservesLimit (parallelPair f g) G
⊢ (iso G f g).inv ≫ G.map (equalizer.ι f g) = equalizer.ι (G.map f) (G.map g)

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesEqualizer.iso G f g), ← Category.assoc, Iso.hom_inv_id]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasEqualizer f g
inst✝¹ : HasEqualizer (G.map f) (G.map g)
inst✝ : PreservesLimit (parallelPair f g) G
⊢ 𝟙 (G.obj (equalizer f g)) ≫ G.map (equalizer.ι f g) = (iso G f g).hom ≫ equalizer.ι (G.map f) (G.map g)
-- Mathlib/RingTheory/Support.lean
lemma Module.support_of_noZeroSMulDivisors [NoZeroSMulDivisors R M] [Nontrivial M] :
    Module.support R M = Set.univ

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
⊢ support R M = Set.univ

Tactic:
simp only [Set.eq_univ_iff_forall, mem_support_iff', ne_eq, smul_eq_zero, not_or]

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
⊢ ∀ (x : PrimeSpectrum R), ∃ m, ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
⊢ ∀ (x : PrimeSpectrum R), ∃ m, ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0

Tactic:
exact fun p ↦ ⟨x, fun r hr ↦ ⟨fun e ↦ hr (e ▸ p.asIdeal.zero_mem), hx⟩⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
⊢ ∀ (x : PrimeSpectrum R), ∃ m, ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
⊢ ∀ (x : PrimeSpectrum R), ∃ m, ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
    (a == b) = decide (a = b)

Proof state:
α : Type u_1
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
⊢ (a == b) = decide (a = b)

Tactic:
cases h : a == b

Result:
case false
α : Type u_1
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h : (a == b) = false
⊢ false = decide (a = b)

case true
α : Type u_1
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h : (a == b) = true
⊢ true = decide (a = b)

Proof state:
case true
α : Type u_1
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h : (a == b) = true
⊢ true = decide (a = b)

Tactic:
simp [eq_of_beq h]

Result:
no goals

Proof state:
case false
α : Type u_1
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : DecidableEq α
a b : α
h : (a == b) = false
⊢ false = decide (a = b)

Tactic:
simp [ne_of_beq_false h]

Result:
no goals
-- Mathlib/Algebra/Order/Quantale.lean
theorem mul_iSup_distrib : x * ⨆ i, f i = ⨆ i, x * f i

Proof state:
α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ x * ⨆ i, f i = ⨆ i, x * f i

Tactic:
rw [iSup, mul_sSup_distrib, iSup_range]

Result:
no goals