mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_1
X : TopCat
E : precoverage.ZeroHypercover X
⊢ Presieve.map uliftFunctor E.presieve₀ ∈
    (Precoverage.comap (forget TopCat) Types.jointlySurjectivePrecoverage).coverings (uliftFunctor.obj X)

pp: case refine_2
X : TopCat
E : precoverage.ZeroHypercover X
⊢ Presieve.map uliftFunctor E.presieve₀ ∈ isOpenEmbedding.precoverage.coverings (uliftFunctor.obj X)

Tactic:
· simp only [Presieve.map_ofArrows, Precoverage.mem_comap_iff,
      Types.ofArrows_mem_jointlySurjectivePrecoverage_iff, ConcreteCategory.hom_ofHom,
      Set.mem_range, TypeCat.Fun.coe_mk]
    intro ⟨x⟩
    obtain ⟨i, y, rfl⟩ := exists_mem_zeroHypercover_range E x
    use i, ⟨y⟩
    rfl

Goal state after:
case refine_2
X : TopCat
E : precoverage.ZeroHypercover X
⊢ Presieve.map uliftFunctor E.presieve₀ ∈ isOpenEmbedding.precoverage.coverings (uliftFunctor.obj X)
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: case intro.mpr
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
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Tactic:
obtain ⟨e, he, he'⟩ := ((CompleteOrthogonalIdempotents.single A).map
      g.toRingHom).lift_of_isNilpotent_ker (Ideal.Quotient.mk J) hJ'
        fun _ ↦ Ideal.Quotient.mk_surjective _

Goal state after:
case intro.mpr
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' : ⇑(Ideal.Quotient.mk J) ∘ e = ⇑g.toRingHom ∘ fun x ↦ Pi.single x 1
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g
Module: Mathlib.RingTheory.Unramified.Pi

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

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

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

Goal state after:
case map_mul
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
⊢ ∀ (x_1 y : f x),
    (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) (x_1 * y) =
      (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) x_1 *
        (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) y
Module: Mathlib.RingTheory.Etale.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✝ : IsEtaleAt R P
⊢ ∃ f ∉ P, Etale R (Localization.Away f)

Tactic:
obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, hpr, hr⟩ :=
    PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open
      (show ⟨P, ‹_›⟩ ∈ etaleLocus R A by assumption) isOpen_etaleLocus

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✝ : IsEtaleAt R P
r : A
hpr : { asIdeal := P, isPrime := inst✝¹ } ∈ ↑(PrimeSpectrum.basicOpen r)
hr : ↑(PrimeSpectrum.basicOpen r) ⊆ etaleLocus R A
⊢ ∃ f ∉ P, Etale R (Localization.Away f)
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]
        rw [← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq,
          ← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq,
          ← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq]
        simp only [LinearMap.coe_comp, Derivation.coeFn_coe, Function.comp_apply,
          Derivation.leibniz, mk_apply, mulActionBaseChange_smul_tmul, TensorProduct.tmul_add]

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

Goal state before:
pp: case right
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ I ^ n • ⊤
y2 : N
hy2 : y2 ∈ I ^ n • ⊤
x1 : M
hx1 : x1 ∈ I ^ n • ⊤
hx1' : f x1 ≡ y1 [SMOD I ^ (n + 1) • ⊤]
x2 : M
hx2 : x2 ∈ I ^ n • ⊤
hx2' : f x2 ≡ y2 [SMOD I ^ (n + 1) • ⊤]
⊢ f (x1 + x2) ≡ y1 + y2 [SMOD I ^ (n + 1) • ⊤]

Tactic:
simp only [map_add]

Goal state after:
case right
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ I ^ n • ⊤
y2 : N
hy2 : y2 ∈ I ^ n • ⊤
x1 : M
hx1 : x1 ∈ I ^ n • ⊤
hx1' : f x1 ≡ y1 [SMOD I ^ (n + 1) • ⊤]
x2 : M
hx2 : x2 ∈ I ^ n • ⊤
hx2' : f x2 ≡ y2 [SMOD I ^ (n + 1) • ⊤]
⊢ f x1 + f x2 ≡ y1 + y2 [SMOD I ^ (n + 1) • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: case h
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 s : R
x : M
⊢ (Ideal.Quotient.mk (I • ⊤)) (r • s) • Submodule.Quotient.mk x = r • Submodule.Quotient.mk s • Submodule.Quotient.mk x

Tactic:
mk_smul_mk,

Goal state after:
case h
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 s : R
x : M
⊢ (r • s) • Submodule.Quotient.mk x = r • Submodule.Quotient.mk s • Submodule.Quotient.mk x
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
b : AdicCompletion I M
⊢ 1 • b = b

Tactic:
ext n
    simp only [smul_eval, val_one, one_smul]

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
x y : R
⊢ ⟨fun n ↦ (factor ⋯) ((f n) (x + y)), ⋯⟩ = ⟨fun n ↦ (factor ⋯) ((f n) x), ⋯⟩ + ⟨fun n ↦ (factor ⋯) ((f n) y), ⋯⟩

Tactic:
simp only [map_add]

Goal state after:
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
x y : R
⊢ ⟨fun n ↦ (factor ⋯) ((f n) x) + (factor ⋯) ((f n) y), ⋯⟩ =
    ⟨fun n ↦ (factor ⋯) ((f n) x), ⋯⟩ + ⟨fun n ↦ (factor ⋯) ((f n) y), ⋯⟩
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑(AlgebraTensorModule.map LinearMap.id f)

Tactic:
by
  rw [tensor_map_id_left_eq_map I f]
  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective,
    EquivLike.injective_comp]
  exact map_injective I hf

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup K
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R K
inst✝² : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
q : Submodule R M
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : E →ₗ[R] M
hi : Function.Injective ⇑i
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective ⇑↑(LinearEquiv.ofInjective i hi).symm

pp: case hg
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup K
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R K
inst✝² : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
q : Submodule R M
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : E →ₗ[R] M
hi : Function.Injective ⇑i
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective ⇑(i.range.projectionOnto q h ∘ₗ f)

Tactic:
· exact (LinearEquiv.ofInjective i hi).symm.bijective

Goal state after:
case hg
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup K
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R K
inst✝² : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
q : Submodule R M
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module R E
i : E →ₗ[R] M
hi : Function.Injective ⇑i
h : IsCompl i.range q
hker : Disjoint g.ker q
hmap : Submodule.map g q = ⊤
⊢ Function.Bijective ⇑(i.range.projectionOnto q h ∘ₗ f)
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
i : σ
⊢ P.cotangentComplexAux (Cotangent.mk x) i = (aeval P.val) ((pderiv (P.map i)) ↑x)

Tactic:
by
  dsimp only [cotangentComplexAux, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    cotangentComplex_mk]
  simp only [Generators.toExtension_Ring, Finsupp.lcomapDomain_apply,
    Finsupp.linearEquivFunOnFinite_apply, Finsupp.comapDomain_apply,
    Generators.cotangentSpaceBasis_repr_tmul, one_mul]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.negAddY (P x / P z) (P x / P z) (P y / P z) (-n / P z / d) =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2) +
          P y * P z ^ 2 * d ^ 3) /
        P z ^ 2 /
      (P z * d ^ 3)

Tactic:
rw [Affine.negAddY, toAffine_addX_of_eq hPz hd]
  simp [field]

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

Goal state before:
pp: case hsa
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 ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
⊢ ∀ (i : κ), P.sectionCotangent (P.cotangentSpaceBasis (f i)) = 0

Tactic:
intro i
    apply sectionCotangent_zero_of_notMem_range _ _
    simp [← hcompl.compl_eq]

Goal state after:
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
hZ : IsUnit (W.dblZ P)
⊢ ![W.dblX P, W.dblY P, W.dblZ P] =
    ![W.dblX P,
      W.dblZ P *
        ![W.dblX 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)),
            1]
          y,
      W.dblZ P *
        ![W.dblX 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)),
            1]
          z]

Tactic:
← dblY_of_Z_ne_zero 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
hZ : IsUnit (W.dblZ P)
⊢ ![W.dblX P, W.dblY P, W.dblZ P] =
    ![W.dblX P, W.dblZ P * ![W.dblX P / W.dblZ P, W.dblY P / W.dblZ P, 1] y,
      W.dblZ P * ![W.dblX P / W.dblZ P, W.dblY P / W.dblZ P, 1] z]
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
h : IsStandardSmooth R S
ι σ : Type
w✝ : Finite σ
left✝ : Finite ι
P : SubmersivePresentation R S ι σ
⊢ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(D R S)

Tactic:
exact ⟨_, P.basisKaehler, by simp [Set.range_subset_iff]⟩

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

Goal state before:
pp: case h
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 ι
Q : Generators S T Unit := ⋯
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ⋯
f : P.Ring ⧸ P.ker ^ 2 := ⋯
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) := ⋯
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : ↑⟨(fun x ↦ f ^ x) n, ⋯⟩ * (algebraMap P.Ring (P.Ring ⧸ P.ker ^ 2)) ↑x = 0
⊢ ⟨g ^ n, ⋯⟩ • Extension.Cotangent.mk x = 0

Tactic:
dsimp [f] at hm

Goal state after:
case h
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 ι
Q : Generators S T Unit := ⋯
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ⋯
f : P.Ring ⧸ P.ker ^ 2 := ⋯
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) := ⋯
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g) ^ n * (Ideal.Quotient.mk (P.ker ^ 2)) ↑x = 0
⊢ ⟨g ^ n, ⋯⟩ • Extension.Cotangent.mk x = 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 ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
hx : (Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom) x = cMulXSubOneCotangent T g
⊢ Extension.Cotangent.map ((localizationAway T g).ofComp P).toExtensionHom ∘ₗ cotangentCompAwaySec g P x = LinearMap.id

Tactic:
by
  refine (basisCotangentAway T g).ext fun r ↦ ?_
  simpa only [LinearMap.coe_comp, Function.comp_apply, basisCotangentAway_apply,
    cotangentCompAwaySec_apply]

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

Goal state before:
pp: case pos
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝ : x = 0
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) 0 = x

pp: case pos
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝¹ : ¬x = 0
h✝ : x = -1
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (-1) = x

pp: case neg
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝¹ : ¬x = 0
h✝ : ¬x = -1
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (Function.surjInv ⋯ x) = x

Tactic:
· next h => subst h; rfl

Goal state after:
case pos
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝¹ : ¬x = 0
h✝ : x = -1
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (-1) = x

case neg
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝¹ : ¬x = 0
h✝ : ¬x = -1
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (Function.surjInv ⋯ x) = x
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case pos
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝¹ : ¬x = 0
h✝ : x = -1
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (-1) = x

pp: case neg
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝¹ : ¬x = 0
h✝ : ¬x = -1
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (Function.surjInv ⋯ x) = x

Tactic:
· next h => subst h; rfl

Goal state after:
case neg
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
x : MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b))
h✝¹ : ¬x = 0
h✝ : ¬x = -1
⊢ (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) (Function.surjInv ⋯ x) = x
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).IsStandardSmooth
⊢ Algebra.IsStandardSmooth R T

Tactic:
rw [RingHom.IsStandardSmooth] at h

Goal state after:
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
⊢ Algebra.IsStandardSmooth R T
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
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
σ' : ι → ℕ
hσ' : ∀ (x : ι), σ x = p * σ' x
⊢ ∀ (a : ι), a ∈ σ.support ↔ σ' a ≠ 0

Tactic:
by simp [hσ', hp.ne_zero]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
⊢ FormallyUnramified (Spec.map φ)

Tactic:
rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified)]

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified