mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : (ofArrows X c.inj).HasPairwisePullbacks
inst✝ : PreservesLimit (Discrete.functor fun x ↦ op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : (fun X ↦ X) (∏ᶜ fun b ↦ F.obj (op (X b)))),
    ∃! a,
      (ConcreteCategory.hom
            (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
              Equalizer.Presieve.Arrows.forkMap F X c.inj))
          a =
        b
b : Equalizer.Presieve.Arrows.FirstObj F X
a✝ :
  (ConcreteCategory.hom (Equalizer.Presieve.Arrows.firstMap F X c.inj)) b =
    (ConcreteCategory.hom (Equalizer.Presieve.Arrows.secondMap F X c.inj)) b
t : F.obj (∏ᶜ fun x ↦ op (X x))
ht₁ :
  (ConcreteCategory.hom
        (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
          Equalizer.Presieve.Arrows.forkMap F X c.inj))
      t =
    b
ht₂ :
  ∀ (y : (fun X ↦ X) (F.obj (∏ᶜ fun x ↦ op (X x)))),
    (fun a ↦
          (ConcreteCategory.hom
                (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
                  Equalizer.Presieve.Arrows.forkMap F X c.inj))
              a =
            b)
        y →
      y = t
y : F.obj (op c.pt)
hy : (fun x ↦ (ConcreteCategory.hom (Equalizer.Presieve.Arrows.forkMap F X c.inj)) x = b) y
⊢ (ConcreteCategory.hom
        (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
          Equalizer.Presieve.Arrows.forkMap F X c.inj))
      ((ConcreteCategory.hom (F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).hom)) y) =
    b

Tactic:
by simp [← hy, ← comp_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case refine_1
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)

Tactic:
apply hF.isSheafFor

Goal state after:
case refine_1
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Sieve.generate (Presieve.ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a) ∈ Scheme.zariskiTopology (⊥_ Scheme)
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case refine_2
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
i j : ι
⊢ i ≠ j →
    (fun i j ↦
        IsPullback (initial.to (unop (X i))) (initial.to (unop (X j)))
          (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
          (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) j))
      i j

Tactic:
exact CoproductDisjoint.isPullback_of_isInitial
      (coproductIsCoproduct' <| Discrete.functor <| unop ∘ X) initialIsInitial

Goal state after:
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
p : Ideal A
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
⊢ ∃ f ∉ p, Smooth R (Localization.Away f)

Tactic:
obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hxf, hf⟩ :=
    isBasis_basic_opens.exists_subset_of_mem_open ‹⟨p, ‹_›⟩ ∈ smoothLocus R A› isOpen_smoothLocus

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
p : Ideal A
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
f : A
hxf : { asIdeal := p, isPrime := inst✝¹ } ∈ ↑(basicOpen f)
hf : ↑(basicOpen f) ⊆ smoothLocus R A
⊢ ∃ f ∉ p, Smooth R (Localization.Away f)
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 / P z = Q x / Q z
hy : ¬P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z)
⊢ (3 * (P x / P z) ^ 2 + 2 * W.toAffine.a₂ * (P x / P z) + W.toAffine.a₄ - W.toAffine.a₁ * (P y / P z)) /
      (P y / P z - W.negY P / P z) =
    -(eval P) W.polynomialX / P z / (P y - W.negY P)

Tactic:
simp [field, eval_polynomialX]

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
inst✝ : Algebra.IsPushout R S A B
⊢ ↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))) =
    ↑R LinearMap.id

Tactic:
apply TensorProduct.ext'

Goal state after:
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
inst✝ : Algebra.IsPushout R S A B
⊢ ∀ (x : S) (y : Ω[A⁄R]),
    (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
        (x ⊗ₜ[R] y) =
      (↑R LinearMap.id) (x ⊗ₜ[R] y)
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)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
⊢ FormallySmooth R S

Tactic:
have hf₁ : Function.Surjective fP := by
    intro x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x
    obtain ⟨x, rfl⟩ := hf₀ x
    obtain ⟨s, rfl⟩ := hf₀ s
    refine ⟨IsLocalization.mk' (M := M') _ x ⟨s, hs⟩, ?_⟩
    simp [fP, IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul, IsUnit.liftRight]

Goal state after:
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)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
⊢ FormallySmooth R S
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ sumInv I M ∘ₗ sum I M = LinearMap.id

Tactic:
by
  ext j x : 2
  apply DirectSum.ext_component (AdicCompletion I R) (fun i ↦ ?_)
  ext n
  simp only [LinearMap.coe_comp, Function.comp_apply, sum_lof, map_mk, component_sumInv,
    mk_apply_coe, AdicCauchySequence.map_apply_coe, Submodule.mkQ_apply, LinearMap.id_comp]
  rw [DirectSum.component.of, DirectSum.component.of]
  split
  · next h => subst h; simp
  · simp

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
n : ℕ
d : N
hdmem : d ∈ I ^ (k + n + 1) • ⊤
y yₙ : M
hd : f y = ↑x (k + n + 1) - d
hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤
h : f (y - yₙ) ∈ I ^ (k + n) • ⊤
hincl : I ^ (k + n - k) • (I ^ k • ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
hyyₙ : y - yₙ ∈ I ^ n • ⊤
⊢ ⟨y - yₙ, hyyₙ⟩ ∈ {d | f (yₙ + ↑d) - ↑x (k + n + 1) ∈ I ^ (k + n + 1) • ⊤}

Tactic:
simpa [hd, Nat.succ_eq_add_one, Nat.add_assoc]

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
inst✝⁵ : Finite σ
T : Type u_1
ι' : Type u_2
σ' : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : Finite σ'
Q : SubmersivePresentation S T ι' σ'
P : SubmersivePresentation R S ι σ
⊢ IsUnit ((algebraMap S T) P.jacobian) ∧ IsUnit Q.jacobian

Tactic:
exact ⟨RingHom.isUnit_map _ <| P.jacobian_isUnit, Q.jacobian_isUnit⟩

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

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 : PreSubmersivePresentation R S ι σ
x : ↥P.ker
⊢ (∀ (x_1 : σ), P.cotangentComplexAux (Cotangent.mk x) x_1 = 0 x_1) ↔
    ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0

Tactic:
cotangentComplexAux_apply,

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
inst✝ : Finite σ
P : PreSubmersivePresentation R S ι σ
x : ↥P.ker
⊢ (∀ (x_1 : σ), (aeval P.val) ((pderiv (P.map x_1)) ↑x) = 0 x_1) ↔ ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

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 ι σ
x : ↥P.ker
hx : Cotangent.mk x ∈ P.cotangentComplexAux.ker
⊢ ↑x ∈ P.toExtension.ker ^ 2

Tactic:
rw [LinearMap.mem_ker, P.cotangentComplexAux_zero_iff] at hx

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
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : ↥P.ker
hx : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
⊢ ↑x ∈ P.toExtension.ker ^ 2
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
⊢ ![0, W.dblU P, W.dblZ P] = W.dblU P • ![0, 1, 0]

Tactic:
dblZ_of_Y_eq 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.dblU P, 0] = W.dblU P • ![0, 1, 0]
Module: Mathlib.RingTheory.Extension.Cotangent.Free

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
κ : 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:
apply disjoint_ker_toKaehler_of_linearIndependent
    simp_rw [← hb]
    exact b.linearIndependent

Goal state after:
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))
this✝ : Function.Bijective ⇑(P.cotangentRestrict ⋯)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this✝ }
this : Finite I
Q : Presentation R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot : ∀ (r : Unit ⊕ Fin n), bcot r = Extension.Cotangent.mk ⟨Q.relation r, ⋯⟩
⊢ IsStandardSmooth R S

Tactic:
let P' : PreSubmersivePresentation R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
    { __ := Q
      map := Sum.map _root_.id Sum.inl
      map_inj := Sum.map_injective.mpr ⟨fun _ _ h ↦ h, Sum.inl_injective⟩ }

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 ⋯)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this✝ }
this : Finite I
Q : Presentation R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot : ∀ (r : Unit ⊕ Fin n), bcot r = Extension.Cotangent.mk ⟨Q.relation r, ⋯⟩
P' : PreSubmersivePresentation R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  let __spread.0 := Q;
  { toPresentation := __spread.0, map := Sum.map _root_.id Sum.inl, map_inj := ⋯ }
⊢ IsStandardSmooth R S
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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addZ P Q = (P x * Q z - Q x * P z) ^ 3 / (P z * Q z)

Tactic:
← addZ_eq' hP hQ,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addZ P Q = W.addZ P Q * (P z * Q z) / (P z * Q z)
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case refine_3
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
⊢ IsUnit ((algebraMap P.Ring S) D.g)

Tactic:
suffices h : (algebraMap P.Ring S) D.g = 1 by simp [h]
    rw [← map_one (algebraMap P.Ring S), ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker]
    exact D.hgmem

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

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
⊢ Nat.card ↑(Set.range P.map)ᶜ = n

Tactic:
by rw [Nat.card_coe_set_eq, Set.ncard_compl,
        Set.ncard_range_of_injective P.map_inj, ← e, Algebra.Presentation.dimension]

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

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
P' : Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators := Algebra.Generators.ofSurjective (fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))) ⋯;
  { toGenerators := __Generators, relation := ⇑e.symm ∘ P.relation, span_range_relation_eq_ker := ⋯, map := _root_.id,
    map_inj := ⋯ }
⊢ IsUnit P'.jacobian

Tactic:
by
      convert! P.jacobian_isUnit using 1
      simp_rw [Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, map_det]
      congr 1
      ext i j
      trans algebraMap P.Ring S (e ((e.symm (P.relation j)).pderiv i))
      · simpa [Algebra.PreSubmersivePresentation.jacobiMatrix_apply, P',
          Algebra.Generators.ofSurjective] using congr($H _)
      suffices e ((e.symm (P.relation j)).pderiv i) = (P.relation j).pderiv (P.map i) by
        simp [Algebra.PreSubmersivePresentation.jacobiMatrix_apply, this]
      simp [e, ← MvPolynomial.pderiv_rename e₀.injective, show e₀ (Sum.inl i) = P.map i from rfl]

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

Goal state before:
pp: 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
inst✝ : Smooth A B
⊢ ∃ A₀ B₀ x x_1 x_2 x_3 x_4,
    Function.Injective ⇑(algebraMap A₀ A) ∧ FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)

Tactic:
by
  obtain ⟨A₀, B₀, _, _, hA₀, _, _⟩ := exists_subalgebra_fg R A B
  use A₀, B₀, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
    Subtype.val_injective, ⟨A₀.fg_top.mpr hA₀⟩, inferInstance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

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

Tactic:
inf_left_comm

Goal state after:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType) =
    @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
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
⊢ (aeval a) (∑ x ∈ F.support.attach, (monomial ↑x) (coeff (↑x) F)) = 0

Tactic:
rw [F.support.sum_attach (fun i ↦ monomial i (F.coeff i)), support_sum_monomial_coeff, hFa]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝³ : HasPullbacks C
P Q : MorphismProperty C
inst✝² : P.DescendsAlong Q
inst✝¹ : P.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
⊢ P.diagonal.DescendsAlong Q

Tactic:
by
  apply DescendsAlong.mk'
  introv hf hfst
  have heq : pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
      (pullbackSymmetry _ _).hom ≫
      (pullbackRightPullbackFstIso _ _ _).hom ≫
      (pullback.congrHom (by simp) rfl).hom ≫
      (pullbackSymmetry _ _).hom ≫
      pullback.diagonal (pullback.fst f g) ≫
      (diagonalObjPullbackFstIso f g).hom := by
    apply pullback.hom_ext
    apply pullback.hom_ext <;> simp [pullback.condition]
    simp [pullback.condition]
  rw [diagonal_iff]
  apply MorphismProperty.of_pullback_fst_of_descendsAlong (P := P) (Q := Q)
      (f := pullback.fst (pullback.snd g g ≫ g) f)
  · exact MorphismProperty.pullback_fst _ _ hf
  · rw [heq]
    iterate 4 rw [cancel_left_of_respectsIso (P := P)]
    rwa [cancel_right_of_respectsIso (P := P)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : P.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
algInst✝¹ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑T := (CommRingCat.Hom.hom ψ).toAlgebra
hf :
  P (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑T))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))))
⊢ Q (algebraMap (↑T) (↑T ⊗[↑R] ↑S))

Tactic:
rwa [← pullbackSpecIso_hom_fst R T S, P.cancel_left_of_respectsIso, H₂] at hf

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Defs

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
⊢ (RatFunc.mk p q).liftOn' f H = f p q

Tactic:
RatFunc.liftOn',

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
⊢ (RatFunc.mk p q).liftOn f ⋯ = f p q
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommSemiring A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : 1 < v w
p : A[X]
hp : p ≠ 0
⊢ v (∑ x ∈ Finset.range (p.natDegree + 1), (aeval w) ((monomial x) (p.coeff x))) =
    v ((aeval w) ((monomial p.natDegree) p.leadingCoeff))

Tactic:
apply Valuation.map_sum_eq_of_lt _ (by simp)

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommSemiring A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
v : Valuation B Γ
hv : Valuation.IsTrivialOn A v
w : B
hpos : 1 < v w
p : A[X]
hp : p ≠ 0
⊢ ∀ i ∈ Finset.range (p.natDegree + 1) \ {p.natDegree},
    v ((aeval w) ((monomial i) (p.coeff i))) < v ((aeval w) ((monomial p.natDegree) (p.coeff p.natDegree)))