harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Factors.lean
theorem perm_primeFactorsList_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
    (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Proof state:
case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ++ b.primeFactorsList
⊢ Prime p

Tactic:
rw [List.mem_append] at hp

Result:
case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
⊢ Prime p

Proof state:
case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b

Tactic:
rw [List.prod_append, prod_primeFactorsList ha, prod_primeFactorsList hb]

Result:
no goals

Proof state:
case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
⊢ Prime p

Tactic:
rcases hp with hp' | hp' <;> exact prime_of_mem_primeFactorsList hp'

Result:
no goals

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
refine (primeFactorsList_unique ?_ ?_).symm

Result:
case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b

case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ p ∈ a.primeFactorsList ++ b.primeFactorsList, Prime p

Proof state:
case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ p ∈ a.primeFactorsList ++ b.primeFactorsList, Prime p

Tactic:
intro p hp

Result:
case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ++ b.primeFactorsList
⊢ Prime p
-- Mathlib/Algebra/Category/Grp/Zero.lean
theorem isZero_of_subsingleton (G : Grp) [Subsingleton G] : IsZero G

Proof state:
case refine_1
G : Grp
inst✝ : Subsingleton ↑G
X : Grp
f : G ⟶ X
⊢ f = default

Tactic:
ext x

Result:
case refine_1.hf.h
G : Grp
inst✝ : Subsingleton ↑G
X : Grp
f : G ⟶ X
x : ↑G
⊢ (Hom.hom f) x = (Hom.hom default) x

Proof state:
case refine_2
G : Grp
inst✝ : Subsingleton ↑G
X : Grp
f : X ⟶ G
⊢ f = default

Tactic:
ext

Result:
case refine_2.hf.h
G : Grp
inst✝ : Subsingleton ↑G
X : Grp
f : X ⟶ G
x✝ : ↑X
⊢ (Hom.hom f) x✝ = (Hom.hom default) x✝

Proof state:
G : Grp
inst✝ : Subsingleton ↑G
⊢ IsZero G

Tactic:
refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩

Result:
case refine_1
G : Grp
inst✝ : Subsingleton ↑G
X : Grp
f : G ⟶ X
⊢ f = default

case refine_2
G : Grp
inst✝ : Subsingleton ↑G
X : Grp
f : X ⟶ G
⊢ f = default

Proof state:
case refine_1.hf.h
G : Grp
inst✝ : Subsingleton ↑G
X : Grp
f : G ⟶ X
x : ↑G
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
have : x = 1 := Subsingleton.elim _ _

Result:
case refine_1.hf.h
G : Grp
inst✝ : Subsingleton ↑G
X : Grp
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) x = (Hom.hom default) x

Proof state:
case refine_1.hf.h
G : Grp
inst✝ : Subsingleton ↑G
X : Grp
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
rw [this, map_one, map_one]

Result:
no goals

Proof state:
case refine_2.hf.h
G : Grp
inst✝ : Subsingleton ↑G
X : Grp
f : X ⟶ G
x✝ : ↑X
⊢ (Hom.hom f) x✝ = (Hom.hom default) x✝

Tactic:
subsingleton

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_of_integrable_trim (hm : m ≤ m0) (hf_int : Integrable f (μ'.trim hm)) :
    Integrable f μ'

Proof state:
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f (μ'.trim hm)
⊢ Integrable f μ'

Tactic:
obtain ⟨hf_meas_ae, hf⟩ := hf_int

Result:
case intro
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
hf : HasFiniteIntegral f (μ'.trim hm)
⊢ Integrable f μ'

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
hf : HasFiniteIntegral f (μ'.trim hm)
⊢ Integrable f μ'

Tactic:
refine ⟨aestronglyMeasurable_of_aestronglyMeasurable_trim hm hf_meas_ae, ?_⟩

Result:
case intro
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
hf : HasFiniteIntegral f (μ'.trim hm)
⊢ HasFiniteIntegral f μ'

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
hf : HasFiniteIntegral f (μ'.trim hm)
⊢ HasFiniteIntegral f μ'

Tactic:
simpa [HasFiniteIntegral, lintegral_trim_ae hm hf_meas_ae.enorm] using hf

Result:
no goals
-- Mathlib/Data/List/TFAE.lean
theorem tfae_cons_of_mem {a b} {l : List Prop} (h : b ∈ l) : TFAE (a :: l) ↔ (a ↔ b) ∧ TFAE l :=
  ⟨fun H => ⟨H a (by simp) b (Mem.tail a h),
    fun _ hp _ hq => H _ (Mem.tail a hp) _ (Mem.tail a hq)⟩,
      by
        rintro ⟨ab, H⟩ p (_ | ⟨_, hp⟩) q (_ | ⟨_, hq⟩)
        · rfl
        · exact ab.trans (H _ h _ hq)
        · exact (ab.trans (H _ h _ hp)).symm
        · exact H _ hp _ hq⟩

Proof state:
case intro.tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
⊢ p ↔ a

Tactic:
exact (ab.trans (H _ h _ hp)).symm

Result:
no goals

Proof state:
case intro.tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q

Tactic:
exact H _ hp _ hq

Result:
no goals

Proof state:
a b : Prop
l : List Prop
h : b ∈ l
H : (a :: l).TFAE
⊢ a ∈ a :: l

Tactic:
simp

Result:
no goals

Proof state:
case intro.head.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
⊢ a ↔ a

Tactic:
rfl

Result:
no goals

Proof state:
case intro.head.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
q : Prop
hq : Mem q l
⊢ a ↔ q

Tactic:
exact ab.trans (H _ h _ hq)

Result:
no goals

Proof state:
a b : Prop
l : List Prop
h : b ∈ l
⊢ (a ↔ b) ∧ l.TFAE → (a :: l).TFAE

Tactic:
rintro ⟨ab, H⟩ p (_ | ⟨_, hp⟩) q (_ | ⟨_, hq⟩)

Result:
case intro.head.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
⊢ a ↔ a

case intro.head.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
q : Prop
hq : Mem q l
⊢ a ↔ q

case intro.tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
⊢ p ↔ a

case intro.tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma toENNReal_coe {x : ℝ≥0∞} : (x : EReal).toENNReal = x

Proof state:
x : ℝ≥0∞
⊢ (↑x).toENNReal = x

Tactic:
by_cases h_top : x = ⊤

Result:
case pos
x : ℝ≥0∞
h_top : x = ⊤
⊢ (↑x).toENNReal = x

case neg
x : ℝ≥0∞
h_top : ¬x = ⊤
⊢ (↑x).toENNReal = x

Proof state:
case neg
x : ℝ≥0∞
h_top : ¬x = ⊤
⊢ (↑x).toENNReal = x

Tactic:
rwa [toENNReal, if_neg _, toReal_coe_ennreal, ENNReal.ofReal_toReal_eq_iff]

Result:
x : ℝ≥0∞
h_top : ¬x = ⊤
⊢ ¬↑x = ⊤

Proof state:
case pos
x : ℝ≥0∞
h_top : x = ⊤
⊢ (↑x).toENNReal = x

Tactic:
rw [h_top, coe_ennreal_top, toENNReal_top]

Result:
no goals

Proof state:
x : ℝ≥0∞
h_top : ¬x = ⊤
⊢ ¬↑x = ⊤

Tactic:
simp [h_top]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Noetherian.lean
theorem isLocallyNoetherian_iff_openCover (𝒰 : Scheme.OpenCover X) :
    IsLocallyNoetherian X ↔ ∀ (i : 𝒰.J), IsLocallyNoetherian (𝒰.obj i)

Proof state:
case mpr
X : Scheme
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), IsLocallyNoetherian (𝒰.obj i)
i : 𝒰.affineRefinement.openCover.J
⊢ IsNoetherianRing ↑Γ(𝒰.affineRefinement.openCover.obj i, ⊤)

Tactic:
exact @isNoetherianRing_of_ringEquiv _ _ _ _
  (IsOpenImmersion.ΓIsoTop (Scheme.Cover.map _ i.2)).symm.commRingCatIsoToRingEquiv
  (IsLocallyNoetherian.component_noetherian ⟨_, isAffineOpen_opensRange _⟩)

Result:
no goals

Proof state:
case mp
X : Scheme
𝒰 : X.OpenCover
⊢ IsLocallyNoetherian X → ∀ (i : 𝒰.J), IsLocallyNoetherian (𝒰.obj i)

Tactic:
intro h i

Result:
case mp
X : Scheme
𝒰 : X.OpenCover
h : IsLocallyNoetherian X
i : 𝒰.J
⊢ IsLocallyNoetherian (𝒰.obj i)

Proof state:
X : Scheme
𝒰 : X.OpenCover
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.J), IsLocallyNoetherian (𝒰.obj i)

Tactic:
constructor

Result:
case mp
X : Scheme
𝒰 : X.OpenCover
⊢ IsLocallyNoetherian X → ∀ (i : 𝒰.J), IsLocallyNoetherian (𝒰.obj i)

case mpr
X : Scheme
𝒰 : X.OpenCover
⊢ (∀ (i : 𝒰.J), IsLocallyNoetherian (𝒰.obj i)) → IsLocallyNoetherian X

Proof state:
case mp
X : Scheme
𝒰 : X.OpenCover
h : IsLocallyNoetherian X
i : 𝒰.J
⊢ IsLocallyNoetherian (𝒰.obj i)

Tactic:
exact isLocallyNoetherian_of_isOpenImmersion (𝒰.map i)

Result:
no goals

Proof state:
case mpr
X : Scheme
𝒰 : X.OpenCover
⊢ (∀ (i : 𝒰.J), IsLocallyNoetherian (𝒰.obj i)) → IsLocallyNoetherian X

Tactic:
rw [isLocallyNoetherian_iff_of_affine_openCover (𝒰 := 𝒰.affineRefinement.openCover)]

Result:
case mpr
X : Scheme
𝒰 : X.OpenCover
⊢ (∀ (i : 𝒰.J), IsLocallyNoetherian (𝒰.obj i)) →
    ∀ (i : 𝒰.affineRefinement.openCover.J), IsNoetherianRing ↑Γ(𝒰.affineRefinement.openCover.obj i, ⊤)

Proof state:
case mpr
X : Scheme
𝒰 : X.OpenCover
⊢ (∀ (i : 𝒰.J), IsLocallyNoetherian (𝒰.obj i)) →
    ∀ (i : 𝒰.affineRefinement.openCover.J), IsNoetherianRing ↑Γ(𝒰.affineRefinement.openCover.obj i, ⊤)

Tactic:
intro h i

Result:
case mpr
X : Scheme
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.J), IsLocallyNoetherian (𝒰.obj i)
i : 𝒰.affineRefinement.openCover.J
⊢ IsNoetherianRing ↑Γ(𝒰.affineRefinement.openCover.obj i, ⊤)
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma opcyclesMap_comp_descOpcycles {A : C} (k : L.X i ⟶ A) (j : ι) (hj : c.prev i = j)
    (hk : L.d j i ≫ k = 0) (φ : K ⟶ L) :
    opcyclesMap φ i ≫ L.descOpcycles k j hj hk = K.descOpcycles (φ.f i ≫ k) j hj
      (by rw [← φ.comm_assoc, hk, comp_zero])

Proof state:
C : Type u_1
inst✝⁴ : Category.{?u.105019, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ✝ : K ⟶ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
⊢ K.d j i ≫ φ.f i ≫ k = 0

Tactic:
rw [← φ.comm_assoc, hk, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex C c
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
⊢ opcyclesMap φ i ≫ L.descOpcycles k j hj hk = K.descOpcycles (φ.f i ≫ k) j hj ⋯

Tactic:
simp only [← cancel_epi (K.pOpcycles i), p_opcyclesMap_assoc, p_descOpcycles]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem nonempty_monotone_mem {s : Set α} (hs : s.Nonempty) :
    Nonempty { u // Monotone u ∧ ∀ i : ℕ, u i ∈ s }

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }

Tactic:
exact ⟨⟨fun _ => x, fun i j _ => le_rfl, fun _ => hx⟩⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
hs : s.Nonempty
⊢ Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }

Tactic:
obtain ⟨x, hx⟩ := hs

Result:
case intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem smul_mem_iff_mem (hc : c ≠ 0) :
    c • x ∈ fundamentalCone K ↔ x ∈ fundamentalCone K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
⊢ c • x ∈ fundamentalCone K ↔ x ∈ fundamentalCone K

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ smul_mem_of_mem h hc⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
h : c • x ∈ fundamentalCone K
⊢ x ∈ fundamentalCone K

Proof state:
case h.e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
h : c • x ∈ fundamentalCone K
⊢ x = c⁻¹ • c • x

Tactic:
rw [eq_inv_smul_iff₀ hc]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
h : c • x ∈ fundamentalCone K
⊢ x ∈ fundamentalCone K

Tactic:
convert smul_mem_of_mem h (inv_ne_zero hc)

Result:
case h.e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
h : c • x ∈ fundamentalCone K
⊢ x = c⁻¹ • c • x
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem Monic.ne_zero_of_ne (h : (0 : R) ≠ 1) {p : R[X]} (hp : p.Monic) : p ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
h : 0 ≠ 1
p : R[X]
hp : p.Monic
⊢ p ≠ 0

Tactic:
nontriviality R

Result:
R : Type u
inst✝¹ : Semiring R
h : 0 ≠ 1
p : R[X]
hp : p.Monic
inst✝ : Nontrivial R
⊢ p ≠ 0

Proof state:
R : Type u
inst✝¹ : Semiring R
h : 0 ≠ 1
p : R[X]
hp : p.Monic
inst✝ : Nontrivial R
⊢ p ≠ 0

Tactic:
exact hp.ne_zero

Result:
no goals
-- Mathlib/Algebra/Ring/Equiv.lean
theorem toRingHom_comp_symm_toRingHom (e : R ≃+* S) :
    e.toRingHom.comp e.symm.toRingHom = RingHom.id _

Proof state:
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
e : R ≃+* S
⊢ e.toRingHom.comp e.symm.toRingHom = RingHom.id S

Tactic:
ext

Result:
case a
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
e : R ≃+* S
x✝ : S
⊢ (e.toRingHom.comp e.symm.toRingHom) x✝ = (RingHom.id S) x✝

Proof state:
case a
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
e : R ≃+* S
x✝ : S
⊢ (e.toRingHom.comp e.symm.toRingHom) x✝ = (RingHom.id S) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isReflection_conj_iff (w t : W) :
    cs.IsReflection (w * t * w⁻¹) ↔ cs.IsReflection t

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
h : cs.IsReflection (w * t * w⁻¹)
⊢ cs.IsReflection t

Tactic:
simpa [← mul_assoc] using h.conj w⁻¹

Result:
no goals

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection (w * t * w⁻¹) → cs.IsReflection t

Tactic:
intro h

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
h : cs.IsReflection (w * t * w⁻¹)
⊢ cs.IsReflection t

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection (w * t * w⁻¹) ↔ cs.IsReflection t

Tactic:
constructor

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection (w * t * w⁻¹) → cs.IsReflection t

case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection t → cs.IsReflection (w * t * w⁻¹)

Proof state:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection t → cs.IsReflection (w * t * w⁻¹)

Tactic:
exact IsReflection.conj (w := w)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem coprime_zero_right (n : Nat) : Coprime n 0 ↔ n = 1

Proof state:
n : Nat
⊢ n.Coprime 0 ↔ n = 1

Tactic:
simp [Coprime]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
    (l.take n).dropLast = l.take (n - 1)

Proof state:
α : Type u_1
n : Nat
l : List α
h : n < l.length
⊢ (take n l).dropLast = take (n - 1) l

Tactic:
simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, Nat.min_eq_left, take_take, sub_le]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Sqrt.lean
theorem deriv_sqrt_aux {x : ℝ} (hx : x ≠ 0) :
    HasStrictDerivAt (√·) (1 / (2 * √x)) x ∧ ∀ n, ContDiffAt ℝ n (√·) x

Proof state:
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x

Tactic:
have : ↑2 * √x ^ (2 - 1) ≠ 0 := by simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]

Result:
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * √x ^ (2 - 1) ≠ 0
⊢ HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x

Proof state:
case inr.left
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * √x ^ (2 - 1) ≠ 0
⊢ HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x

Tactic:
simpa using sqPartialHomeomorph.hasStrictDerivAt_symm hx this (hasStrictDerivAt_pow 2 _)

Result:
no goals

Proof state:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
this : (fun x => √x) =ᶠ[𝓝 x] fun x => 0
⊢ HasStrictDerivAt (fun x => √x) 0 x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x

Tactic:
exact
  ⟨(hasStrictDerivAt_const x (0 : ℝ)).congr_of_eventuallyEq this.symm, fun n =>
    contDiffAt_const.congr_of_eventuallyEq this⟩

Result:
no goals

Proof state:
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ 2 * √x ^ (2 - 1) ≠ 0

Tactic:
simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]

Result:
no goals

Proof state:
case inr.right
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * √x ^ (2 - 1) ≠ 0
⊢ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x

Tactic:
exact fun n => sqPartialHomeomorph.contDiffAt_symm_deriv this hx (hasDerivAt_pow 2 (√x))
  (contDiffAt_id.pow 2)

Result:
no goals

Proof state:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x

Tactic:
rw [sqrt_eq_zero_of_nonpos hx.le, mul_zero, div_zero]

Result:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun x => √x) 0 x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x

Tactic:
rcases hx.lt_or_lt with hx | hx

Result:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x

case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x

Proof state:
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * √x ^ (2 - 1) ≠ 0
⊢ HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x

Tactic:
constructor

Result:
case inr.left
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * √x ^ (2 - 1) ≠ 0
⊢ HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x

case inr.right
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * √x ^ (2 - 1) ≠ 0
⊢ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x
-- Mathlib/Topology/ContinuousMap/Weierstrass.lean
theorem continuousMap_mem_polynomialFunctions_closure (a b : ℝ) (f : C(Set.Icc a b, ℝ)) :
    f ∈ (polynomialFunctions (Set.Icc a b)).topologicalClosure

Proof state:
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ (polynomialFunctions (Set.Icc a b)).topologicalClosure

Tactic:
rw [polynomialFunctions_closure_eq_top _ _]

Result:
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ ⊤

Proof state:
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem expSeries_div_hasSum_exp_of_mem_ball [CompleteSpace 𝔸] (x : 𝔸)
    (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasSum (fun n => x ^ n / n !) (exp 𝕂 x)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n => x ^ n / ↑n !) (exp 𝕂 x)

Tactic:
rw [← expSeries_apply_eq_div' (𝕂 := 𝕂) x]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x) (exp 𝕂 x)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : NontriviallyNormedField 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius
⊢ HasSum (fun n => (expSeries 𝕂 𝔸 n) fun x_1 => x) (exp 𝕂 x)

Tactic:
exact expSeries_hasSum_exp_of_mem_ball x hx

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem squarefree_and_prime_pow_iff_prime {n : ℕ} : Squarefree n ∧ IsPrimePow n ↔ Prime n

Proof state:
n : ℕ
⊢ Squarefree n ∧ IsPrimePow n ↔ Prime n

Tactic:
refine ⟨?_, fun hn => ⟨hn.squarefree, hn.isPrimePow⟩⟩

Result:
n : ℕ
⊢ Squarefree n ∧ IsPrimePow n → Prime n

Proof state:
n : ℕ
⊢ (Squarefree n ∧ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n

Tactic:
rintro ⟨h, p, k, hp, hk, rfl⟩

Result:
case intro.intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree (p ^ k)
⊢ Prime (p ^ k)

Proof state:
case intro.intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree (p ^ k)
⊢ Prime (p ^ k)

Tactic:
rw [squarefree_pow_iff hp.ne_one hk.ne'] at h

Result:
case intro.intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)

Proof state:
case intro.intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)

Tactic:
rwa [h.2, pow_one]

Result:
no goals

Proof state:
n : ℕ
⊢ Squarefree n ∧ IsPrimePow n → Prime n

Tactic:
rw [isPrimePow_nat_iff]

Result:
n : ℕ
⊢ (Squarefree n ∧ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem finInsepDegree_top : finInsepDegree F (⊤ : IntermediateField E K) = finInsepDegree F K

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
⊢ finInsepDegree F ↥⊤ = finInsepDegree F K

Tactic:
rw [finInsepDegree_def', insepDegree_top, ← finInsepDegree_def']

Result:
no goals