mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ ψ : K →+* ℂ
h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)
⊢ ∃ σ, φ.comp ↑σ.symm = ψ

Tactic:
let := (φ.comp (algebraMap k K)).toAlgebra
  let := φ.toAlgebra
  have : IsScalarTower k K ℂ := IsScalarTower.of_algebraMap_eq' rfl
  let ψ' : K →ₐ[k] ℂ := { ψ with commutes' := fun r ↦ (RingHom.congr_fun h r).symm }
  use (AlgHom.restrictNormal' ψ' K).symm
  ext1 x
  exact AlgHom.restrictNormal_commutes ψ' K x

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

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsLeft R
⊢ (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)

Tactic:
p

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsLeft R
p : MvPowerSeries σ R
⊢ (monomial n) r * p = 0 → p = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsRight R
⊢ (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)

Tactic:
p

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsRight R
p : MvPowerSeries σ R
⊢ p * (monomial n) r = 0 → p = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
exact ENat.natCast_toNat (ne_top_of_lt (by simpa))

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

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ ↑(weightedOrder w g).toNat = weightedOrder w g

Tactic:
exact ENat.natCast_toNat (ne_top_of_lt (by simpa))

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
⊢ ‖x‖ < 1 ↔ v x < 1

Tactic:
rw [← map_one val.v, ← v.restrict_lt_iff]
  simpa only [map_one] using! (Valuation.RankOne.strictMono val.v).lt_iff_lt (b := 1)

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

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : constantCoeff φ = ↑u
⊢ u = Units.mk0 (constantCoeff φ) ⋯

Tactic:
Units.ext_iff

Goal state after:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : constantCoeff φ = ↑u
⊢ ↑u = ↑(Units.mk0 (constantCoeff φ) ⋯)
Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) ((rescale a) p) = (coeff n) ((rescale a) q)
⊢ ∀ (n : ℕ), (coeff n) p = (coeff n) q

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) ((rescale a) p) = (coeff n) ((rescale a) q)
n : ℕ
⊢ (coeff n) p = (coeff n) q
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: R : Type u_1
k : Type u_2
inst✝ : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := ↑u
hu : u₀ = ↑u
h₀ : IsUnit u₀
⊢ u₀.Unit_of_divided_by_X_pow_order⁻¹ = u⁻¹

Tactic:
inv_inj,

Goal state after:
R : Type u_1
k : Type u_2
inst✝ : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := ↑u
hu : u₀ = ↑u
h₀ : IsUnit u₀
⊢ u₀.Unit_of_divided_by_X_pow_order = u
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negAddY P (W'.neg P) + -3 * (P y - W'.negY P) * 0 -
      (W'.dblZ P +
        -3 * (P y - W'.negY P) *
          (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3))) =
    0

Tactic:
rw [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hf : Presieve.IsSeparated J F
⊢ Presieve.IsSeparatedFor F E.presieve₀

Tactic:
rw [Presieve.isSeparatedFor_iff_generate]
    exact hf _ E.mem₀

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

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

Tactic:
Mono.right_cancellation _ _ pullback.condition

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : i = j
⊢ (ConcreteCategory.hom (F.map (pullback.snd (c.inj j) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) j)) a) =
    (ConcreteCategory.hom (F.map (pullback.snd (c.inj j) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) j)) a)
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
f : R →+* S
⊢ (W'.map f).polynomialY = (MvPolynomial.map f) W'.polynomialY

Tactic:
simp only [polynomialY, map_polynomial, pderiv_map]

Goal state after:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case w
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (1 + (aeval x) (derivative (minpoly K pb.gen)) * u) * (aeval x) (minpoly K pb.gen) ∈ I ^ 2

pp: case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (u * (aeval x) (minpoly K pb.gen)) ^ 2 = 0

Tactic:
pow_two,

Goal state after:
case w
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (1 + (aeval x) (derivative (minpoly K pb.gen)) * u) * (aeval x) (minpoly K pb.gen) ∈ I * I

case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (u * (aeval x) (minpoly K pb.gen)) ^ 2 = 0
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: 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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
a b : AdicCauchySequence I M
⊢ ⟨fun n ↦ f (↑(a + b) n), ⋯⟩ = ⟨fun n ↦ f (↑a n), ⋯⟩ + ⟨fun n ↦ f (↑b n), ⋯⟩

Tactic:
by ext n; simp

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

Goal state before:
pp: 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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : R
a : AdicCauchySequence I M
⊢ ⟨fun n ↦ f (↑(r • a) n), ⋯⟩ = (RingHom.id R) r • ⟨fun n ↦ f (↑a n), ⋯⟩

Tactic:
by ext n; simp

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

Goal state before:
pp: 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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
n✝ : ℕ
⊢ (reduceModIdeal (I ^ n✝) f) ((evalₐ I n✝) r • ↑x n✝) = (evalₐ I n✝) r • (reduceModIdeal (I ^ n✝) f) (↑x n✝)

Tactic:
map_smul

Goal state after:
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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
n✝ : ℕ
⊢ (evalₐ I n✝) r • (reduceModIdeal (I ^ n✝) f) (↑x n✝) = (evalₐ I n✝) r • (reduceModIdeal (I ^ n✝) f) (↑x n✝)
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 : AdicCompletion I R
⊢ r • 0 = 0

Tactic:
by ext n; simp

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 : AdicCompletion I R
x y : AdicCompletion I M
⊢ r • (x + y) = r • x + r • y

Tactic:
by ext n; simp

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
x : AdicCompletion I M
⊢ 0 • x = 0

Tactic:
by ext n; 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
⊢ Function.Exact ⇑(map I f) ⇑(map I g)

Tactic:
refine LinearMap.exact_of_comp_eq_zero_of_ker_le_range ?_ (fun y ↦ ?_)

Goal state after:
case refine_1
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
⊢ map I g ∘ₗ map I f = 0

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
⊢ y ∈ (map I g).ker → y ∈ (map I f).range
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✝
g✝ : M✝ →ₗ[R✝] P✝
s✝ : M✝ →ₗ[R✝] K✝
κ✝ : Type u_6
σ✝ : Type u_7
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
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
c : κ ⊕ σ →₀ R
h : (c.sum fun i a ↦ a • v i) ∈ s.ker
this : (c.sum fun i a ↦ a • v i) ∈ Submodule.span R (Set.range v)
⊢ g (c.sum fun i a ↦ a • v i) ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

Tactic:
simp only [LinearMap.mem_ker, Finsupp.sum, map_sum, map_smul,
    Finset.sum_sum_eq_sum_toLeft_add_sum_toRight, map_add, hslzero, smul_zero,
    Finset.sum_const_zero, zero_add] at h

Goal state after:
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✝
g✝ : M✝ →ₗ[R✝] P✝
s✝ : M✝ →ₗ[R✝] K✝
κ✝ : Type u_6
σ✝ : Type u_7
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
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
c : κ ⊕ σ →₀ R
this : (c.sum fun i a ↦ a • v i) ∈ Submodule.span R (Set.range v)
h : ∑ x ∈ c.support.toRight, c (Sum.inr x) • s (v (Sum.inr x)) = 0
⊢ g (c.sum fun i a ↦ a • v i) ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: case h
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 ι σ
i j : σ
⊢ P.cotangentComplexAux (Cotangent.mk ⟨P.relation i, ⋯⟩) j = P.basisDeriv i j

Tactic:
P.cotangentComplexAux_apply

Goal state after:
case h
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 ι σ
i j : σ
⊢ (aeval P.val) ((pderiv (P.map j)) ↑⟨P.relation i, ⋯⟩) = P.basisDeriv i j
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
n : ℕ
inst✝ : IsStandardSmoothOfRelativeDimension n R S
w✝³ w✝² : Type
w✝¹ : Finite w✝²
w✝ : Finite w✝³
P : SubmersivePresentation R S w✝³ w✝²
hP : P.dimension = n
⊢ Module.rank S Ω[S⁄R] = ↑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
n : ℕ
inst✝ : IsStandardSmoothOfRelativeDimension n R S
w✝³ w✝² : Type
w✝¹ : Finite w✝²
w✝ : Finite w✝³
P : SubmersivePresentation R S w✝³ w✝²
hP : P.dimension = n
⊢ ↑P.dimension = ↑n
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})
⊢ ((localizationAway T g).comp P).ker =
    Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}

Tactic:
rw [ker_comp_eq_sup, Algebra.Generators.map_toComp_ker, this,
    Ideal.comap_map_of_surjective _ (toAlgHom_ofComp_surjective _ P), ← RingHom.ker_eq_comap_bot,
    ← sup_assoc]

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.span {(rename Sum.inr) f * X (Sum.inl ()) - 1} ⊔
      RingHom.ker ((localizationAway T g).ofComp P).toAlgHom =
    RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: ⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Etale

Tactic:
by
  rw [eq_formallyUnramified_and_smooth]
  exact FormallyUnramified.stableUnderComposition.and Smooth.stableUnderComposition

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
D : DescentAux A B
⊢ D.P.coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)

Tactic:
Subalgebra.setRange_algebraMap

Goal state after:
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
⊢ D.P.coeffs ⊆ ↑(subalgebra R D)
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
D : DescentAux A B
i : D.vars
this : ↑(D.h i).coeffs ⊆ ⋃ i, ↑(D.h i).coeffs
⊢ ↑(D.h i).coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)

Tactic:
Subalgebra.setRange_algebraMap

Goal state after:
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
i : D.vars
this : ↑(D.h i).coeffs ⊆ ⋃ i, ↑(D.h i).coeffs
⊢ ↑(D.h i).coeffs ⊆ ↑(subalgebra R D)
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
D : DescentAux A B
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ ↑(D.p i).coeffs
this : ↑p.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs
⊢ ↑p.coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)

Tactic:
Subalgebra.setRange_algebraMap

Goal state after:
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
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ ↑(D.p i).coeffs
this : ↑p.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs
⊢ ↑p.coeffs ⊆ ↑(subalgebra R D)
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
D : DescentAux A B
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ ↑(D.q i).coeffs
this : ↑q.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x)
⊢ ↑q.coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)

Tactic:
Subalgebra.setRange_algebraMap

Goal state after:
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
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ ↑(D.q i).coeffs
this : ↑q.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x)
⊢ ↑q.coeffs ⊆ ↑(subalgebra R D)
Module: Mathlib.RingTheory.Smooth.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
⊢ Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range Subtype.val))) L

Tactic:
convert! H <;> simp

Goal state after: