mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ w ≤ φ.lexOrder → ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff d) φ = 0

Tactic:
intro h d hd
    apply coeff_eq_zero_of_lt_lexOrder
    exact lt_of_lt_of_le hd h

Goal state after:
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)
⊢ (∃ i, True ∧ {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U) ↔ U ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | v.norm (p.1 - p.2) < ε}

Tactic:
iInf_subtype',

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)
⊢ (∃ i, True ∧ {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U) ↔ U ∈ ⨅ x, 𝓟 {p | v.norm (p.1 - p.2) < ↑x}
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : constantCoeff φ = ↑u
⊢ φ.invOfUnit u = φ.invOfUnit (Units.mk0 (constantCoeff φ) ⋯)

Tactic:
apply congrArg (invOfUnit φ)

Goal state after:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : constantCoeff φ = ↑u
⊢ u = Units.mk0 (constantCoeff φ) ⋯
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).IsElliptic

Tactic:
· by_cases h1728 : j = 1728
    · have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
      have := Fact.mk h2.isUnit
      rw [h1728, ofJ_1728_of_two_ne_zero h2]
      infer_instance
    · have := Fact.mk (Ne.isUnit h0)
      have := Fact.mk (sub_ne_zero.2 h1728).isUnit
      rw [ofJ_ne_0_ne_1728 j h0 h1728]
      infer_instance

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹¹ : Field K
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra R K
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : IsFractionRing R K
v✝ : HeightOneSpectrum R
L : Type u_3
inst✝⁶ : NumberField K
inst✝⁵ : Field L
inst✝⁴ : NumberField L
inst✝³ : Algebra K L
v : HeightOneSpectrum (𝓞 K)
w : HeightOneSpectrum (𝓞 L)
inst✝² : Algebra (adicCompletion K v) (adicCompletion L w)
inst✝¹ : ContinuousSMul (adicCompletion K v) (adicCompletion L w)
inst✝ : IsScalarTower K (adicCompletion K v) (adicCompletion L w)
Φ : adicCompletion K v ⊗[K] L →ₗ[adicCompletion K v] adicCompletion L w :=
  (Algebra.TensorProduct.lift (Algebra.algHom (adicCompletion K v) (adicCompletion K v) (adicCompletion L w))
      (Algebra.algHom K L (adicCompletion L w)) ⋯).toLinearMap
h_dense : DenseRange ⇑Φ
⊢ Function.Surjective ⇑Φ

Tactic:
rw [← Set.range_eq_univ, ← Φ.coe_range, ← Φ.range.closed_of_finiteDimensional.closure_eq]

Goal state after:
K : Type u_1
inst✝¹¹ : Field K
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra R K
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : IsFractionRing R K
v✝ : HeightOneSpectrum R
L : Type u_3
inst✝⁶ : NumberField K
inst✝⁵ : Field L
inst✝⁴ : NumberField L
inst✝³ : Algebra K L
v : HeightOneSpectrum (𝓞 K)
w : HeightOneSpectrum (𝓞 L)
inst✝² : Algebra (adicCompletion K v) (adicCompletion L w)
inst✝¹ : ContinuousSMul (adicCompletion K v) (adicCompletion L w)
inst✝ : IsScalarTower K (adicCompletion K v) (adicCompletion L w)
Φ : adicCompletion K v ⊗[K] L →ₗ[adicCompletion K v] adicCompletion L w :=
  (Algebra.TensorProduct.lift (Algebra.algHom (adicCompletion K v) (adicCompletion K v) (adicCompletion L w))
      (Algebra.algHom K L (adicCompletion L w)) ⋯).toLinearMap
h_dense : DenseRange ⇑Φ
⊢ closure ↑Φ.range = Set.univ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ W'.Equation P

Tactic:
by convert! hP (↑hu.unit⁻¹) h; rw [smul_smul, hu.val_inv_mul, one_smul]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
⊢ IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ IsLimit (E.toPreOneHypercover.multifork F)

Tactic:
let c' : Cofan E.toPreOneHypercover.Y' :=
    Cofan.mk
      ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y (i₁ := ⟨⟩) (i₂ := ⟨⟩) ⟨⟩)
      fun b ↦ pullback.map _ _ _ _ (c.inj _) (c.inj _) (𝟙 _) (by simp) (by simp)

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
⊢ IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ IsLimit (E.toPreOneHypercover.multifork F)
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
i j : (E.sigmaOfIsColimit hc).I₀
⊢ HasPullback ((E.sigmaOfIsColimit hc).f i) ((E.sigmaOfIsColimit hc).f j)

Tactic:
dsimp [sigmaOfIsColimit]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i ↦ F.map (c.inj i).op) = F.map (Pi.lift fun i ↦ (c.inj i).op) ≫ piComparison F fun i ↦ op (X i)
⊢ (piComparison F fun x ↦ op (X x)) =
    F.map ((opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫ Pi.lift fun i ↦ (c.inj i).op) ≫
      piComparison F fun i ↦ op (X i)

Tactic:
have hh : Pi.lift (fun i ↦ (c.inj i).op) = (productIsProduct (op <| X ·)).lift c.op := by
    simp [Pi.lift, productIsProduct]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
this : HasCoproduct X
h : (Pi.lift fun i ↦ F.map (c.inj i).op) = F.map (Pi.lift fun i ↦ (c.inj i).op) ≫ piComparison F fun i ↦ op (X i)
hh : (Pi.lift fun i ↦ (c.inj i).op) = (productIsProduct fun x ↦ op (X x)).lift c.op
⊢ (piComparison F fun x ↦ op (X x)) =
    F.map ((opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫ Pi.lift fun i ↦ (c.inj i).op) ≫
      piComparison F fun i ↦ op (X i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
h : (W'⁄A).Equation P
⊢ (W'⁄B).Equation (⇑f ∘ P)

Tactic:
convert! Equation.map f.toRingHom h using 1
  rw [AlgHom.toRingHom_eq_coe, map_baseChange]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_3
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
f : (fun X ↦ X) ((yoneda.obj X).obj (Opposite.op Y))
hf : (fun t ↦ ∀ (i : 𝒰.I₀), (ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op)) t = x i) f
⊢ f =
    ofHom
      (ContinuousMap.liftCover (fun i ↦ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
        (fun i ↦ { toFun := ⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ }) ⋯ ⋯)

Tactic:
dsimp
    ext x
    obtain ⟨i, y, rfl⟩ := exists_mem_zeroHypercover_range 𝒰 x
    have := congr($(hf i).hom y)
    dsimp at this ⊢
    rw [this, heq, ContinuousMap.liftCover_coe]
    simp

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

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).neg (⇑f ∘ P) = ⇑f ∘ (W'⁄A).neg P

Tactic:
by
  rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_neg, map_baseChange]

Goal state after:
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ Smooth) ((algebraMap S (Localization.Away ↑r)).comp f)
this : f.FinitePresentation
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation R S
⊢ f.Smooth

Tactic:
refine ⟨?_, ‹_›⟩

Goal state after:
R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ Smooth) ((algebraMap S (Localization.Away ↑r)).comp f)
this : f.FinitePresentation
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation R S
⊢ Algebra.FormallySmooth R S
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
f : A
⊢ Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ∧ (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ Module.freeLocus A Ω[A⁄R] ↔
    Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R] ∧
      Subsingleton (H1Cotangent R (Localization.Away f))

Tactic:
iff_comm,

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
f : A
⊢ Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R] ∧
      Subsingleton (H1Cotangent R (Localization.Away f)) ↔
    Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ∧ (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ Module.freeLocus A Ω[A⁄R]
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
⊢ (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) 1 = 1

Tactic:
simp only [AlgHom.comp_toLinearMap, LinearMap.coe_comp, LinearMap.coe_single,
          Function.comp_apply, AlgHom.toLinearMap_apply, Ideal.Quotient.mkₐ_eq_mk]
        rw [eq_comm, ← sub_eq_zero, ← (Ideal.Quotient.mk J').map_one, ← map_sub,
          Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]

Goal state after:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
A : Type u
inst✝⁹ : Field K
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : EssFiniteType K A
inst✝⁴ : FormallyEtale K A
inst✝³ : Algebra K B
inst✝² : EssFiniteType K B
inst✝¹ : FormallyEtale K B
inst✝ : IsSepClosed K
f : A →ₐ[K] B
x : A
p : PrimeSpectrum B
heq : ofId K (B ⧸ p.asIdeal) = (Ideal.quotientMapₐ p.asIdeal f ⋯).comp (ofId K (A ⧸ Ideal.comap f p.asIdeal))
h :
  (Ideal.quotientMapₐ p.asIdeal f ⋯) ((Ideal.Quotient.mk (Ideal.comap f p.asIdeal)) x) =
    (Ideal.Quotient.mk p.asIdeal) (f x)
⊢ (Ideal.quotientMapₐ p.asIdeal f ⋯)
      ((ofId K (A ⧸ Ideal.comap f p.asIdeal))
        ((AlgEquiv.ofBijective (ofId K (A ⧸ Ideal.comap (↑f) p.asIdeal)) ⋯).symm
          ((Ideal.Quotient.mk (Ideal.comap (↑f) p.asIdeal)) x))) =
    (Ideal.Quotient.mk p.asIdeal) (f x)

Tactic:
convert h

Goal state after:
K : Type u_1
A : Type u
inst✝⁹ : Field K
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : EssFiniteType K A
inst✝⁴ : FormallyEtale K A
inst✝³ : Algebra K B
inst✝² : EssFiniteType K B
inst✝¹ : FormallyEtale K B
inst✝ : IsSepClosed K
f : A →ₐ[K] B
x : A
p : PrimeSpectrum B
heq : ofId K (B ⧸ p.asIdeal) = (Ideal.quotientMapₐ p.asIdeal f ⋯).comp (ofId K (A ⧸ Ideal.comap f p.asIdeal))
h :
  (Ideal.quotientMapₐ p.asIdeal f ⋯) ((Ideal.Quotient.mk (Ideal.comap f p.asIdeal)) x) =
    (Ideal.Quotient.mk p.asIdeal) (f x)
⊢ (ofId K (A ⧸ Ideal.comap f p.asIdeal))
      ((AlgEquiv.ofBijective (ofId K (A ⧸ Ideal.comap (↑f) p.asIdeal)) ⋯).symm
        ((Ideal.Quotient.mk (Ideal.comap (↑f) p.asIdeal)) x)) =
    (Ideal.Quotient.mk (Ideal.comap f p.asIdeal)) x
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Flat R S
inst✝¹⁰ : CommRing P
inst✝⁹ : Algebra R P
inst✝⁸ : Algebra P S
inst✝⁷ : IsScalarTower R P S
inst✝⁶ : IsLocalRing R
inst✝⁵ : IsLocalRing S
inst✝⁴ : IsLocalHom (algebraMap R S)
inst✝³ : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst✝³ : Algebra Pp Sp := φ.toAlgebra
algInst✝² : Algebra P Sp := (φ.comp (algebraMap P Pp)).toAlgebra
algInst✝¹ : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst✝ : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst✝¹ : IsScalarTower P Pp Sp := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P Sp))
scalarTowerInst✝ : IsScalarTower Pp Sp 𝓀[S] := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Pp 𝓀[S]))
this✝⁶ : IsScalarTower 𝓀[R] Pp Sp
this✝⁵ : IsScalarTower R Sp 𝓀[S]
this✝⁴ : IsScalarTower P S Sp
this✝³ : IsScalarTower S Sp 𝓀[S]
this✝² : IsScalarTower P Sp 𝓀[S]
this✝¹ : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp).symm
this✝ : Module.Free Pp Ω[Pp⁄𝓀[R]]
this : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (algebraMap P S)) := kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective ⇑φ
h₂' : (RingHom.ker φ).FG
x : Sp
hx : x ∈ 𝓂[Sp]
⊢ Function.Surjective ⇑(algebraMap R 𝓀[R])

Tactic:
exact residue_surjective

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this✝ : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
  AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm) (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
      TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
y : Ω[A⁄R]
x : A
z : S
this : b • z • a • x • (map R S A B) y = ((algebraMap A B) a * (algebraMap S B) b) • z • x • (map R S A B) y
⊢ e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • (Algebra.IsPushout.equiv R A S B) (x ⊗ₜ[R] z) ⊗ₜ[A] y) =
    (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ ((Algebra.IsPushout.equiv R A S B) (x ⊗ₜ[R] z) ⊗ₜ[A] y)

Tactic:
by
    simpa [e₂, e₁, smul_tmul', Algebra.IsPushout.equiv_tmul, ← mul_smul,
      Algebra.IsPushout.equiv_symm_algebraMap_left, Algebra.IsPushout.equiv_symm_algebraMap_right]

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblX P = 0

Tactic:
by
  rw [dblX, hPz, X_eq_zero_of_Z_eq_zero hP hPz]
  ring1

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Finite σ
inst✝ : DecidableEq σ
i j : σ
⊢ (((Pi.basisFun S σ).constr S) fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) (Pi.single i 1) j =
    (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Tactic:
← Pi.basisFun_apply,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Finite σ
inst✝ : DecidableEq σ
i j : σ
⊢ (((Pi.basisFun S σ).constr S) fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) ((Pi.basisFun S σ) i) j =
    (aeval P.val) ((pderiv (P.map j)) (P.relation i))
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
p q : Submodule R M
hpq : IsCompl p q
hker : Disjoint g.ker q
hmap : map g q = ⊤
⊢ Function.Injective ⇑(p.projectionOnto q hpq ∘ₗ f)

Tactic:
rwa [LinearMap.coe_comp, Set.InjOn.injective_iff ↑(LinearMap.range f) _ subset_rfl]

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
p q : Submodule R M
hpq : IsCompl p q
hker : Disjoint g.ker q
hmap : map g q = ⊤
⊢ Set.InjOn ⇑(p.projectionOnto q hpq) ↑f.range
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: case intro
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : P.HasCoeffs R₀
inst✝¹ : Finite ι
inst✝ : Finite σ
val✝ : Fintype σ
⊢ FinitePresentation R₀ (ModelOfHasCoeffs R₀)

Tactic:
exact .quotient ⟨Finset.image (P.relationOfHasCoeffs R₀) .univ, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp
      ((Ideal.Quotient.liftₐ P.ker
            ((TensorProduct.map (AlgHom.id R R)
                  (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
              ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
            ⋯).comp
        ((↑(AlgEquiv.restrictScalars R P.quotientEquiv).symm).comp
          ((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)))) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)

Tactic:
← AlgHom.comp_assoc _ _ (Ideal.Quotient.mkₐ R P.ker),

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp
      ((Ideal.Quotient.liftₐ P.ker
            ((TensorProduct.map (AlgHom.id R R)
                  (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
              ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
            ⋯).comp
        (((↑(AlgEquiv.restrictScalars R P.quotientEquiv).symm).comp ↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp
          (Ideal.Quotient.mkₐ R P.ker))) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)