mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
⊢ embedRealFun 1 = 1

Tactic:
apply le_antisymm

Goal state after:
case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
⊢ embedRealFun 1 ≤ 1

case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
⊢ 1 ≤ embedRealFun 1
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
⊢ (coeff n) φ⁻¹ = (coeff n) 0

Tactic:
rw [coeff_inv]

Goal state after:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
⊢ (if n = 0 then (constantCoeff φ)⁻¹
    else -(constantCoeff φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) φ⁻¹ else 0) =
    (coeff n) 0
Module: Mathlib.AlgebraicGeometry.Geometrically.Connected

Goal state before:
pp: ⊢ @GeometricallyConnected = geometrically fun x ↦ ConnectedSpace ↥x

Tactic:
ext; exact geometricallyConnected_iff _

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialY / P z ^ 2 + (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY +
        (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) + W.a₃ * (P z ^ 2 / P z ^ 2))) =
    0

Tactic:
rw [eval_polynomialY, Affine.evalEval_polynomialY]; ring1

Goal state after:
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
⊢ (W'⁄B).polynomial = (MvPolynomial.map ↑f) (W'⁄A).polynomial

Tactic:
← map_polynomial,

Goal state after:
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
⊢ (W'⁄B).polynomial = ((W'⁄A).map ↑f).polynomial
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
s : Set ↑(uliftFunctor.mapCocone c).pt
⊢ (∀ (j : J✝), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' ⇑Homeomorph.ulift.symm ⁻¹' s)) ↔ ∀ (i : J✝), IsOpen s

Tactic:
congr!

Goal state after:
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
s : Set ↑(uliftFunctor.mapCocone c).pt
a✝ : J✝
⊢ IsOpen (⇑(ConcreteCategory.hom (c.ι.app a✝)) ⁻¹' ⇑Homeomorph.ulift.symm ⁻¹' s) ↔ IsOpen s
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

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

Tactic:
simp only [Set.mem_range, ContinuousMap.coe_mk, Function.comp_apply, forall_exists_index]

Goal state after:
case refine_1.refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i j : 𝒰.I₀
y : ↑Y
⊢ ∀ (x_1 : ↑(𝒰.X i)) (h : (ConcreteCategory.hom (𝒰.f i)) x_1 = y) (x_2 : ↑(𝒰.X j))
    (h_1 : (ConcreteCategory.hom (𝒰.f j)) x_2 = y),
    (Hom.hom (x i)) (⋯.toHomeomorph.symm ⟨y, ⋯⟩) = (Hom.hom (x j)) (⋯.toHomeomorph.symm ⟨y, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: P : MorphismProperty Scheme
F : Schemeᵒᵖ ⥤ Type u_1
inst✝¹ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : Finite 𝒰.I₀
this✝ : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f) ↔
    Presieve.IsSheafFor F (Presieve.singleton (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f))

Tactic:
congr!

Goal state after:
P : MorphismProperty Scheme
F : Schemeᵒᵖ ⥤ Type u_1
inst✝¹ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : Finite 𝒰.I₀
this✝ : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f = Presieve.singleton (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)
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✝ : EssFiniteType R A
p : PrimeSpectrum A
this✝ : EssFiniteType A (Localization.AtPrime p.asIdeal)
this : EssFiniteType R (Localization.AtPrime p.asIdeal)
⊢ Module.Projective (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R]

Tactic:
exact ⟨fun _ ↦ Module.free_of_flat_of_isLocalRing, fun _ ↦ inferInstance⟩

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

Goal state before:
pp: case pos
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝² : CommRing B
x✝¹ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
a : (i : I) → A i →ₐ[R] B ⧸ Ideal.span {1 - e i}
ha : ∀ (i : I) (x : A i), (Ideal.Quotient.mk (J' i)) ((a i) x) = (ι i) (g (Pi.single i x))
x✝ : (i : I) → A i
i : I
x : A i
y : B
hy : (Ideal.Quotient.mk (Ideal.span {1 - e i})) y = (a i) x
hy' : (Ideal.Quotient.mk (Ideal.span {1 - e i})) (y * e i) = (a i) x
⊢ (a i) (Pi.single i x i) = (Ideal.Quotient.mk (Ideal.span {1 - e i})) (y * e i)

Tactic:
rw [Pi.single_eq_same, hy']

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
I : Ideal R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Algebra S R
r : S
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ (transitionMap I R hmn) ((algebraMap S ((n : ℕ) → R ⧸ I ^ n • ⊤)) r n✝) =
    (algebraMap S ((n : ℕ) → R ⧸ I ^ n • ⊤)) r m✝

Tactic:
simp only [Pi.algebraMap_apply,
        IsScalarTower.algebraMap_apply S R (R ⧸ (I ^ _ • ⊤ : Ideal R)),
        Ideal.Quotient.algebraMap_eq, mapQ_eq_factor]
      rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) =
    ↑(piEquivOfFintype I fun x ↦ R).symm ∘ₗ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)

Tactic:
rw [← piEquivOfFintype_comp_ofTensorProduct_eq I ι, ← LinearMap.comp_assoc]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) =
    (↑(piEquivOfFintype I fun x ↦ R).symm ∘ₗ ↑(piEquivOfFintype I fun x ↦ R)) ∘ₗ ofTensorProduct I (ι → R)
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R✝¹ : Type u_1
S✝ : Type u_2
inst✝⁹ : CommRing R✝¹
inst✝⁸ : CommRing S✝
I✝ : Ideal R✝¹
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝¹ M
R✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
⊢ (Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom = (f m✝).toRingHom

Tactic:
ext x; exact congr($(hf hle) x)

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

Goal state before:
pp: R✝¹ : Type u_1
S✝ : Type u_2
inst✝⁹ : CommRing R✝¹
inst✝⁸ : CommRing S✝
I✝ : Ideal R✝¹
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝¹ M
R✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
r : R
n m✝ n✝ : ℕ
hle : m✝ ≤ n✝
⊢ (Ideal.Quotient.factorPow ?m.137 hle).comp (?m.138 n✝) = ?m.138 m✝

Tactic:
ext x; exact congr($(hf hle) x)

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

Goal state before:
pp: S : Type u_5
inst✝⁴ : CommRing S
I : Ideal S
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
n : ℕ
x : A
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
⊢ (Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom = (f m✝).toRingHom

Tactic:
ext x; exact congr($(hf hle) x)

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

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

Tactic:
simp only [evalₐ, AlgHom.coe_comp, Function.comp_apply, AlgHom.ofLinearMap_apply]

Goal state after:
S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n)) ((ofAlgEquiv I).symm x) = ↑(Ideal.quotientEquivAlgOfEq S ⋯) ((eval I S n) x)
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case refine_2
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
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ (map I g).ker
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
hb : ∀ (n : ℕ), g (↑b n) ∈ I ^ n • ⊤
a : (n : ℕ) → ↑{a | f a - ↑b (k + n) ∈ I ^ (k + n) • ⊤} := mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ Submodule.Quotient.mk (f ↑(a n)) = Submodule.Quotient.mk (↑b (k + n))

Tactic:
Submodule.Quotient.eq

Goal state after:
case refine_2
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
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ (map I g).ker
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
hb : ∀ (n : ℕ), g (↑b n) ∈ I ^ n • ⊤
a : (n : ℕ) → ↑{a | f a - ↑b (k + n) ∈ I ^ (k + n) • ⊤} := mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ f ↑(a n) - ↑b (k + n) ∈ I ^ n • ⊤
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case refine_2
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
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ (map I g).ker
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
hb : ∀ (n : ℕ), g (↑b n) ∈ I ^ n • ⊤
a : (n : ℕ) → ↑{a | f a - ↑b (k + n) ∈ I ^ (k + n) • ⊤} := mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ Submodule.Quotient.mk (f ↑(a n)) = Submodule.Quotient.mk (↑b (k + n))

Tactic:
rw [Submodule.Quotient.eq]

Goal state after:
case refine_2
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
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ (map I g).ker
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
hb : ∀ (n : ℕ), g (↑b n) ∈ I ^ n • ⊤
a : (n : ℕ) → ↑{a | f a - ↑b (k + n) ∈ I ^ (k + n) • ⊤} := mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ f ↑(a n) - ↑b (k + n) ∈ I ^ n • ⊤
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : Finite σ
val✝ : Fintype σ
⊢ (P.ofAlgEquiv e).jacobian = e P.jacobian

Tactic:
jacobian_eq_jacobiMatrix_det,

Goal state after:
case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : Finite σ
val✝ : Fintype σ
⊢ (algebraMap (P.ofAlgEquiv e).Ring T) (P.ofAlgEquiv e).jacobiMatrix.det = e P.jacobian
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
⊢ (ofBijectiveAlgebraMap h).jacobian = 1

Tactic:
jacobian_eq_jacobiMatrix_det,

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
⊢ (algebraMap (ofBijectiveAlgebraMap h).Ring S) (ofBijectiveAlgebraMap h).jacobiMatrix.det = 1
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
r : R
inst✝ : IsLocalization.Away r S
⊢ (localizationAway S r).jacobian = (algebraMap R S) r

Tactic:
jacobian_eq_jacobiMatrix_det,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap (localizationAway S r).Ring S) (localizationAway S r).jacobiMatrix.det = (algebraMap R S) r
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
ι' : 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 : σ'
⊢ (aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P).jacobiMatrix (Sum.inl j) (Sum.inl i)) = Q.jacobiMatrix j i

Tactic:
rw [jacobiMatrix_apply, jacobiMatrix_apply, comp_map, Sum.elim_inl,
    ← Q.comp_aeval_relation_inl P.toPresentation]
  apply aeval_sumElim_pderiv_inl

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
ι' : 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 σ'
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det = Q.jacobian

Tactic:
jacobian_eq_jacobiMatrix_det,

Goal state after:
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 σ'
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det = (algebraMap Q.Ring T) Q.jacobiMatrix.det
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case intro.intro
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✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ'
val✝ : Fintype σ
⊢ (Q.comp P).jacobian = P.jacobian • Q.jacobian

Tactic:
jacobian_eq_jacobiMatrix_det,

Goal state after:
case intro.intro
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✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ'
val✝ : Fintype σ
⊢ (algebraMap (Q.comp P).Ring T) (Q.comp P).jacobiMatrix.det = P.jacobian • Q.jacobian
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 σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ (LinearMap.toMatrix' P.aevalDifferential).det = P.jacobian

Tactic:
jacobian_eq_jacobiMatrix_det,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ (LinearMap.toMatrix' P.aevalDifferential).det = (algebraMap P.Ring S) P.jacobiMatrix.det
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 ι σ
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
⊢ ∃ v, ∑ i, v i * P.relation i = P.jacobiMatrix.det * P.σ ↑⋯.unit⁻¹ - 1

Tactic:
have H : P.jacobiMatrix.det * P.σ ↑(P.jacobian_isUnit.unit⁻¹) - 1 ∈ P.ker := by
    simp [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
  rwa [← P.span_range_relation_eq_ker, Ideal.mem_span_range_iff_exists_fun] at H

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✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h✝ : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this✝ : eₚ = ↑b.repr.symm
heₚ : Function.Bijective ⇑eₚ
this : Finite κ
g : S
hg : g ∉ p
h : Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers g)) e)
l₁ₜ : (κ →₀ S) →ₗ[S] κ →₀ Localization.Away g := Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.Away g))
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
let l₂ₜ : Ω[S⁄R] →ₗ[S] Ω[Localization.Away g⁄R] :=
    map R R S (Localization.Away g)

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h✝ : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this✝ : eₚ = ↑b.repr.symm
heₚ : Function.Bijective ⇑eₚ
this : Finite κ
g : S
hg : g ∉ p
h : Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers g)) e)
l₁ₜ : (κ →₀ S) →ₗ[S] κ →₀ Localization.Away g := Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.Away g))
l₂ₜ : Ω[S⁄R] →ₗ[S] Ω[Localization.Away g⁄R] := map R R S (Localization.Away g)
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)