mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ (ofId K (B ⧸ p.asIdeal))
      ((AlgEquiv.ofBijective (ofId K (A ⧸ Ideal.comap (↑f) p.asIdeal)) ⋯).symm
        ((Ideal.Quotient.mk (Ideal.comap (↑f) p.asIdeal)) x)) =
    (ofId K (B ⧸ p.asIdeal))
      ((AlgEquiv.ofBijective (ofId K (B ⧸ p.asIdeal)) ⋯).symm ((Ideal.Quotient.mk p.asIdeal) (f x)))

Tactic:
nth_rw 1 [heq]

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)
⊢ ((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)) =
    (ofId K (B ⧸ p.asIdeal))
      ((AlgEquiv.ofBijective (ofId K (B ⧸ p.asIdeal)) ⋯).symm ((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
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
x : B
y : Ω[A⁄R]
⊢ e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • x ⊗ₜ[A] y) =
    (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ (x ⊗ₜ[A] y)

Tactic:
obtain ⟨x, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective x
  induction x with
  | zero => simp
  | add x y _ _ => simp only [smul_add, map_add, *, add_tmul]
  | tmul x z =>
  suffices b • z • a • x • KaehlerDifferential.map R S A B y =
      (algebraMap A B a * algebraMap S B b) • z • x • KaehlerDifferential.map R S A B y by
    simpa [e₂, e₁, smul_tmul', Algebra.IsPushout.equiv_tmul, ← mul_smul,
      Algebra.IsPushout.equiv_symm_algebraMap_left, Algebra.IsPushout.equiv_symm_algebraMap_right]
  simp only [← mul_smul, ← @algebraMap_smul S _ B, ← @algebraMap_smul A _ B]
  ring_nf

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
this : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix = 1
⊢ ((algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix).det = 1

Tactic:
this,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
this : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix = 1
⊢ Matrix.det 1 = 1
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case add
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : Fintype σ'
i j : σ
p q : MvPolynomial ι R
hp :
  { toRingHom := eval₂Hom (algebraMap R T) (Q.comp P).val, commutes' := ⋯ } ((rename Sum.inr) p) =
    eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) p
hq :
  { toRingHom := eval₂Hom (algebraMap R T) (Q.comp P).val, commutes' := ⋯ } ((rename Sum.inr) q) =
    eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) q
⊢ { toRingHom := eval₂Hom (algebraMap R T) (Q.comp P).val, commutes' := ⋯ } ((rename Sum.inr) (p + q)) =
    eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) (p + q)

Tactic:
| add p q hp hq =>

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₀
r : σ
⊢ (MvPolynomial.aeval P.val) (P.relation r) = 0

Tactic:
aeval_val_relation

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₀
r : σ
⊢ 0 = 0
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:
simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le]

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₀
⊢ Set.range (relationOfHasCoeffs R₀) ⊆ ↑(RingHom.ker (MvPolynomial.aeval P.val))
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
inst✝ : IsStandardSmooth R S
n : ℕ
h : Module.rank S Ω[S⁄R] = ↑n
w✝² w✝¹ : Type
w✝ : Finite w✝¹
left✝ : Finite w✝²
P : SubmersivePresentation R S w✝² w✝¹
⊢ ↑P.dimension = ↑n

Tactic:
← P.rank_kaehlerDifferential

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
inst✝ : IsStandardSmooth R S
n : ℕ
h : Module.rank S Ω[S⁄R] = ↑n
w✝² w✝¹ : Type
w✝ : Finite w✝¹
left✝ : Finite w✝²
P : SubmersivePresentation R S w✝² w✝¹
⊢ Module.rank S Ω[S⁄R] = ↑n
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: case a
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
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P) * P z ^ 2 + W'.negDblY P * P z ^ 2 -
      ((eval P) W'.polynomialX ^ 3 + -(eval P) W'.polynomialX ^ 3) =
    0

Tactic:
dblX_of_Y_eq hP hPz hQz hx hy hy',

Goal state after:
case a
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
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ (-W'.negDblY P - W'.a₁ * 0 - W'.a₃ * W'.dblZ P) * P z ^ 2 + W'.negDblY P * P z ^ 2 -
      ((eval P) W'.polynomialX ^ 3 + -(eval P) W'.polynomialX ^ 3) =
    0
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: 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 ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
this :
  (localizationAway T g).ker =
    Ideal.map ((localizationAway T g).ofComp P).toAlgHom (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1})
⊢ RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔
      Ideal.comap ((localizationAway T g).ofComp P).toAlgHom (localizationAway T g).ker =
    RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}

Tactic:
this,

Goal state after:
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 ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
this :
  (localizationAway T g).ker =
    Ideal.map ((localizationAway T g).ofComp P).toAlgHom (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1})
⊢ RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔
      Ideal.comap ((localizationAway T g).ofComp P).toAlgHom
        (Ideal.map ((localizationAway T g).ofComp P).toAlgHom (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1})) =
    RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}
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
⊢ W.negY ![W.dblX P, W.negDblY P, W.dblZ 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))

Tactic:
negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' 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
⊢ W.toAffine.negY (![W.dblX P, W.negDblY P, W.dblZ P] x / ![W.dblX P, W.negDblY P, W.dblZ P] z)
      (![W.dblX P, W.negDblY P, W.dblZ P] y / ![W.dblX P, W.negDblY P, W.dblZ P] 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))
Module: Mathlib.RingTheory.Extension.Cotangent.Free

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
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Function.Bijective ⇑(P.cotangentRestrict hu)

Tactic:
by
  rw [cotangentRestrict, Finsupp.lcomapDomain_eq_linearProjOfIsCompl _ huv.symm]
  set f : _ →ₗ[S] (ι →₀ S) := P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
  let g : (ι →₀ S) →ₗ[S] (Ω[S⁄R]) := P.toExtension.toKaehler ∘ₗ P.cotangentSpaceBasis.repr.symm
  have hfg : Function.Exact f g := by
    simp only [f, g, LinearEquiv.conj_exact_iff_exact]
    exact Extension.exact_cotangentComplex_toKaehler
  apply LinearMap.linearProjOfIsCompl_comp_bijective_of_exact hfg
  · exact P.cotangentSpaceBasis.repr.injective.comp <|
      (Extension.subsingleton_h1Cotangent P.toExtension).mp P.equivH1Cotangent.subsingleton
  · simp only [disjoint_iff, g]
    apply Submodule.map_injective_of_injective (f := P.cotangentSpaceBasis.repr.symm.toLinearMap)
      P.cotangentSpaceBasis.repr.symm.injective
    rw [Submodule.map_inf P.cotangentSpaceBasis.repr.symm.toLinearMap
        P.cotangentSpaceBasis.repr.symm.injective, Submodule.map_span, ← Set.range_comp,
        Function.comp_def, LinearMap.ker_comp, Submodule.map_comap_eq_of_surjective]
    · simpa [← disjoint_iff]
    · exact P.cotangentSpaceBasis.repr.symm.surjective
  · simpa [g, Submodule.map_comp, Submodule.map_span, ← Set.range_comp, Function.comp_def]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ ![W.dblX P, W.dblY P, W.dblZ P] = W.dblU P • ![0, 1, 0]

Tactic:
dblX_of_Y_eq hP hPz hQz hx hy hy',

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ ![0, W.dblY P, W.dblZ P] = W.dblU P • ![0, 1, 0]
Module: Mathlib.RingTheory.Extension.Cotangent.Free

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
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb : ∀ (k : κ), b k = (D R S) (P.val (v k))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤

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
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb : ∀ (k : κ), b k = (D R S) (P.val (v k))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))

Tactic:
· simp_rw [← hb]
    exact b.span_eq

Goal state after:
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
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb : ∀ (k : κ), b k = (D R S) (P.val (v k))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
inst✝ : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
a✝ : Nontrivial S
n : ℕ
P✝ : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → a ∈ Set.range ⇑b → S
hf' : ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : a ∈ Set.range ⇑b), (D R S) (f' a_1) = a
P : Generators R S (Fin n ⊕ I) := P✝.extend fun i ↦ f' ⋯
hb : ∀ (i : I), b i = (D R S) (P.val (Sum.inr i))
⊢ IsStandardSmooth R S

Tactic:
have : Function.Bijective (P.cotangentRestrict _) :=
    P.cotangentRestrict_bijective_of_basis_kaehlerDifferential Sum.inl_injective
      Set.isCompl_range_inl_range_inr.symm b hb

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
inst✝ : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
a✝ : Nontrivial S
n : ℕ
P✝ : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → a ∈ Set.range ⇑b → S
hf' : ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : a ∈ Set.range ⇑b), (D R S) (f' a_1) = a
P : Generators R S (Fin n ⊕ I) := P✝.extend fun i ↦ f' ⋯
hb : ∀ (i : I), b i = (D R S) (P.val (Sum.inr i))
this : Function.Bijective ⇑(P.cotangentRestrict ⋯)
⊢ IsStandardSmooth R S
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
⊢ Presentation.ModelOfHasCoeffs ↥(subalgebra R D) →ₐ[↥(subalgebra R D)]
    MvPolynomial D.vars ↥(subalgebra R D) ⧸
      RingHom.ker
          (Ideal.Quotient.mkₐ (↥(subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
        2

Tactic:
refine Ideal.Quotient.liftₐ _ ((Ideal.Quotient.mkₐ _ _).comp <| aeval p) ?_

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
⊢ ∀ a ∈ Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))),
    ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (RingHom.ker
                  (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                    (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                2)).comp
          (aeval p))
        a =
      0
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr.e'_6.e'_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
e_2✝ : ↥((localizationAway S D.gbar).comp D.presLeft.toGenerators).toExtension.ker = ↥D.pres.toExtension.ker
e_1✝ : ((localizationAway S D.gbar).comp D.presLeft.toGenerators).toExtension.Ring = D.pres.toExtension.Ring
⊢ ↑((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toAlgHom ↑(D.kerGen r) = D.pres.relation (Sum.inr r)

Tactic:
simp [pres, Presentation.comp_relation_inr, kerGen, presLeft, Generators.toComp_toAlgHom]

Goal state after:
case inr.e'_6.e'_3
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
e_2✝ : ↥((localizationAway S D.gbar).comp D.presLeft.toGenerators).toExtension.ker = ↥D.pres.toExtension.ker
e_1✝ : ((localizationAway S D.gbar).comp D.presLeft.toGenerators).toExtension.Ring = D.pres.toExtension.Ring
⊢ ↑(rename Sum.inr) ↑(D.f (b r)) = (rename Sum.inr) ↑(D.f (b r))
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
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := Equiv.subtypeEquivRight ⋯
⊢ Polynomial.map
      (↑((renameEquiv k d).trans
          (H.aevalEquiv.trans
            ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯))))
      ((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)) =
    Polynomial.map (↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩))
      ((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F))

Tactic:
refine congrFun (congrArg Polynomial.map ?_) _

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
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := Equiv.subtypeEquivRight ⋯
⊢ ↑((renameEquiv k d).trans
        (H.aevalEquiv.trans ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯))) =
    ↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsFinite = @IsAffineHom ⊓ @IsSeparated ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)

Tactic:
this,

Goal state after:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsFinite = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ addU (⇑f ∘ P) (⇑f ∘ Q) = f (addU P Q)

Tactic:
simp only [addU]
  map_simp

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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha : adjoin k (Set.range a) = ⊤
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K

Tactic:
have ⟨i, hi⟩ := exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow p hp H n ha'

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
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha : adjoin k (Set.range a) = ⊤
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
i : ι
hi : (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
⊢ ∃ i, (IsTranscendenceBasis k fun j ↦ a ↑j) ∧ Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K