harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem dickson_one_one_eval_add_inv (x y : R) (h : x * y = 1) :
    ∀ n, (dickson 1 (1 : R) n).eval (x + y) = x ^ n + y ^ n
  | 0 => by
    simp only [eval_one, eval_add, pow_zero, dickson_zero]; norm_num
  | 1 => by simp only [eval_X, dickson_one, pow_one]
  | n + 2 => by
    simp only [eval_sub, eval_mul, dickson_one_one_eval_add_inv x y h _, eval_X, dickson_add_two,
      C_1, eval_one]
    conv_lhs => simp only [pow_succ', add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]
    ring

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
⊢ eval (x + y) (3 - ↑1) = 1 + 1

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ eval (x + y) (dickson 1 1 (n + 2)) = x ^ (n + 2) + y ^ (n + 2)

Tactic:
simp only [eval_sub, eval_mul, dickson_one_one_eval_add_inv x y h _, eval_X, dickson_add_two,
  C_1, eval_one]

Result:
R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
⊢ eval (x + y) (dickson 1 1 1) = x ^ 1 + y ^ 1

Tactic:
simp only [eval_X, dickson_one, pow_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
⊢ eval (x + y) (dickson 1 1 0) = x ^ 0 + y ^ 0

Tactic:
simp only [eval_one, eval_add, pow_zero, dickson_zero]

Result:
R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
⊢ eval (x + y) (3 - ↑1) = 1 + 1

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)

Tactic:
conv_lhs => simp only [pow_succ', add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]

Result:
R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)

Tactic:
ring

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean
lemma opShiftFunctorEquivalence_zero_unitIso_inv_app (X : Cᵒᵖ) :
    (opShiftFunctorEquivalence C 0).unitIso.inv.app X =
      (((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop⟦(0 : ℤ)⟧').op ≫
        ((shiftFunctorZero C ℤ).inv.app X.unop).op

Proof state:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 0).unitIso.inv.app X).unop =
    (((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop).op ≫
        ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op).unop

Tactic:
dsimp [opShiftFunctorEquivalence]

Result:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctorCompIsoId C 0 0 ⋯).inv.app (Opposite.unop X) ≫
      (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop =
    (shiftFunctorZero C ℤ).inv.app (Opposite.unop X) ≫ (shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop

Proof state:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctorCompIsoId C 0 0 ⋯).inv.app (Opposite.unop X) ≫
      (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop =
    (shiftFunctorZero C ℤ).inv.app (Opposite.unop X) ≫ (shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop

Tactic:
rw [shiftFunctorZero_op_hom_app, unop_comp, Quiver.Hom.unop_op, Functor.map_comp,
  shiftFunctorCompIsoId_zero_zero_inv_app, assoc]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (opShiftFunctorEquivalence C 0).unitIso.inv.app X =
    ((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop).op ≫
      ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op

Tactic:
apply Quiver.Hom.unop_inj

Result:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 0).unitIso.inv.app X).unop =
    (((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop).op ≫
        ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op).unop
-- Mathlib/Algebra/Regular/SMul.lean
theorem of_smul (a : R) (ab : IsSMulRegular M (a • s)) : IsSMulRegular M s :=
  @Function.Injective.of_comp _ _ _ (fun m : M => a • m) _ fun c d cd => by
  dsimp only [Function.comp_def] at cd
  rw [← smul_assoc, ← smul_assoc] at cd
  exact ab cd

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : (a • s) • c = (a • s) • d
⊢ c = d

Tactic:
exact ab cd

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : ((fun m => a • m) ∘ fun x => s • x) c = ((fun m => a • m) ∘ fun x => s • x) d
⊢ c = d

Tactic:
dsimp only [Function.comp_def] at cd

Result:
R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : a • s • c = a • s • d
⊢ c = d

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : a • s • c = a • s • d
⊢ c = d

Tactic:
rw [← smul_assoc, ← smul_assoc] at cd

Result:
R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : (a • s) • c = (a • s) • d
⊢ c = d
-- Mathlib/Algebra/Module/FinitePresentation.lean
lemma FinitePresentation.of_isBaseChange
    {A} [CommRing A] [Algebra R A] [Module A N] [IsScalarTower R A N]
    (f : M →ₗ[R] N) (h : IsBaseChange A f) [Module.FinitePresentation R M] :
    Module.FinitePresentation A N :=
  Module.finitePresentation_of_surjective
    h.equiv.toLinearMap h.equiv.surjective (by simpa using Submodule.fg_bot)

Proof state:
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module A N
inst✝¹ : IsScalarTower R A N
f : M →ₗ[R] N
h : IsBaseChange A f
inst✝ : Module.FinitePresentation R M
⊢ (LinearMap.ker ↑h.equiv).FG

Tactic:
simpa using Submodule.fg_bot

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem find?_congr [@TransCmp α cmp] (t : RBSet α cmp) (h : cmp v₁ v₂ = .eq) :
    t.find? v₁ = t.find? v₂

Proof state:
α : Type u_1
cmp : α → α → Ordering
v₁ v₂ : α
inst✝ : TransCmp cmp
t : RBSet α cmp
h : cmp v₁ v₂ = Ordering.eq
⊢ t.find? v₁ = t.find? v₂

Tactic:
simp [find?, TransCmp.cmp_congr_left' h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
lemma measure_preimage_fst_singleton_eq_sum [Fintype β] (μ : Measure (α × β)) (x : α) :
    μ (Prod.fst ⁻¹' {x}) = ∑ y, μ {(x, y)}

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Fintype β
μ : Measure (α × β)
x : α
⊢ μ (Prod.fst ⁻¹' {x}) = ∑ y : β, μ {(x, y)}

Tactic:
rw [measure_preimage_fst_singleton_eq_tsum μ x, tsum_fintype]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_eq_append_iff {xs ys zs : List α} :
    xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse

Proof state:
α : Type u_1
xs ys zs : List α
⊢ xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse

Tactic:
rw [reverse_eq_iff, reverse_append]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem edgeDensity_empty_right (s : Finset α) : edgeDensity r s ∅ = 0

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
⊢ edgeDensity r s ∅ = 0

Tactic:
rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem reindexFinsetRange_repr (x : M) (i : ι)
    (h := Finset.mem_image_of_mem b (Finset.mem_univ i)) :
    b.reindexFinsetRange.repr x ⟨b i, h⟩ = b.repr x i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
x : M
i : ι
h : optParam (b i ∈ Finset.image (⇑b) Finset.univ) ⋯
⊢ (b.reindexFinsetRange.repr x) ⟨b i, h⟩ = (b.repr x) i

Tactic:
simp [reindexFinsetRange]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem prodMonoidal_rightUnitor_inv_snd (X : C₁ × C₂) :
    ((ρ_ X).inv : X ⟶ X ⊗ 𝟙_ _).2 = (ρ_ X.2).inv

Proof state:
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (ρ_ X).inv.2 = (ρ_ X.2).inv

Tactic:
cases X

Result:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).inv.2 = (ρ_ (fst✝, snd✝).2).inv

Proof state:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (ρ_ (fst✝, snd✝)).inv.2 = (ρ_ (fst✝, snd✝).2).inv

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Rademacher.lean
theorem ae_differentiableWithinAt_of_mem_of_real (hf : LipschitzOnWith C f s) :
    ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Proof state:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
g : E → ℝ
g_lip : LipschitzWith C g
hg : EqOn f g s
x : E
hx : DifferentiableAt ℝ g x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
exact hx.differentiableWithinAt.congr hg (hg xs)

Result:
no goals

Proof state:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
g : E → ℝ
g_lip : LipschitzWith C g
hg : EqOn f g s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
filter_upwards [g_lip.ae_differentiableAt_of_real] with x hx xs

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
g : E → ℝ
g_lip : LipschitzWith C g
hg : EqOn f g s
x : E
hx : DifferentiableAt ℝ g x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
obtain ⟨g, g_lip, hg⟩ : ∃ (g : E → ℝ), LipschitzWith C g ∧ EqOn f g s := hf.extend_real

Result:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
g : E → ℝ
g_lip : LipschitzWith C g
hg : EqOn f g s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expectWith_congr (hst : s = t) (hpq : ∀ i ∈ t, p i ↔ q i) (h : ∀ i ∈ t, q i → f i = g i) :
    𝔼 i ∈ s with p i, f i = 𝔼 i ∈ t with q i, g i :=
  expect_congr (by rw [hst, filter_inj'.2 hpq]) <| by simpa using h

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ filter (fun i => p i) s = filter (fun i => q i) t

Tactic:
rw [hst, filter_inj'.2 hpq]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ ∀ i ∈ filter (fun i => q i) t, f i = g i

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem square_commutes : SumEval C ho ∘ Sum.inl =
    ModuleCat.ofHom (πs C o) ∘ eval (π C (ord I · < o))

Proof state:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑C
⊢ ((πs C o) (Products.eval (π C fun x => ord I x < o) ↑l)) x✝ =
    (eval (π C fun x => ord I x < o) l) (ProjRestrict C (fun x => ord I x < o) x✝)

Tactic:
rfl

Result:
no goals

Proof state:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑C
⊢ ((SumEval C ho ∘ Sum.inl) l) x✝ =
    ((⇑(ConcreteCategory.hom (ModuleCat.ofHom (πs C o))) ∘ eval (π C fun x => ord I x < o)) l) x✝

Tactic:
dsimp [SumEval]

Result:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑C
⊢ (Products.eval C ↑l) x✝ = (eval (π C fun x => ord I x < o) l) (ProjRestrict C (fun x => ord I x < o) x✝)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ SumEval C ho ∘ Sum.inl = ⇑(ConcreteCategory.hom (ModuleCat.ofHom (πs C o))) ∘ eval (π C fun x => ord I x < o)

Tactic:
ext l

Result:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑C
⊢ ((SumEval C ho ∘ Sum.inl) l) x✝ =
    ((⇑(ConcreteCategory.hom (ModuleCat.ofHom (πs C o))) ∘ eval (π C fun x => ord I x < o)) l) x✝

Proof state:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑C
⊢ (Products.eval C ↑l) x✝ = (eval (π C fun x => ord I x < o) l) (ProjRestrict C (fun x => ord I x < o) x✝)

Tactic:
rw [← Products.eval_πs C (Products.prop_of_isGood  _ _ l.prop)]

Result:
case h.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑C
⊢ ((πs C o) (Products.eval (π C fun x => ord I x < o) ↑l)) x✝ =
    (eval (π C fun x => ord I x < o) l) (ProjRestrict C (fun x => ord I x < o) x✝)
-- Mathlib/FieldTheory/Separable.lean
theorem separable_iff_derivative_ne_zero {f : F[X]} (hf : Irreducible f) :
    f.Separable ↔ derivative f ≠ 0 :=
  ⟨fun h1 h2 => hf.not_unit <| isCoprime_zero_right.1 <| h2 ▸ h1, fun h =>
    EuclideanDomain.isCoprime_of_dvd (mt And.right h) fun g hg1 _hg2 ⟨p, hg3⟩ hg4 =>
      let ⟨u, hu⟩ := (hf.isUnit_or_isUnit hg3).resolve_left hg1
      have : f ∣ derivative f

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ f ∣ derivative f

Tactic:
conv_lhs => rw [hg3, ← hu]

Result:
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ g * ↑u ∣ derivative f

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ g * ↑u ∣ derivative f

Tactic:
rwa [Units.mul_right_dvd]

Result:
no goals
-- Mathlib/Probability/Process/Filtration.lean
theorem stronglyMeasurable_limitProcess : StronglyMeasurable[⨆ n, ℱ n] (limitProcess f ℱ μ)

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable
    (if h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) then Classical.choose h
    else 0)

Tactic:
split_ifs with h

Result:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable (Classical.choose h)

case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ¬∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable 0

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable (Classical.choose h)

case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ¬∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable 0

Tactic:
exacts [(Classical.choose_spec h).1, stronglyMeasurable_zero]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable (limitProcess f ℱ μ)

Tactic:
rw [limitProcess]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable
    (if h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) then Classical.choose h
    else 0)
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem erase_monomial {n : ℕ} {a : R} : erase n (monomial n a) = 0 :=
  toFinsupp_injective <| by simp

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (erase n ((monomial n) a)).toFinsupp = toFinsupp 0

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem up_neg : 0 < up

Proof state:
⊢ 0 ≤ up ∧ ∃ i, ∀ (j : (up.moveLeft i).RightMoves), 0 ⧏ (up.moveLeft i).moveRight j

Tactic:
simp [zero_le_lf, zero_lf_star]

Result:
no goals

Proof state:
⊢ 0 < up

Tactic:
rw [lt_iff_le_and_lf, zero_lf]

Result:
⊢ 0 ≤ up ∧ ∃ i, ∀ (j : (up.moveLeft i).RightMoves), 0 ⧏ (up.moveLeft i).moveRight j
-- Mathlib/CategoryTheory/Action/Limits.lean
/-- `F : C ⥤ SingleObj G ⥤ V` preserves the colimit of some `K : J ⥤ C` if it does
evaluated at `SingleObj.star G`. -/
private lemma SingleObj.preservesColimit (F : C ⥤ SingleObj G ⥤ V)
    {J : Type w₁} [Category.{w₂} J] (K : J ⥤ C)
    (h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))) :
    PreservesColimit K F

Proof state:
case H
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ SingleObj G ⥤ V
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ ∀ (k : SingleObj G), PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj k)

Tactic:
intro _

Result:
case H
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ SingleObj G ⥤ V
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
k✝ : SingleObj G
⊢ PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj k✝)

Proof state:
case H
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ SingleObj G ⥤ V
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
k✝ : SingleObj G
⊢ PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj k✝)

Tactic:
exact h

Result:
no goals

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ SingleObj G ⥤ V
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_evaluation

Result:
case H
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ SingleObj G ⥤ V
J : Type w₁
inst✝ : Category.{w₂, w₁} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ ∀ (k : SingleObj G), PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj k)
-- Mathlib/FieldTheory/Galois/Basic.lean
theorem map_fixingSubgroup (σ : L ≃ₐ[K] L) :
    (E.map σ).fixingSubgroup = (MulAut.conj σ) • E.fixingSubgroup

Proof state:
case h
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
σ τ : L ≃ₐ[K] L
⊢ τ ∈ (map (↑σ) E).fixingSubgroup ↔ τ ∈ MulAut.conj σ • E.fixingSubgroup

Tactic:
simp only [coe_map, AlgHom.coe_coe, Set.mem_image, SetLike.mem_coe, AlgEquiv.smul_def,
  forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, Subtype.forall,
  Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← symm_apply_eq,
  IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff]

Result:
case h
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
σ τ : L ≃ₐ[K] L
⊢ (∀ a ∈ E, σ.symm (τ (σ a)) = a) ↔ ∀ y ∈ E, ((MulAut.conj σ)⁻¹ • τ) y = y

Proof state:
case h
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
σ τ : L ≃ₐ[K] L
⊢ (∀ a ∈ E, σ.symm (τ (σ a)) = a) ↔ ∀ y ∈ E, ((MulAut.conj σ)⁻¹ • τ) y = y

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
σ : L ≃ₐ[K] L
⊢ (map (↑σ) E).fixingSubgroup = MulAut.conj σ • E.fixingSubgroup

Tactic:
ext τ

Result:
case h
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
σ τ : L ≃ₐ[K] L
⊢ τ ∈ (map (↑σ) E).fixingSubgroup ↔ τ ∈ MulAut.conj σ • E.fixingSubgroup
-- Mathlib/Topology/Order/LeftRight.lean
theorem nhdsLT_sup_nhdsGE (a : α) : 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a

Tactic:
rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]

Result:
no goals