mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (map (algebraMap F E) p).Splits
hp : Irreducible p
⊢ MulAction.IsPretransitive p.Gal ↑(p.rootSet E)

Tactic:
refine ⟨fun x y ↦ ?_⟩

Goal state after:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (map (algebraMap F E) p).Splits
hp : Irreducible p
x y : ↑(p.rootSet E)
⊢ ∃ g, g • x = y
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
⊢ ∃ C > 0, ∀ (z : ℂ), ‖f z‖ ≤ C

Tactic:
by
    rcases isBounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
    exact
      ⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z =>
        (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
⊢ Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b

Tactic:
by rw [← hIcc, eL.symm_preimage_preimage]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ k ≤ p.roots.card

Tactic:
hroots

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ k ≤ p.natDegree
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e'_5
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ p.natDegree - k = p.roots.card - k

Tactic:
hroots

Goal state after:
case e'_5
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ p.natDegree - k = p.natDegree - k
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e'_6
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ p.natDegree - k = p.roots.card - k

Tactic:
hroots

Goal state after:
case e'_6
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ p.natDegree - k = p.natDegree - k
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
φ : K →+* A
hz : (fun φ ↦ φ x) φ ∈ (map (algebraMap ℚ A) (minpoly ℚ x)).roots.toFinset
⊢ ‖(fun φ ↦ φ x) φ‖ ≤ B

Tactic:
exact h φ

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B
i : ℕ
⊢ ‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))

Tactic:
have hx := Algebra.IsSeparable.isIntegral ℚ x
  rw [← norm_algebraMap' A, ← coeff_map (algebraMap ℚ A)]
  refine coeff_bdd_of_roots_le _ (minpoly.monic hx)
      (IsAlgClosed.splits _) (minpoly.natDegree_le x) (fun z hz => ?_) i
  classical
  rw [← Multiset.mem_toFinset] at hz
  obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
  exact h φ

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
⊢ StrictMono ⇑e

Tactic:
simp only [AddMonoidHom.coe_toMultiplicativeRight, AddMonoidHom.coe_coe, e]

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
⊢ StrictMono (⇑ofAdd ∘ ⇑f ∘ ⇑Additive.ofMul)
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case pos
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
⊢ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f a‖

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons]

Goal state after:
case pos
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
⊢ ‖f a * (Multiset.map f t).prod‖ ≤ ‖f a‖
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case neg
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
⊢ ∃ i, (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Tactic:
rcases eq_or_ne t 0 with rfl | ht

Goal state after:
case neg.inl
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a M : ι
hMa : ‖f a‖ < ‖f M‖
hMs : 0 ≠ 0 → M ∈ 0
hM : ‖(Multiset.map f 0).prod‖ ≤ ‖f M‖
⊢ ∃ i, (a ::ₘ 0 ≠ 0 → i ∈ a ::ₘ 0) ∧ ‖(Multiset.map f (a ::ₘ 0)).prod‖ ≤ ‖f i‖

case neg.inr
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
⊢ ∃ i, (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case neg.inr.refine_2
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
⊢ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f M‖

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons]

Goal state after:
case neg.inr.refine_2
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
⊢ ‖f a * (Multiset.map f t).prod‖ ≤ ‖f M‖
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
R : Type u_2
k : Type u_3
inst✝ : Field k
⊢ 1⁻¹ = 1

Tactic:
by
      rw [MvPowerSeries.inv_eq_iff_mul_eq_one, mul_one]
      simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x y : K
w : HeightOneSpectrum (𝓞 K)
hw : place (embedding w) = ↑v
H : ∀ (x : K), v x = (HeightOneSpectrum.adicAbv K w) x
⊢ v (x + y) ≤ max (v x) (v y)

Tactic:
simpa only [H] using adicAbv_add_le_max K w x y

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 3)
⊢ (ofJ0 R).IsElliptic

Tactic:
rw [isElliptic_iff, ofJ0_Δ]
  convert! (hu.out.pow 3).neg
  norm_num1

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows

Tactic:
apply Presieve.isSheafFor_subsieve_aux (S := .generate (.ofArrows 𝒰.X 𝒰.f))

Goal state after:
case h
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows ≤ (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows

case hS
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f)).arrows

case trans
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ S⦄,
    (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f →
      Presieve.IsSeparatedFor F (Sieve.pullback f (Sieve.generate (Presieve.ofArrows 𝒰.X 𝒰.f))).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
⊢ ∀ (gi : Z ⟶ E.X i) (gj : Z ⟶ E.X j),
    gi ≫ E.f i = gj ≫ E.f j → (ConcreteCategory.hom (F.map gi.op)) (s i) = (ConcreteCategory.hom (F.map gj.op)) (s j)

Tactic:
gi

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
⊢ ∀ (gj : Z ⟶ E.X j),
    gi ≫ E.f i = gj ≫ E.f j → (ConcreteCategory.hom (F.map gi.op)) (s i) = (ConcreteCategory.hom (F.map gj.op)) (s j)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ ¬(P x / P z = Q x / Q z ∧ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z))

Tactic:
rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
this :
  W.Nonsingular
    ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
      1]
hx : P x * Q z = Q x * P z
⊢ W.Nonsingular (W.add P Q)

Tactic:
simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hQz hx <|
              not_and.mp hxy hx]

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:
by
  rw [← map_polynomial, map_baseChange]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsLocalRing S
inst✝³ : Algebra R S
P : Extension R S
inst✝² : FormallySmooth R P.Ring
inst✝¹ : Module.Free P.Ring Ω[P.Ring⁄R]
inst✝ : Module.Finite P.Ring Ω[P.Ring⁄R]
h' : P.ker.FG
⊢ FormallySmooth R S ↔ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P.cotangentComplex)

Tactic:
by
  have : Module.Finite P.Ring P.Cotangent :=
    have : Module.Finite P.Ring P.ker := .of_fg h'
    .of_surjective _ Extension.Cotangent.mk_surjective
  have : Module.Finite S P.Cotangent := Module.Finite.of_restrictScalars_finite P.Ring _ _
  rw [← IsLocalRing.split_injective_iff_lTensor_residueField_injective,
    P.formallySmooth_iff_split_injection]

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 : R ⧸ I • ⊤
b₁ b₂ : R
h : b₁ ≈ b₂
a✝ : M
⊢ b₁ - b₂ ∈ I

Tactic:
show I = I • ⊤ by simp,

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 : R ⧸ I • ⊤
b₁ b₂ : R
h : b₁ ≈ b₂
a✝ : M
⊢ b₁ - b₂ ∈ I • ⊤
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: 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
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 : ℕ
⊢ ↑(a (n + 1)) ≡ ↑(a n) [SMOD I ^ n • ⊤]

Tactic:
simp [a, mapExactAux, SModEq]

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 σ
P : SubmersivePresentation R S ι σ
⊢ LinearIndependent S fun i j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Tactic:
by
  simp_rw [← SubmersivePresentation.basisDeriv_apply]
  exact P.basisDeriv.linearIndependent

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 : SubmersivePresentation R S ι σ
⊢ Function.Injective ⇑P.cotangentComplexAux

Tactic:
rw [← LinearMap.ker_eq_bot, eq_bot_iff]
  intro x hx
  obtain ⟨(x : P.ker), rfl⟩ := Cotangent.mk_surjective x
  rw [Submodule.mem_bot, Cotangent.mk_eq_zero_iff]
  rw [LinearMap.mem_ker, P.cotangentComplexAux_zero_iff] at hx
  have : x.val ∈ Ideal.span (Set.range P.relation) := by
    rw [P.span_range_relation_eq_ker]
    exact x.property
  obtain ⟨c, hc⟩ := Finsupp.mem_ideal_span_range_iff_exists_finsupp.mp this
  have heq (i : σ) :
      aeval P.val (pderiv (P.map i) <| c.sum fun i a ↦ a * P.relation i) = 0 := by
    rw [hc]
    apply hx
  simp only [Finsupp.sum, map_sum, Derivation.leibniz, smul_eq_mul, map_add, map_mul,
    Presentation.aeval_val_relation, zero_mul, add_zero] at heq
  have heq2 : ∑ i ∈ c.support,
      aeval P.val (c i) • (fun j ↦ aeval P.val (pderiv (P.map j) (P.relation i))) = 0 := by
    ext j
    simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply]
    apply heq
  have (i : σ) : aeval P.val (c i) = 0 := by
    have := P.linearIndependent_aeval_val_pderiv_relation
    rw [linearIndependent_iff''] at this
    have := this c.support (fun i ↦ aeval P.val (c i))
      (by intro i; simp only [Finsupp.mem_support_iff, ne_eq, not_not]; intro h; simp [h]) heq2
    exact this i
  change _ ∈ P.ker ^ 2
  rw [← hc]
  apply Ideal.sum_mem
  intro i hi
  rw [pow_two]
  apply Ideal.mul_mem_mul
  · rw [P.ker_eq_ker_aeval_val]
    simpa using this i
  · exact P.relation_mem_ker i

Goal state after:
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 ι
a : ((localizationAway T g).comp P).Ring
hx : ((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) * a ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}
⊢ (compLocalizationAwayAlgHom T g P) (((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) * a) = 0

Tactic:
rw [map_mul, compLocalizationAwayAlgHom_relation_eq_zero, zero_mul]

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
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 ∈ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))

Tactic:
MvPolynomial.mem_range_map_iff_coeffs_subset,

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 ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)
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 ∈ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))

Tactic:
MvPolynomial.mem_range_map_iff_coeffs_subset,

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 ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ (LinearMap.liftBaseChange S
        (Extension.Cotangent.map ((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom))
      (D.tensorCotangentEquiv.symm (b r)) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
tensorCotangentEquiv_symm_apply,

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ (LinearMap.liftBaseChange S
        (Extension.Cotangent.map ((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom))
      (1 ⊗ₜ[D.T] Extension.Cotangent.mk (D.kerGen r)) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩