mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
⊢ IsPrincipalIdealRing O

Tactic:
rcases subsingleton_or_nontrivial (MonoidHom.mrange v)ˣ with hs | _

Goal state after:
case inl
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
hs : Subsingleton (↥(MonoidHom.mrange v))ˣ
⊢ IsPrincipalIdealRing O

case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
⊢ IsPrincipalIdealRing O
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
inst✝ : IsGalois k K
φ ψ : K →+* ℂ
h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)
this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra
this✝ : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
⊢ ∃ σ, φ.comp ↑σ.symm = ψ

Tactic:
let ψ' : K →ₐ[k] ℂ := { ψ with commutes' := fun r ↦ (RingHom.congr_fun h r).symm }

Goal state after:
K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ ψ : K →+* ℂ
h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)
this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra
this✝ : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }
⊢ ∃ σ, φ.comp ↑σ.symm = ψ
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 φ σ
⊢ IsReal (φ.comp (algebraMap k K))

Tactic:
by
  ext1 x
  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 Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H : Nontrivial (ofClass v).ValueGroup₀ˣ
H' : ∀ (x : K), v x ≠ 0 → v x = 1
⊢ False

Tactic:
rw [nontrivial_iff_exists_ne 1] at H

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H : ∃ y, y ≠ 1
H' : ∀ (x : K), v x ≠ 0 → v x = 1
⊢ False
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x✝ y✝ : X
r✝ s✝ : ℝ
x y : X
r s : ℝ
hrs : r ≤ s
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

Tactic:
refine Set.disjoint_or_nonempty_inter (closedBall x r) (closedBall y s) |>.symm.imp
      (fun h ↦ ?_) (Or.inr ·)
    obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem
    have hx := closedBall_subset_closedBall hrs (x := x)
    rwa [closedBall_eq_of_mem hyz |>.trans (closedBall_eq_of_mem <| hx hxz).symm]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
z : ℤ
⊢ ‖x ^ z‖₊ ≤ ‖x‖₊

Tactic:
cases z <;>
  simpa using nnnorm_pow_le _ _

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff ψ ≠ 0
⊢ ψ⁻¹ = φ ↔ φ * ψ = 1

Tactic:
rw [eq_comm, MvPowerSeries.eq_inv_iff_mul_eq_one h]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case h
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ X ^ f.order.toNat * ↑f.Unit_of_divided_by_X_pow_order = f

Tactic:
simp only [Unit_of_divided_by_X_pow_order_nonzero hf]

Goal state after:
case h
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ X ^ f.order.toNat * f.divXPowOrder = f
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
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : adicCompletion K v
⊢ ‖x‖ = ↑((toNNReal ⋯) (Valued.v x))

Tactic:
simp [Valued.toNormedField.norm_def, Valuation.RankOne.hom, HeightOneSpectrum.rankOne_hom'_def,
    valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective
      (valuedAdicCompletion_surjective K v)]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
⊢ Function.HasFiniteMulSupport fun w ↦ w ((algebraMap (𝓞 K) K) a) / w ((algebraMap (𝓞 K) K) b)

Tactic:
simp_rw [← RingOfIntegers.coe_eq_algebraMap]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
⊢ Function.HasFiniteMulSupport fun w ↦ w ↑a / w ↑b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: 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
h1728 : j = 1728
h : 2 = 0
⊢ j = 0

Tactic:
by linear_combination h1728 + 864 * h

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h : 2 = 0
⊢ j = 0

Tactic:
by linear_combination h1728 + 864 * h

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

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : ¬i = j
this : PreservesLimit (Functor.empty Cᵒᵖ) F
⊢ (ConcreteCategory.hom
        (F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
            F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫
              PreservesTerminal.iso F).hom)
      ((ConcreteCategory.hom (F.map (pullback.fst (c.inj i) (c.inj j)).op))
        ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) i)) a)) =
    (ConcreteCategory.hom
        (F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
            F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫
              PreservesTerminal.iso F).hom)
      ((ConcreteCategory.hom (F.map (pullback.snd (c.inj i) (c.inj j)).op))
        ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) j)) a))

Tactic:
ext ⟨i⟩

Goal state after:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i✝ j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : ¬i✝ = j
this : PreservesLimit (Functor.empty Cᵒᵖ) F
i : PEmpty.{1}
⊢ (ConcreteCategory.hom (limit.π (Functor.empty (Type w)) { as := i }))
      ((ConcreteCategory.hom
          (F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
              F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫
                PreservesTerminal.iso F).hom)
        ((ConcreteCategory.hom (F.map (pullback.fst (c.inj i✝) (c.inj j)).op))
          ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) i✝)) a))) =
    (ConcreteCategory.hom (limit.π (Functor.empty (Type w)) { as := i }))
      ((ConcreteCategory.hom
          (F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
              F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫
                PreservesTerminal.iso F).hom)
        ((ConcreteCategory.hom (F.map (pullback.snd (c.inj i✝) (c.inj j)).op))
          ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) j)) a)))
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).FormallySmooth ↔ Algebra.FormallySmooth R S

Tactic:
rw [FormallySmooth, toAlgebra_algebraMap]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyUnramified
h : (g.comp f).FormallyEtale
⊢ g.FormallyEtale

Tactic:
by
  algebraize [f, g, g.comp f]
  exact Algebra.FormallyEtale.of_restrictScalars (R := R)

Goal state after:
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr
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_1 : Algebra R B] (I_1 : Ideal B),
    I_1 ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I_1).comp

Tactic:
intro B _ _ J hJ f₁ f₂ e

Goal state after:
case intro.mpr
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₂
⊢ f₁ = f₂
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: 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)
x y : L
this✝ : FiniteDimensional K ↥K⟮x, y⟯
this : Algebra.IsSeparable K ↥K⟮x, y⟯
α : L
hα : α ∈ K⟮x, y⟯
e : IntermediateField.map K⟮x, y⟯.val K⟮⟨α, hα⟩⟯ = IntermediateField.map K⟮x, y⟯.val ⊤
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Tactic:
rw [IntermediateField.adjoin_map, ← AlgHom.fieldRange_eq_map] at e

Goal state after:
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)
x y : L
this✝ : FiniteDimensional K ↥K⟮x, y⟯
this : Algebra.IsSeparable K ↥K⟮x, y⟯
α : L
hα : α ∈ K⟮x, y⟯
e : IntermediateField.adjoin K (⇑K⟮x, y⟯.val '' {⟨α, hα⟩}) = K⟮x, y⟯.val.fieldRange
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
Module: Mathlib.RingTheory.Smooth.Local

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsLocalRing S
inst✝¹¹ : Algebra R S
P : Type u_3
K : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : Algebra S K
inst✝⁴ : Algebra P K
inst✝³ : IsScalarTower P S K
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
h₃ : maximalIdeal S ≤ RingHom.ker (algebraMap S K)
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this✝² : Algebra (ResidueField S) K := f.toAlgebra
this✝¹ : IsScalarTower S (ResidueField S) K
this✝ : IsScalarTower P (ResidueField S) K
this :
  ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) ∘ₗ
      LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
        ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K ↥(RingHom.ker (algebraMap P S))).symm =
    cotangentComplexBaseChange R S P K
⊢ Function.Injective ⇑(LinearMap.lTensor K (cotangentComplexBaseChange R S P (ResidueField S))) ↔
    Function.Injective ⇑(cotangentComplexBaseChange R S P K)

Tactic:
rw [← this]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsLocalRing S
inst✝¹¹ : Algebra R S
P : Type u_3
K : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : Algebra S K
inst✝⁴ : Algebra P K
inst✝³ : IsScalarTower P S K
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
h₃ : maximalIdeal S ≤ RingHom.ker (algebraMap S K)
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this✝² : Algebra (ResidueField S) K := f.toAlgebra
this✝¹ : IsScalarTower S (ResidueField S) K
this✝ : IsScalarTower P (ResidueField S) K
this :
  ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) ∘ₗ
      LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
        ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K ↥(RingHom.ker (algebraMap P S))).symm =
    cotangentComplexBaseChange R S P K
⊢ Function.Injective ⇑(LinearMap.lTensor K (cotangentComplexBaseChange R S P (ResidueField S))) ↔
    Function.Injective
      ⇑(↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) ∘ₗ
          LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
            ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K ↥(RingHom.ker (algebraMap P S))).symm)
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))
⊢ (AlgEquiv.ofBijective (ofId K (A ⧸ Ideal.comap (↑f) p.asIdeal)) ⋯).symm
      ((Ideal.Quotient.mk (Ideal.comap (↑f) p.asIdeal)) x) =
    (AlgEquiv.ofBijective (ofId K (B ⧸ p.asIdeal)) ⋯).symm ((Ideal.Quotient.mk p.asIdeal) (f x))

Tactic:
suffices h : Ideal.quotientMapₐ p.asIdeal f le_rfl x = f x by
    apply FaithfulSMul.algebraMap_injective K (B ⧸ p.asIdeal)
    rw [← ofId_apply, ← ofId_apply]
    nth_rw 1 [heq]
    simp only [AlgHom.coe_comp, Function.comp_apply, AlgEquiv.ofBijective_apply_symm_apply]
    convert h
    apply AlgEquiv.ofBijective_apply_symm_apply

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))
⊢ (Ideal.quotientMapₐ p.asIdeal f ⋯) ((Ideal.Quotient.mk (Ideal.comap f p.asIdeal)) x) =
    (Ideal.Quotient.mk p.asIdeal) (f x)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.tmul
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
z m✝ : A
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * (IsScalarTower.toAlgHom R A B).toLinearMap m✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((IsScalarTower.toAlgHom R A B).toLinearMap m✝) +
      (IsScalarTower.toAlgHom R A B).toLinearMap m✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)

Tactic:
simp only [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom',
          algebraMap_smul, ← map_mul]

Goal state after:
case tmul.tmul
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
z m✝ : A
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) (z * m✝)) =
    z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) m✝) +
      m✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
S : Type u_6
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsPrecomplete I R
haus : IsHausdorff (Ideal.map f I) S
h : Function.Surjective ⇑((Ideal.Quotient.mk (Ideal.map f I)).comp f)
x✝ : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := (Algebra.ofId R S).toLinearMap
⊢ Function.Surjective ⇑f

Tactic:
change Function.Surjective ((restrictScalars R (I.map f)).mkQ ∘ₗ fₗ) at h

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
S : Type u_6
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsPrecomplete I R
haus : IsHausdorff (Ideal.map f I) S
x✝ : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := (Algebra.ofId R S).toLinearMap
h : Function.Surjective ⇑((restrictScalars R (Ideal.map f I)).mkQ ∘ₗ fₗ)
⊢ Function.Surjective ⇑f
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
inst✝¹ : Finite σ
inst✝ : Subsingleton S
⊢ Ideal.span (Set.range fun x ↦ 1) = { val := fun x ↦ 1, σ' := fun x ↦ 1, aeval_val_σ' := ⋯, algebraMap_eq := ⋯ }.ker

Tactic:
by
    simp [Generators.ker, Extension.ker, RingHom.ker_eq_top_of_subsingleton]

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₀
⊢ ∀ a ∈ Ideal.span (Set.range (relationOfHasCoeffs R₀)), (MvPolynomial.aeval P.val) a = 0

Tactic:
← RingHom.mem_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₀
⊢ ∀ a ∈ Ideal.span (Set.range (relationOfHasCoeffs R₀)), a ∈ RingHom.ker (MvPolynomial.aeval P.val)
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₀
⊢ ∀ a ∈ P.ker,
    ((TensorProduct.map (AlgHom.id R R) (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
          ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
        a =
      0

Tactic:
← RingHom.mem_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₀
⊢ ∀ a ∈ P.ker,
    a ∈
      RingHom.ker
        ((TensorProduct.map (AlgHom.id R R)
              (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
          ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
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
inst✝⁵ : Finite σ
P : SubmersivePresentation 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₀
this : Fintype σ := Fintype.ofFinite σ
⊢ (MvPolynomial.aeval P.val) (P.jacobianOfHasCoeffs R₀) = P.jacobian

Tactic:
rw [← MvPolynomial.aeval_map_algebraMap R, map_jacobianOfHasCoeffs,
    P.jacobian_eq_jacobiMatrix_det, Generators.algebraMap_apply]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Smooth R A
A₀ B₀ : Type u_1
w✝⁴ : CommRing A₀
w✝³ : CommRing B₀
w✝² : Algebra ℤ A₀
w✝¹ : Algebra A₀ R
w✝ : Algebra A₀ B₀
left✝² : Function.Injective ⇑(algebraMap A₀ R)
left✝¹ : FiniteType ℤ A₀
left✝ : Smooth A₀ B₀
e : A ≃ₐ[R] TensorProduct A₀ R B₀
this✝ : IsNoetherianRing A₀
this : Module.Flat A₀ B₀
⊢ Module.Flat R A

Tactic:
exact .of_linearEquiv e.toLinearEquiv

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: 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
⊢ ∀ a ∈ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)), (aeval P.val) a = 0

Tactic:
← RingHom.mem_ker,

Goal state after:
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
⊢ ∀ a ∈ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)), a ∈ RingHom.ker (aeval P.val)
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case refine_1
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
⊢ Function.Surjective ⇑(algebraMap D.T S)

Tactic:
refine .of_comp (g := algebraMap P.Ring D.T) ?_

Goal state after:
case refine_1
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
⊢ Function.Surjective (⇑(algebraMap D.T S) ∘ ⇑(algebraMap P.Ring D.T))