mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
⊢ ∫ (x : ℝ × ℝ) in Set.Icc a b, (f' x) (1, 0) + (g' x) (0, 1) =
    ∑ i,
      ((∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
          ![f, g] i (e.symm (i.insertNth (e b i) x))) -
        ∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
          ![f, g] i (e.symm (i.insertNth (e a i) x)))

Tactic:
refine integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ ![f, g]
        ![f', g'] s hs a b hle ?_ (fun x hx => ?_) _ ?_ Hi
      · exact fun x y => (OrderIso.finTwoArrowIso ℝ).symm.le_iff_le
      · exact (volume_preserving_finTwoArrow ℝ).symm _
      · exact Fin.forall_fin_two.2 ⟨Hcf, Hcg⟩
      · rw [Icc_prod_eq, interior_prod_eq, interior_Icc, interior_Icc] at hx
        exact Fin.forall_fin_two.2 ⟨Hdf x hx, Hdg x hx⟩
      · intro x; rw [Fin.sum_univ_two]; rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
φ : K →+* ℂ
hφ : IsReal φ
⊢ (φ 1).re = 1

Tactic:
by simp only [map_one, one_re]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝² : Field K
k : Type u_2
inst✝¹ : Field k
inst✝ : Algebra k K
φ : K →+* ℂ
σ : Gal(K/k)
h : IsConj φ σ
x : k
⊢ (star (φ.comp (algebraMap k K))) x = (φ.comp (algebraMap k K)) x

Tactic:
simp only [conjugate_coe_eq, RingHom.coe_comp, Function.comp_apply, ← h.eq,
    starRingEnd_apply, AlgEquiv.commutes]

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  { toFun := fun x ↦ Units.mk0 (NNReal.mk (2 ^ (↑x).log) ⋯) ⋯, map_one' := ⋯, map_mul' := ⋯ }
⊢ StrictMono ⇑(map' (rf.comp e))

Tactic:
refine map'_strictMono ?_

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  { toFun := fun x ↦ Units.mk0 (NNReal.mk (2 ^ (↑x).log) ⋯) ⋯, map_one' := ⋯, map_mul' := ⋯ }
⊢ StrictMono ⇑(rf.comp e)
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
δ : ℝ≥0 := (RankOne.hom v) ↑ε
hδ : δ = (RankOne.hom v) ↑ε
⊢ 0 < (RankOne.hom v) ↑ε

Tactic:
← map_zero hv.hom

Goal state after:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
δ : ℝ≥0 := (RankOne.hom v) ↑ε
hδ : δ = (RankOne.hom v) ↑ε
⊢ (RankOne.hom v) 0 < (RankOne.hom v) ↑ε
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
⊢ 1 < absNorm v.asIdeal

Tactic:
by_contra! h

Goal state after:
R : Type u_2
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
h : absNorm v.asIdeal ≤ 1
⊢ False
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: case right
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : ↑I.multicospan.sections
r : J.R
⊢ ↑((fun s ↦
            ⟨fun i ↦
              match i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)),
              ⋯⟩)
          ((fun s ↦ { val := fun i ↦ ↑s (WalkingMulticospan.left i), property := ⋯ }) s))
      (WalkingMulticospan.right r) =
    ↑s (WalkingMulticospan.right r)

Tactic:
· exact s.property (.fst r)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
hr : Presieve.Arrows.Compatible F E.f s
s' : Presieve.FamilyOfElements F (Presieve.ofArrows E.X E.f)
hs' : ∀ (i : E.I₀), s' (E.f i) ⋯ = s i
t' : F.obj (op X)
ht' : ∀ (i : E.I₀), (ConcreteCategory.hom (F.map (E.f i).op)) t' = s i
hunique :
  ∀ (y : (fun X ↦ X) (F.obj (op X))),
    (fun t ↦ ∀ (i : E.I₀), (ConcreteCategory.hom (F.map (E.f i).op)) t = s i) y → y = t'
y : F.obj (op X)
hy : (fun t_1 ↦ t.IsAmalgamation t_1) y
⊢ y = t'

Tactic:
refine hunique _ fun i ↦ huniq _ _ fun Z g hg ↦ ?_

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
hr : Presieve.Arrows.Compatible F E.f s
s' : Presieve.FamilyOfElements F (Presieve.ofArrows E.X E.f)
hs' : ∀ (i : E.I₀), s' (E.f i) ⋯ = s i
t' : F.obj (op X)
ht' : ∀ (i : E.I₀), (ConcreteCategory.hom (F.map (E.f i).op)) t' = s i
hunique :
  ∀ (y : (fun X ↦ X) (F.obj (op X))),
    (fun t ↦ ∀ (i : E.I₀), (ConcreteCategory.hom (F.map (E.f i).op)) t = s i) y → y = t'
y : F.obj (op X)
hy : (fun t_1 ↦ t.IsAmalgamation t_1) y
i : E.I₀
Z : C
g : Z ⟶ E.X i
hg : (Sieve.pullback (E.f i) S).arrows g
⊢ (ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (F.map (E.f i).op)) y) =
    Presieve.FamilyOfElements.pullback (E.f i) t g hg
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ precoverage IsOpenImmersion ≤ Precoverage.comap forgetToTop TopCat.precoverage

Tactic:
rw [TopCat.precoverage, Precoverage.comap_inf, precoverage]

Goal state after:
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ jointlySurjectivePrecoverage ⊓ IsOpenImmersion.precoverage ≤
    Precoverage.comap forgetToTop
        (Precoverage.comap (CategoryTheory.forget TopCat) Types.jointlySurjectivePrecoverage) ⊓
      Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i : 𝒰.I₀
⊢ (ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op))
      (ofHom
        (ContinuousMap.liftCover (fun i ↦ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
          (fun i ↦ { toFun := ⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ }) ⋯ ⋯)) =
    x i

Tactic:
apply ConcreteCategory.hom_ext

Goal state after:
case refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i : 𝒰.I₀
⊢ ∀ (x_1 : ↑(Opposite.unop (Opposite.op (𝒰.X i)))),
    (ConcreteCategory.hom
          ((ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op))
            (ofHom
              (ContinuousMap.liftCover (fun i ↦ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
                (fun i ↦ { toFun := ⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ }) ⋯ ⋯))))
        x_1 =
      (ConcreteCategory.hom (x i)) x_1
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
let Af := Localization.Away f

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) = -(eval P) W.polynomialX / P z / (P y - W.negY P)

Tactic:
simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x / P z = Q x / Q z
hy : ¬P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z)
⊢ W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) = -(eval P) W.polynomialX / P z / (P y - W.negY P)
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case refine_3
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
⊢ (g 0) 0 = 0

Tactic:
rw [map_zero]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ ↑r n • Submodule.Quotient.mk (↑x n) = ↑r m • Submodule.Quotient.mk (↑x m)

Tactic:
rw [← Submodule.Quotient.mk_smul, ← Module.Quotient.mk_smul_mk,
    AdicCauchySequence.mk_eq_mk hmn, Ideal.mk_eq_mk I hmn, Module.Quotient.mk_smul_mk,
    Submodule.Quotient.mk_smul]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n)) ((ofAlgEquiv I).symm x) = (evalₐ I n) x

Tactic:
by
  simp only [evalₐ, AlgHom.coe_comp, Function.comp_apply, AlgHom.ofLinearMap_apply]
  rw [← mk_smul_top_ofAlgEquiv_symm I n x]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
hZ : IsUnit (W.dblZ P)
⊢ ![W.dblX P, W.dblY P, W.dblZ P] =
    ![W.dblZ P *
        ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          x,
      W.dblZ P *
        ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          y,
      W.dblZ P *
        ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          z]

Tactic:
← dblX_of_Z_ne_zero hP hQ hPz hQz hx hy,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
hZ : IsUnit (W.dblZ P)
⊢ ![W.dblX P, W.dblY P, W.dblZ P] =
    ![W.dblZ P *
        ![W.dblX P / W.dblZ P,
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          x,
      W.dblZ P *
        ![W.dblX P / W.dblZ P,
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          y,
      W.dblZ P *
        ![W.dblX P / W.dblZ P,
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          z]
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ P.σ g ^ n • Extension.Cotangent.mk x = 0

Tactic:
← map_smul,

Goal state after:
case h
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ Extension.Cotangent.mk (P.σ g ^ n • x) = 0
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.tensorCotangentInv ∘ₗ D.tensorCotangentHom = LinearMap.id

Tactic:
· ext : 2
    refine LinearMap.ext_on_range D.span_range_mk_kerGen fun i ↦ ?_
    simp [-toExtension_commRing, -toExtension_Ring, -toExtension_algebra₂, tensorCotangentHom_tmul,
      kerGen, D.hf]

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hFa : (aeval a) F = 0
i : ι
⊢ (AlgHom.restrictScalars k (Polynomial.aeval (a i))) (F.toPolynomialAdjoinImageCompl a i) = (aeval a) F

Tactic:
simp_rw [toPolynomialAdjoinImageCompl, ← AlgEquiv.coe_toAlgHom, ← AlgHom.comp_apply]

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hFa : (aeval a) F = 0
i : ι
⊢ ((AlgHom.restrictScalars k (Polynomial.aeval (a i))).comp
        ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp
          ((↑(optionEquivLeft k { b // b ≠ i })).comp ↑(renameEquiv k (Equiv.optionSubtypeNe i).symm))))
      F =
    (aeval a) F
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
⊢ False

Tactic:
have hF''0 : F'' ≠ 0 := ne_of_ne_of_eq (AddMonoidAlgebra.ofCoeff_eq_zero.ne.2 <|
    (Finsupp.mapDomain_injective fun s t h ↦ Subtype.ext
    (Finsupp.ext fun i ↦ by rw [hσ' _ s.2, hσ' _ t.2, h])).ne hF'0) (by simp)

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ ![P y ^ 2 * Q z * Q x, W'.addY P Q, W'.addZ P Q] = (P y ^ 2 * Q z) • Q

Tactic:
addY_of_Z_eq_zero_left hP hPz,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ ![P y ^ 2 * Q z * Q x, P y ^ 2 * Q z * Q y, W'.addZ P Q] = (P y ^ 2 * Q z) • Q
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
inst✝¹ : ExpChar k p
inst✝ : Algebra.EssFiniteType k K
s : Finset K
hs : (fun t ↦ IsTranscendenceBasis k Subtype.val) ↑s
Hs :
  ∀ ⦃j : Set K⦄,
    (fun t ↦ IsTranscendenceBasis k Subtype.val) j →
      (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j →
        (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s
⊢ ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(adjoin k ↑s)) K

Tactic:
refine ⟨s, hs, ⟨fun n ↦ of_not_not fun hn ↦ ?_⟩⟩

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
inst✝¹ : ExpChar k p
inst✝ : Algebra.EssFiniteType k K
s : Finset K
hs : (fun t ↦ IsTranscendenceBasis k Subtype.val) ↑s
Hs :
  ∀ ⦃j : Set K⦄,
    (fun t ↦ IsTranscendenceBasis k Subtype.val) j →
      (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j →
        (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) j ≤
          (fun t ↦ restrictScalars k (separableClosure (↥(adjoin k t)) K)) ↑s
n : K
hn : ¬IsSeparable (↥(adjoin k ↑s)) n
⊢ False
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
x : S
hx : x ∈ m
⊢ 0 ∈ Multiset.map (eval x) (Multiset.map (fun x ↦ X - C x) m)

Tactic:
simpa [sub_eq_zero]

Goal state after: