harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_inter_add_diff₀ (ht : NullMeasurableSet t μ) (hfs : IntegrableOn f s μ) :
    ∫ x in s ∩ t, f x ∂μ + ∫ x in s \ t, f x ∂μ = ∫ x in s, f x ∂μ

Proof state:
case hν
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ Integrable f (μ.restrict (s \ t))

Tactic:
exact Integrable.mono_measure hfs (Measure.restrict_mono diff_subset le_rfl)

Result:
no goals

Proof state:
case hμ
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
exact Integrable.mono_measure hfs (Measure.restrict_mono inter_subset_left le_rfl)

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ ∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
rw [← Measure.restrict_inter_add_diff₀ s ht, integral_add_measure]

Result:
case hμ
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ Integrable f (μ.restrict (s ∩ t))

case hν
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ Integrable f (μ.restrict (s \ t))
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionBy_isInternal {q : ι → R} (hq : (S : Set ι).Pairwise <| (IsCoprime on q))
    (hM : Module.IsTorsionBy R M <| ∏ i ∈ S, q i) :
    DirectSum.IsInternal fun i : S => torsionBy R M <| q i

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : Module.IsTorsionBy R M (∏ i ∈ S, q i)
⊢ DirectSum.IsInternal fun i => torsionBy R M (q ↑i)

Tactic:
rw [← Module.isTorsionBySet_span_singleton_iff, Ideal.submodule_span_eq, ←
  Ideal.finset_inf_span_singleton _ _ hq, Finset.inf_eq_iInf] at hM

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : Module.IsTorsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})
⊢ DirectSum.IsInternal fun i => torsionBy R M (q ↑i)

Proof state:
case h.e'_8.h
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : Module.IsTorsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})
x✝ : { x // x ∈ S }
⊢ torsionBy R M (q ↑x✝) = torsionBySet R M ↑(Ideal.span {q ↑x✝})

Tactic:
exact (torsionBySet_span_singleton_eq _ (R := R) (M := M)).symm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : Module.IsTorsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})
⊢ DirectSum.IsInternal fun i => torsionBy R M (q ↑i)

Tactic:
convert torsionBySet_isInternal
    (fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij) hM

Result:
case h.e'_8.h
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : Module.IsTorsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})
x✝ : { x // x ∈ S }
⊢ torsionBy R M (q ↑x✝) = torsionBySet R M ↑(Ideal.span {q ↑x✝})
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
@[simp]
lemma singularPart_zero_right (μ : Measure α) : μ.singularPart 0 = μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ.singularPart 0 = μ.singularPart 0 + withDensity 0 (μ.rnDeriv 0)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ.singularPart 0 = μ

Tactic:
conv_rhs => rw [haveLebesgueDecomposition_add μ 0]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ.singularPart 0 = μ.singularPart 0 + withDensity 0 (μ.rnDeriv 0)
-- Mathlib/Data/Set/Pointwise/Support.lean
theorem support_comp_inv_smul₀ [Zero γ] {c : α} (hc : c ≠ 0) (f : β → γ) :
    (support fun x ↦ f (c⁻¹ • x)) = c • support f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
hc : c ≠ 0
f : β → γ
⊢ (support fun x => f (c⁻¹ • x)) = c • support f

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
hc : c ≠ 0
f : β → γ
x : β
⊢ (x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
hc : c ≠ 0
f : β → γ
x : β
⊢ (x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f

Tactic:
simp only [mem_smul_set_iff_inv_smul_mem₀ hc, mem_support]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem snd_pow_of_smul_comm [Monoid R] [AddMonoid M] [DistribMulAction R M]
    [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : tsze R M) (n : ℕ)
    (h : x.snd <• x.fst = x.fst •> x.snd) : snd (x ^ n) = n • x.fst ^ n.pred •> x.snd

Proof state:
case refine_1
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
⊢ ∀ x_1 ∈ List.map (fun i => x.fst ^ (n - i + i) •> x.snd) (List.range n.succ), x_1 = x.fst ^ n •> x.snd

Tactic:
rintro m hm

Result:
case refine_1
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
m : M
hm : m ∈ List.map (fun i => x.fst ^ (n - i + i) •> x.snd) (List.range n.succ)
⊢ m = x.fst ^ n •> x.snd
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullback_diagonal_map_snd_snd_fst :
    (pullback.snd (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i
        (by simp [condition]) (by simp [condition]))) ≫
      snd _ _ ≫ i₂ ≫ fst _ _ =
      pullback.fst _ _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯)

Tactic:
conv_rhs => rw [← Category.comp_id (pullback.fst _ _)]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.337738, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ (i₂ ≫ snd f i) ≫ i = (i₂ ≫ fst f i) ≫ f

Tactic:
simp [condition]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X

Tactic:
rw [← diagonal_snd f, pullback.condition_assoc, pullback.lift_snd]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.337738, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ (i₁ ≫ snd f i) ≫ i = (i₁ ≫ fst f i) ≫ f

Tactic:
simp [condition]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem finset_span_isCompactElement (S : Finset M) :
    CompleteLattice.IsCompactElement (span R S : Submodule R M)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Finset M
⊢ CompleteLattice.IsCompactElement (span R ↑S)

Tactic:
rw [span_eq_iSup_of_singleton_spans]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Finset M
⊢ CompleteLattice.IsCompactElement (⨆ x ∈ ↑S, span R {x})

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Finset M
⊢ CompleteLattice.IsCompactElement (⨆ x ∈ ↑S, span R {x})

Tactic:
simp only [Finset.mem_coe]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Finset M
⊢ CompleteLattice.IsCompactElement (⨆ x ∈ S, span R {x})

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Finset M
⊢ CompleteLattice.IsCompactElement (⨆ x ∈ S, span R {x})

Tactic:
rw [← Finset.sup_eq_iSup]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Finset M
⊢ CompleteLattice.IsCompactElement (S.sup fun x => span R {x})

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Finset M
⊢ CompleteLattice.IsCompactElement (S.sup fun x => span R {x})

Tactic:
exact
  CompleteLattice.isCompactElement_finsetSup S fun x _ => singleton_span_isCompactElement x

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem Continuous.map_borel_eq {X Y : Type*} [TopologicalSpace X] [PolishSpace X]
    [TopologicalSpace Y] [T0Space Y] [SecondCountableTopology Y] {f : X → Y} (hf : Continuous f)
    (hsurj : Surjective f) : MeasurableSpace.map f (borel X) = borel Y

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : PolishSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T0Space Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Continuous f
hsurj : Surjective f
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ MeasurableSpace.map f (borel X) = borel Y

Tactic:
exact hf.map_eq_borel hsurj

Result:
no goals

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : PolishSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T0Space Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Continuous f
hsurj : Surjective f
⊢ MeasurableSpace.map f (borel X) = borel Y

Tactic:
borelize X

Result:
X : Type u_3
Y : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : PolishSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T0Space Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Continuous f
hsurj : Surjective f
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ MeasurableSpace.map f (borel X) = borel Y
-- Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean
theorem path_nonempty_of_hom {G} [Groupoid.{u, u} G] [IsFreeGroupoid G] {a b : G} :
    Nonempty (a ⟶ b) → Nonempty (Path (symgen a) (symgen b))

Proof state:
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ F.map (of e✝) = ((Functor.const G).obj ()).map (of e✝)

Tactic:
rw [Functor.const_obj_map, id_as_one, differenceFunctor_map, @mul_inv_eq_one _ _ (f _)]

Result:
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ f b✝ =
    f
      (let_fun this := a✝;
      this)

Proof state:
case intro.h.e_5.h.e_self
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
⊢ F = (Functor.const G).obj ()

Tactic:
ext

Result:
case intro.h.e_5.h.e_self.h
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ F.map (of e✝) = ((Functor.const G).obj ()).map (of e✝)

Proof state:
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ (let_fun this := a✝;
    this) ⟶
    b✝

Tactic:
assumption

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Sublist.lean
theorem append_right_sublist_self (xs : List α) {ys : List α} : xs ++ ys <+ xs ↔ ys = []

Proof state:
α : Type u_1
xs ys : List α
⊢ xs ++ ys <+ xs ↔ ys = []

Tactic:
constructor

Result:
case mp
α : Type u_1
xs ys : List α
⊢ xs ++ ys <+ xs → ys = []

case mpr
α : Type u_1
xs ys : List α
⊢ ys = [] → xs ++ ys <+ xs

Proof state:
case mp
α : Type u_1
xs ys : List α
h : xs.length + ys.length ≤ xs.length
⊢ ys = []

Tactic:
have : ys.length = 0 := by omega

Result:
case mp
α : Type u_1
xs ys : List α
h : xs.length + ys.length ≤ xs.length
this : ys.length = 0
⊢ ys = []

Proof state:
case mpr
α : Type u_1
xs ys : List α
⊢ ys = [] → xs ++ ys <+ xs

Tactic:
rintro rfl

Result:
case mpr
α : Type u_1
xs : List α
⊢ xs ++ [] <+ xs

Proof state:
α : Type u_1
xs ys : List α
h : xs.length + ys.length ≤ xs.length
⊢ ys.length = 0

Tactic:
omega

Result:
no goals

Proof state:
case mpr
α : Type u_1
xs : List α
⊢ xs ++ [] <+ xs

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_1
xs ys : List α
h : xs.length + ys.length ≤ xs.length
this : ys.length = 0
⊢ ys = []

Tactic:
simp_all

Result:
no goals

Proof state:
case mp
α : Type u_1
xs ys : List α
⊢ xs ++ ys <+ xs → ys = []

Tactic:
intro h

Result:
case mp
α : Type u_1
xs ys : List α
h : xs ++ ys <+ xs
⊢ ys = []

Proof state:
case mp
α : Type u_1
xs ys : List α
h : xs ++ ys <+ xs
⊢ ys = []

Tactic:
replace h := h.length_le

Result:
case mp
α : Type u_1
xs ys : List α
h : (xs ++ ys).length ≤ xs.length
⊢ ys = []

Proof state:
case mp
α : Type u_1
xs ys : List α
h : (xs ++ ys).length ≤ xs.length
⊢ ys = []

Tactic:
simp only [length_append] at h

Result:
case mp
α : Type u_1
xs ys : List α
h : xs.length + ys.length ≤ xs.length
⊢ ys = []
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.of_aeval {r : A} (f : R[X]) (hf : f.natDegree ≠ 0)
    (hf' : f.leadingCoeff ∈ nonZeroDivisors R) (H : IsAlgebraic R (aeval r f)) :
    IsAlgebraic R r

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ nonZeroDivisors R
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
this : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0
h : p.comp f = 0
⊢ (p.comp f).coeff (p.natDegree * f.natDegree) = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case intro.intro
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ nonZeroDivisors R
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
this : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0
⊢ IsAlgebraic R r

Tactic:
exact ⟨p.comp f, fun h ↦ this (by simp [h]), by rwa [aeval_comp]⟩

Result:
no goals

Proof state:
case intro.intro
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ nonZeroDivisors R
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
⊢ IsAlgebraic R r

Tactic:
have : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0 := fun h ↦ h1 <| by
  rwa [coeff_comp_degree_mul_degree hf,
    mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
    leadingCoeff_eq_zero] at h

Result:
case intro.intro
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ nonZeroDivisors R
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
this : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0
⊢ IsAlgebraic R r

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ nonZeroDivisors R
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
this : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0
⊢ (aeval r) (p.comp f) = 0

Tactic:
rwa [aeval_comp]

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ nonZeroDivisors R
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
h : (p.comp f).coeff (p.natDegree * f.natDegree) = 0
⊢ p = 0

Tactic:
rwa [coeff_comp_degree_mul_degree hf,
  mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
  leadingCoeff_eq_zero] at h

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ nonZeroDivisors R
H : IsAlgebraic R ((aeval r) f)
⊢ IsAlgebraic R r

Tactic:
obtain ⟨p, h1, h2⟩ := H

Result:
case intro.intro
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ nonZeroDivisors R
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
⊢ IsAlgebraic R r
-- Mathlib/Data/Nat/Factorization/Basic.lean
/-- There are exactly `⌊N/n⌋` positive multiples of `n` that are `≤ N`.
See `Nat.card_multiples` for a "shifted-by-one" version. -/
lemma card_multiples' (N n : ℕ) : #{k ∈ range N.succ | k ≠ 0 ∧ n ∣ k} = N / n

Proof state:
case zero
n : ℕ
⊢ #(Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (succ 0))) = 0 / n

Tactic:
simp [Finset.filter_false_of_mem]

Result:
no goals

Proof state:
case pos
n N : ℕ
ih : #(Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range N.succ)) = N / n
h : n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) (Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1)))
      else Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1))) =
    (N + 1) / n

Tactic:
simp [h, succ_div_of_dvd, ih]

Result:
no goals

Proof state:
case succ
n N : ℕ
ih : #(Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range N.succ)) = N / n
⊢ #(Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1).succ)) = (N + 1) / n

Tactic:
rw [Finset.range_succ, Finset.filter_insert]

Result:
case succ
n N : ℕ
ih : #(Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range N.succ)) = N / n
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) (Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1)))
      else Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1))) =
    (N + 1) / n

Proof state:
case neg
n N : ℕ
ih : #(Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range N.succ)) = N / n
h : ¬n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) (Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1)))
      else Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1))) =
    (N + 1) / n

Tactic:
simp [h, succ_div_of_not_dvd, ih]

Result:
no goals

Proof state:
case succ
n N : ℕ
ih : #(Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range N.succ)) = N / n
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) (Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1)))
      else Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1))) =
    (N + 1) / n

Tactic:
by_cases h : n ∣ N.succ

Result:
case pos
n N : ℕ
ih : #(Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range N.succ)) = N / n
h : n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) (Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1)))
      else Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1))) =
    (N + 1) / n

case neg
n N : ℕ
ih : #(Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range N.succ)) = N / n
h : ¬n ∣ N.succ
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) (Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1)))
      else Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range (N + 1))) =
    (N + 1) / n
-- Mathlib/Data/List/InsertIdx.lean
theorem eq_or_mem_of_mem_insertIdx {l : List α} {n : ℕ} {a b : α} (h : a ∈ insertIdx n b l) :
    a = b ∨ a ∈ l

Proof state:
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ insertIdx n b l
⊢ a = b ∨ a ∈ l

Tactic:
cases Nat.lt_or_ge (length l) n with
| inl hn =>
  rw [insertIdx_of_length_lt _ _ _ hn] at h
  exact .inr h
| inr hn =>
  rwa [mem_insertIdx hn] at h

Result:
no goals

Proof state:
case inl
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l
hn : l.length < n
⊢ a = b ∨ a ∈ l

Tactic:
exact .inr h

Result:
no goals

Proof state:
case inr
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ insertIdx n b l
hn : l.length ≥ n
⊢ a = b ∨ a ∈ l

Tactic:
rwa [mem_insertIdx hn] at h

Result:
no goals

Proof state:
case inl
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ insertIdx n b l
hn : l.length < n
⊢ a = b ∨ a ∈ l

Tactic:
rw [insertIdx_of_length_lt _ _ _ hn] at h

Result:
case inl
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l
hn : l.length < n
⊢ a = b ∨ a ∈ l
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma monotoneOn_of_le_succ (hs : s.OrdConnected)
    (hf : ∀ a, ¬ IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)) : MonotoneOn f s

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
⊢ MonotoneOn f s

Tactic:
rintro a ha b hb hab

Result:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f a ≤ f b