harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsVanKampenColimit.map_reflective [HasColimitsOfShape J C]
    {Gl : C ⥤ D} {Gr : D ⥤ C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful]
    {F : J ⥤ D} {c : Cocone (F ⋙ Gr)} (H : IsVanKampenColimit c)
    [∀ X (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)]
    [∀ X (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl]
    [∀ X i (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl] :
    IsVanKampenColimit (Gl.mapCocone c)

Proof state:
J : Type v'
inst✝⁸ : Category.{u', v'} J
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_2
inst✝⁶ : Category.{u_3, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
⊢ IsVanKampenColimit (Gl.mapCocone c)

Tactic:
have := adj.rightAdjoint_preservesLimits

Result:
J : Type v'
inst✝⁸ : Category.{u', v'} J
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_2
inst✝⁶ : Category.{u_3, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this : PreservesLimitsOfSize.{?u.207770, ?u.207769, u_3, v, u_2, u} Gr
⊢ IsVanKampenColimit (Gl.mapCocone c)
-- Mathlib/RingTheory/Algebraic/Integral.lean
theorem of_smul {y : R} (hy : y ∈ nonZeroDivisors R)
    (h : IsAlgebraic R (y • z)) : IsAlgebraic R z :=
  have ⟨p, hp, eval0⟩ := h
  ⟨_, mt (comp_C_mul_X_eq_zero_iff hy).mp hp, by simpa [aeval_comp, Algebra.smul_def] using eval0⟩

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : y ∈ nonZeroDivisors R
h : IsAlgebraic R (y • z)
p : R[X]
hp : p ≠ 0
eval0 : (aeval (y • z)) p = 0
⊢ (aeval z) (p.comp (C y * X)) = 0

Tactic:
simpa [aeval_comp, Algebra.smul_def] using eval0

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem eqId_iff_eq : A.EqId ↔ A.1 = Δ

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ A.fst = Δ

Tactic:
rw [h]

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ (id Δ).fst = Δ

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId → A.fst = Δ

Tactic:
intro h

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.EqId
⊢ A.fst = Δ

Proof state:
case mpr.mk.mk
fst✝ : SimplexCategoryᵒᵖ
f : unop fst✝ ⟶ unop fst✝
hf this : Epi f
⊢ e ⟨fst✝, ⟨f, hf⟩⟩ = (id fst✝).e

Tactic:
exact eq_id_of_epi f

Result:
no goals

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ (id Δ).fst = Δ

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ A.EqId

Tactic:
rcases A with ⟨_, ⟨f, hf⟩⟩

Result:
case mpr.mk.mk
Δ fst✝ : SimplexCategoryᵒᵖ
f : unop Δ ⟶ unop fst✝
hf : Epi f
h : ⟨fst✝, ⟨f, hf⟩⟩.fst = Δ
⊢ EqId ⟨fst✝, ⟨f, hf⟩⟩

Proof state:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → A.EqId

Tactic:
intro h

Result:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ A.EqId

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.EqId
⊢ A.fst = Δ

Tactic:
dsimp at h

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ A.fst = Δ

Proof state:
case mpr.mk.mk
Δ fst✝ : SimplexCategoryᵒᵖ
f : unop Δ ⟶ unop fst✝
hf : Epi f
h : fst✝ = Δ
⊢ EqId ⟨fst✝, ⟨f, hf⟩⟩

Tactic:
subst h

Result:
case mpr.mk.mk
fst✝ : SimplexCategoryᵒᵖ
f : unop fst✝ ⟶ unop fst✝
hf : Epi f
⊢ EqId ⟨fst✝, ⟨f, hf⟩⟩

Proof state:
case mpr.mk.mk
fst✝ : SimplexCategoryᵒᵖ
f : unop fst✝ ⟶ unop fst✝
hf : Epi f
⊢ EqId ⟨fst✝, ⟨f, hf⟩⟩

Tactic:
refine ext _ _ rfl ?_

Result:
case mpr.mk.mk
fst✝ : SimplexCategoryᵒᵖ
f : unop fst✝ ⟶ unop fst✝
hf : Epi f
⊢ e ⟨fst✝, ⟨f, hf⟩⟩ ≫ eqToHom ⋯ = (id fst✝).e

Proof state:
case mpr.mk.mk
fst✝ : SimplexCategoryᵒᵖ
f : unop fst✝ ⟶ unop fst✝
hf : Epi f
⊢ e ⟨fst✝, ⟨f, hf⟩⟩ ≫ eqToHom ⋯ = (id fst✝).e

Tactic:
haveI := hf

Result:
case mpr.mk.mk
fst✝ : SimplexCategoryᵒᵖ
f : unop fst✝ ⟶ unop fst✝
hf this : Epi f
⊢ e ⟨fst✝, ⟨f, hf⟩⟩ ≫ eqToHom ⋯ = (id fst✝).e

Proof state:
case mpr.mk.mk
Δ fst✝ : SimplexCategoryᵒᵖ
f : unop Δ ⟶ unop fst✝
hf : Epi f
h : ⟨fst✝, ⟨f, hf⟩⟩.fst = Δ
⊢ EqId ⟨fst✝, ⟨f, hf⟩⟩

Tactic:
simp only at h

Result:
case mpr.mk.mk
Δ fst✝ : SimplexCategoryᵒᵖ
f : unop Δ ⟶ unop fst✝
hf : Epi f
h : fst✝ = Δ
⊢ EqId ⟨fst✝, ⟨f, hf⟩⟩

Proof state:
case mpr.mk.mk
fst✝ : SimplexCategoryᵒᵖ
f : unop fst✝ ⟶ unop fst✝
hf this : Epi f
⊢ e ⟨fst✝, ⟨f, hf⟩⟩ ≫ eqToHom ⋯ = (id fst✝).e

Tactic:
simp only [eqToHom_refl, comp_id]

Result:
case mpr.mk.mk
fst✝ : SimplexCategoryᵒᵖ
f : unop fst✝ ⟶ unop fst✝
hf this : Epi f
⊢ e ⟨fst✝, ⟨f, hf⟩⟩ = (id fst✝).e

Proof state:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ A.fst = Δ

Tactic:
constructor

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId → A.fst = Δ

case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → A.EqId
-- Mathlib/Order/PartialSups.lean
theorem partialSups_bot [PartialOrder ι] [LocallyFiniteOrder ι] [OrderBot ι]
    (f : ι → α) : partialSups f ⊥ = f ⊥

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
⊢ Iic ⊥ = {⊥}

Tactic:
simp only [← coe_eq_singleton, coe_Iic, Set.Iic_bot]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
this : Iic ⊥ = {⊥}
⊢ (Iic ⊥).sup' ⋯ f = f ⊥

Tactic:
simp only [this, sup'_singleton]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
⊢ (Iic ⊥).sup' ⋯ f = f ⊥

Tactic:
suffices Iic (⊥ : ι) = {⊥} by simp only [this, sup'_singleton]

Result:
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
⊢ Iic ⊥ = {⊥}

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
⊢ (partialSups f) ⊥ = f ⊥

Tactic:
simp only [partialSups_apply]

Result:
α : Type u_1
ι : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
⊢ (Iic ⊥).sup' ⋯ f = f ⊥
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem iInf_span_singleton {ι : Type*} [Fintype ι] {I : ι → R}
    (hI : ∀ (i j) (_ : i ≠ j), IsCoprime (I i) (I j)) :
    ⨅ i, span ({I i} : Set R) = span {∏ i, I i}

Proof state:
R : Type u
inst✝¹ : CommSemiring R
ι : Type u_2
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ ⨅ i, span {I i} = span {∏ i : ι, I i}

Tactic:
rw [← Finset.inf_univ_eq_iInf, finset_inf_span_singleton]

Result:
case hI
R : Type u
inst✝¹ : CommSemiring R
ι : Type u_2
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ (↑Finset.univ).Pairwise (Function.onFun IsCoprime I)

Proof state:
case hI
R : Type u
inst✝¹ : CommSemiring R
ι : Type u_2
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ (↑Finset.univ).Pairwise (Function.onFun IsCoprime I)

Tactic:
rwa [Finset.coe_univ, Set.pairwise_univ]

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem gradient_eq_deriv : ∇ g u = starRingEnd 𝕜 (deriv g u)

Proof state:
case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : ¬DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)

Tactic:
rw [gradient_eq_zero_of_not_differentiableAt h, deriv_zero_of_not_differentiableAt h, map_zero]

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)

Tactic:
rw [h.hasGradientAt.hasDerivAt.deriv, RCLike.conj_conj]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)

Tactic:
by_cases h : DifferentiableAt 𝕜 g u

Result:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)

case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
u : 𝕜
h : ¬DifferentiableAt 𝕜 g u
⊢ ∇ g u = (starRingEnd 𝕜) (deriv g u)
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
lemma scaleRoots_dvd' (p q : R[X]) {r : R} (hr : IsUnit r)
    (hpq : p ∣ q) : p.scaleRoots r ∣ q.scaleRoots r

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
hpq : p ∣ q
⊢ p.scaleRoots r ∣ q.scaleRoots r

Tactic:
obtain ⟨a, rfl⟩ := hpq

Result:
case intro
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ (p * a).scaleRoots r

Proof state:
case intro
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ (p * a).scaleRoots r

Tactic:
rw [← ((hr.pow (natDegree p + natDegree a - natDegree (p * a))).map
  (algebraMap R R[X])).dvd_mul_left, ← Algebra.smul_def, mul_scaleRoots]

Result:
case intro
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r

Proof state:
case intro
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r

Tactic:
exact dvd_mul_right (scaleRoots p r) (scaleRoots a r)

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_two : S R 2 = X ^ 2 - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
this : S R 2 = X * X - 1
⊢ S R 2 = X ^ 2 - 1

Tactic:
linear_combination this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
this : S R (0 + 2) = X * S R (0 + 1) - S R 0
⊢ S R 2 = X ^ 2 - 1

Tactic:
simp only [zero_add, S_one, S_zero] at this

Result:
R : Type u_1
inst✝ : CommRing R
this : S R 2 = X * X - 1
⊢ S R 2 = X ^ 2 - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ S R 2 = X ^ 2 - 1

Tactic:
have := S_add_two R 0

Result:
R : Type u_1
inst✝ : CommRing R
this : S R (0 + 2) = X * S R (0 + 1) - S R 0
⊢ S R 2 = X ^ 2 - 1
-- Mathlib/LinearAlgebra/FreeModule/PID.lean
@[simp] lemma coord_apply_embedding_eq_smul_coord {i : Fin n} :
    snf.bM.coord (snf.f i) ∘ₗ N.subtype = snf.a i • snf.bN.coord i

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
⊢ snf.bM.coord (snf.f i) ∘ₗ N.subtype = snf.a i • snf.bN.coord i

Tactic:
ext m

Result:
case h
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
m : ↥N
⊢ (snf.bM.coord (snf.f i) ∘ₗ N.subtype) m = (snf.a i • snf.bN.coord i) m

Proof state:
case h
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
m : ↥N
⊢ (snf.bM.coord (snf.f i) ∘ₗ N.subtype) m = (snf.a i • snf.bN.coord i) m

Tactic:
simp [Pi.smul_apply (snf.a i)]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_eq_one_or_self (s : Set α) (f : α → M) (a : α) :
    mulIndicator s f a = 1 ∨ mulIndicator s f a = f a

Proof state:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
exact Or.inr (mulIndicator_of_mem h f)

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : a ∉ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
exact Or.inl (mulIndicator_of_not_mem h f)

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : a ∉ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
-- Mathlib/Analysis/AbsoluteValue/Equivalence.lean
/-- An absolute value is equivalent to the trivial iff it is trivial itself. -/
@[simp]
lemma eq_trivial_of_isEquiv_trivial [DecidablePred fun x : R ↦ x = 0] [NoZeroDivisors R]
    (f : AbsoluteValue R ℝ) :
    f ≈ .trivial ↔ f = .trivial

Proof state:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DecidablePred fun x => x = 0
inst✝ : NoZeroDivisors R
f : AbsoluteValue R ℝ
⊢ f ≈ AbsoluteValue.trivial ↔ f = AbsoluteValue.trivial

Tactic:
refine ⟨fun ⟨c, hc₀, hc⟩ ↦ ext fun x ↦ ?_, fun H ↦ H ▸ isEquiv_refl f⟩

Result:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DecidablePred fun x => x = 0
inst✝ : NoZeroDivisors R
f : AbsoluteValue R ℝ
x✝ : f ≈ AbsoluteValue.trivial
c : ℝ
hc₀ : 0 < c
hc : (fun x => f x ^ c) = ⇑AbsoluteValue.trivial
x : R
⊢ f x = AbsoluteValue.trivial x

Proof state:
case inr
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DecidablePred fun x => x = 0
inst✝ : NoZeroDivisors R
f : AbsoluteValue R ℝ
x✝ : f ≈ AbsoluteValue.trivial
c : ℝ
hc₀ : 0 < c
x : R
hx : x ≠ 0
hc : f x ^ c = 1
⊢ f x = 1

Tactic:
exact (Real.rpow_left_inj (f.nonneg x) zero_le_one hc₀.ne').mp <| (Real.one_rpow c).symm ▸ hc

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DecidablePred fun x => x = 0
inst✝ : NoZeroDivisors R
f : AbsoluteValue R ℝ
x✝ : f ≈ AbsoluteValue.trivial
c : ℝ
hc₀ : 0 < c
x : R
hc : (fun x => f x ^ c) x = AbsoluteValue.trivial x
⊢ f x = AbsoluteValue.trivial x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case inl
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DecidablePred fun x => x = 0
inst✝ : NoZeroDivisors R
f : AbsoluteValue R ℝ
x✝ : f ≈ AbsoluteValue.trivial
c : ℝ
hc₀ : 0 < c
hc : (fun x => f x ^ c) 0 = AbsoluteValue.trivial 0
⊢ f 0 = AbsoluteValue.trivial 0

case inr
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DecidablePred fun x => x = 0
inst✝ : NoZeroDivisors R
f : AbsoluteValue R ℝ
x✝ : f ≈ AbsoluteValue.trivial
c : ℝ
hc₀ : 0 < c
x : R
hc : (fun x => f x ^ c) x = AbsoluteValue.trivial x
hx : x ≠ 0
⊢ f x = AbsoluteValue.trivial x

Proof state:
case inl
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DecidablePred fun x => x = 0
inst✝ : NoZeroDivisors R
f : AbsoluteValue R ℝ
x✝ : f ≈ AbsoluteValue.trivial
c : ℝ
hc₀ : 0 < c
hc : (fun x => f x ^ c) 0 = AbsoluteValue.trivial 0
⊢ f 0 = AbsoluteValue.trivial 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DecidablePred fun x => x = 0
inst✝ : NoZeroDivisors R
f : AbsoluteValue R ℝ
x✝ : f ≈ AbsoluteValue.trivial
c : ℝ
hc₀ : 0 < c
x : R
hc : (fun x => f x ^ c) x = AbsoluteValue.trivial x
hx : x ≠ 0
⊢ f x = AbsoluteValue.trivial x

Tactic:
simp only [ne_eq, hx, not_false_eq_true, trivial_apply] at hc ⊢

Result:
case inr
R : Type u_1
inst✝² : Semiring R
inst✝¹ : DecidablePred fun x => x = 0
inst✝ : NoZeroDivisors R
f : AbsoluteValue R ℝ
x✝ : f ≈ AbsoluteValue.trivial
c : ℝ
hc₀ : 0 < c
x : R
hx : x ≠ 0
hc : f x ^ c = 1
⊢ f x = 1
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_continuous : Continuous (exp 𝕂 : 𝔸 → 𝔸)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
⊢ ContinuousOn (exp 𝕂) (EMetric.ball 0 (expSeries 𝕂 𝔸).radius)

Tactic:
exact continuousOn_exp

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
⊢ Continuous (exp 𝕂)

Tactic:
rw [continuous_iff_continuousOn_univ, ← Metric.eball_top_eq_univ (0 : 𝔸), ←
  expSeries_radius_eq_top 𝕂 𝔸]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
⊢ ContinuousOn (exp 𝕂) (EMetric.ball 0 (expSeries 𝕂 𝔸).radius)
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem zero_isRoot_of_coeff_zero_eq_zero {p : R[X]} (hp : p.coeff 0 = 0) : IsRoot p 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.coeff 0 = 0
⊢ p.IsRoot 0

Tactic:
rwa [coeff_zero_eq_eval_zero] at hp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) :
    get l i = get l' ⟨i, h ▸ i.2⟩

Proof state:
α : Type u_1
l l' : List α
h : l = l'
i : Fin l.length
⊢ l.get i = l'.get ⟨↑i, ⋯⟩

Tactic:
cases h

Result:
case refl
α : Type u_1
l : List α
i : Fin l.length
⊢ l.get i = l.get ⟨↑i, ⋯⟩

Proof state:
case refl
α : Type u_1
l : List α
i : Fin l.length
⊢ l.get i = l.get ⟨↑i, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.div (htu : t ~[l] u) (hvw : v ~[l] w) :
    (fun x ↦ t x / v x) ~[l] fun x ↦ u x / w x

Proof state:
α : Type u_1
β : Type u_3
inst✝ : NormedField β
t u v w : α → β
l : Filter α
htu : t ~[l] u
hvw : v ~[l] w
⊢ (fun x => t x / v x) ~[l] fun x => u x / w x

Tactic:
simpa only [div_eq_mul_inv] using htu.mul hvw.inv

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_lt_rpow_of_exponent_lt {x : ℝ≥0∞} {y z : ℝ} (hx : 1 < x) (hx' : x ≠ ⊤) (hyz : y < z) :
    x ^ y < x ^ z

Proof state:
x : ℝ≥0∞
y z : ℝ
hx : 1 < x
hx' : x ≠ ⊤
hyz : y < z
⊢ x ^ y < x ^ z

Tactic:
lift x to ℝ≥0 using hx'

Result:
case intro
y z : ℝ
hyz : y < z
x : ℝ≥0
hx : 1 < ↑x
⊢ ↑x ^ y < ↑x ^ z

Proof state:
case intro
y z : ℝ
hyz : y < z
x : ℝ≥0
hx : 1 < x
⊢ ↑x ^ y < ↑x ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)),
  NNReal.rpow_lt_rpow_of_exponent_lt hx hyz]

Result:
no goals

Proof state:
case intro
y z : ℝ
hyz : y < z
x : ℝ≥0
hx : 1 < ↑x
⊢ ↑x ^ y < ↑x ^ z

Tactic:
rw [one_lt_coe_iff] at hx

Result:
case intro
y z : ℝ
hyz : y < z
x : ℝ≥0
hx : 1 < x
⊢ ↑x ^ y < ↑x ^ z
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean
/-- The fundamental groupoid functor preserves products -/
lemma preservesProduct : Limits.PreservesLimit (Discrete.functor X) π

Proof state:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (π.mapCone (TopCat.piFan X))

Tactic:
apply (Limits.IsLimit.ofConeEquiv (coneDiscreteComp X)).toFun

Result:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit ((coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)))

Proof state:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Grpd.piLimitFan fun i => π.obj (X i))

Tactic:
exact Grpd.piLimitFanIsLimit _

Result:
no goals

Proof state:
I : Type u
X : I → TopCat
⊢ Limits.PreservesLimit (Discrete.functor X) π

Tactic:
apply Limits.preservesLimit_of_preserves_limit_cone (TopCat.piFanIsLimit X)

Result:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (π.mapCone (TopCat.piFan X))

Proof state:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Limits.Fan.mk (π.obj (TopCat.of ((i : I) → ↑(X i)))) (proj X))

Tactic:
apply Limits.IsLimit.ofIsoLimit _ (asIso (piTopToPiCone X)).symm

Result:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Grpd.piLimitFan fun i => π.obj (X i))

Proof state:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit ((coneDiscreteComp X).functor.obj (π.mapCone (TopCat.piFan X)))

Tactic:
simp only [coneDiscreteComp_obj_mapCone]

Result:
I : Type u
X : I → TopCat
⊢ Limits.IsLimit (Limits.Fan.mk (π.obj (TopCat.of ((i : I) → ↑(X i)))) (proj X))
-- Mathlib/SetTheory/Cardinal/Divisibility.lean
theorem nat_is_prime_iff : Prime (n : Cardinal) ↔ n.Prime

Proof state:
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b

Tactic:
rwa [mul_comm] at h'

Result:
no goals

Proof state:
case refine_3.inr
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
⊢ ↑n ∣ b ∨ ↑n ∣ c

Tactic:
rcases aleph0_le_mul_iff.mp h' with ⟨hb, hc, hℵ₀⟩

Result:
case refine_3.inr.intro.intro
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
⊢ ↑n ∣ b ∨ ↑n ∣ c

Proof state:
n✝ n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
hℵ₀b : ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c

Tactic:
exact Or.inl (dvd_of_le_of_aleph0_le hn ((nat_lt_aleph0 n).le.trans hℵ₀b) hℵ₀b)

Result:
no goals

Proof state:
n : ℕ
⊢ ↑n ≠ 0 ↔ n ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_3.inr.intro.intro
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
⊢ ↑n ∣ b ∨ ↑n ∣ c

Tactic:
have hn : (n : Cardinal) ≠ 0 := by
  intro h
  rw [h, zero_dvd_iff, mul_eq_zero] at hbc
  cases hbc <;> contradiction

Result:
case refine_3.inr.intro.intro
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
⊢ ↑n ∣ b ∨ ↑n ∣ c
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesHasSum.smul {f : ℕ → ℂ} (c : ℂ) {s a : ℂ} (hf : LSeriesHasSum f s a) :
    LSeriesHasSum (c • f) s (c * a)

Proof state:
f : ℕ → ℂ
c s a : ℂ
hf : LSeriesHasSum f s a
⊢ LSeriesHasSum (c • f) s (c * a)

Tactic:
simpa [LSeriesHasSum, term_smul] using hf.const_smul c

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem mul_sub (h : 0 < c → c < b → a ≠ ∞) : a * (b - c) = a * b - a * c

Proof state:
a b c : ℝ≥0∞
h : 0 < c → c < b → a ≠ ⊤
⊢ a * (b - c) = a * b - a * c

Tactic:
simp only [mul_comm a]

Result:
a b c : ℝ≥0∞
h : 0 < c → c < b → a ≠ ⊤
⊢ (b - c) * a = b * a - c * a

Proof state:
a b c : ℝ≥0∞
h : 0 < c → c < b → a ≠ ⊤
⊢ (b - c) * a = b * a - c * a

Tactic:
exact ENNReal.sub_mul h

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_zero {i : Set α} : (0 : VectorMeasure α M).restrict i = 0

Proof state:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : MeasurableSet i
⊢ restrict 0 i = 0

Tactic:
ext j hj

Result:
case pos.h
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict 0 i) j = ↑0 j

Proof state:
case pos.h
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict 0 i) j = ↑0 j

Tactic:
rw [restrict_apply 0 hi hj, zero_apply, zero_apply]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict 0 i = 0

Tactic:
exact dif_neg hi

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
⊢ restrict 0 i = 0

Tactic:
by_cases hi : MeasurableSet i

Result:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : MeasurableSet i
⊢ restrict 0 i = 0

case neg
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict 0 i = 0