mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ∫ (θ : ℝ) in 0..2 * π, ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ < ∫ (x : ℝ) in 0..2 * π, R * C

Tactic:
simp only [deriv_circleMap, norm_smul, norm_mul, norm_circleMap_zero, abs_of_pos hR, norm_I,
        mul_one]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
⊢ ∫ (θ : ℝ) in 0..2 * π, R * ‖f (circleMap c R θ)‖ < ∫ (x : ℝ) in 0..2 * π, R * C
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
⊢ (rename ⇑e) (msymm σ R μ) = msymm τ R μ

Tactic:
rw [msymm, map_sum]
  apply Fintype.sum_equiv (Nat.Partition.ofSymShapeEquiv μ e)
  intro
  rw [← Multiset.prod_hom, Multiset.map_map, Nat.Partition.ofSymShapeEquiv]
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ Tendsto (fun x ↦ eval x p) (cocompact R) (cocompact R)

Tactic:
← Metric.cobounded_eq_cocompact,

Goal state after:
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ Tendsto (fun x ↦ eval x p) (Bornology.cobounded R) (Bornology.cobounded R)
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inr.inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
⊢ ‖(map f p).leadingCoeff * (-1) ^ ((map f p).natDegree - i) * (map f p).roots.esymm ((map f p).natDegree - i)‖ ≤
    B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Tactic:
(h1.map _).leadingCoeff,

Goal state after:
case inr.inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
⊢ ‖1 * (-1) ^ ((map f p).natDegree - i) * (map f p).roots.esymm ((map f p).natDegree - i)‖ ≤
    B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
this :
  ∀ (a b : Fin 1 → ℝ) (f : (Fin 1 → ℝ) → E),
    ∫ (x : Fin 1 → ℝ) in Set.Icc a b, f x = ∫ (x : ℝ) in Set.Icc (a 0) (b 0), f fun x_1 ↦ x
⊢ ∑ i,
      ((∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
          ![f, g] i (e.symm (i.insertNth (e b i) x))) -
        ∫ (x : Fin 1 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
          ![f, g] i (e.symm (i.insertNth (e a i) x))) =
    ((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) +
      ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2))

Tactic:
simp only [Fin.sum_univ_two, this]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
this :
  ∀ (a b : Fin 1 → ℝ) (f : (Fin 1 → ℝ) → E),
    ∫ (x : Fin 1 → ℝ) in Set.Icc a b, f x = ∫ (x : ℝ) in Set.Icc (a 0) (b 0), f fun x_1 ↦ x
⊢ ((∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 0) 0) ((e b ∘ Fin.succAbove 0) 0),
          ![f, g] 0 (e.symm (Fin.insertNth 0 (e b 0) fun x_1 ↦ x))) -
        ∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 0) 0) ((e b ∘ Fin.succAbove 0) 0),
          ![f, g] 0 (e.symm (Fin.insertNth 0 (e a 0) fun x_1 ↦ x))) +
      ((∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 1) 0) ((e b ∘ Fin.succAbove 1) 0),
          ![f, g] 1 (e.symm (Fin.insertNth 1 (e b 1) fun x_1 ↦ x))) -
        ∫ (x : ℝ) in Set.Icc ((e a ∘ Fin.succAbove 1) 0) ((e b ∘ Fin.succAbove 1) 0),
          ![f, g] 1 (e.symm (Fin.insertNth 1 (e a 1) fun x_1 ↦ x))) =
    ((∫ (y : ℝ) in Set.Icc a.2 b.2, f (b.1, y)) - ∫ (y : ℝ) in Set.Icc a.2 b.2, f (a.1, y)) +
      ((∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, b.2)) - ∫ (x : ℝ) in Set.Icc a.1 b.1, g (x, a.2))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁵ : Field K
A : Type u_2
inst✝⁴ : Field A
inst✝³ : CharZero A
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
inst✝ : IsAlgClosed A
f : K →ₐ[ℚ] A
⊢ Nonempty (K →+* A)

Tactic:
exact ⟨f.toRingHom⟩

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X ^ 2 - C ↑(2 * z.re) * X + C (↑‖z‖ ^ 2) = (X - C ((starRingEnd ℂ) z)) * (X - C z)

Tactic:
rw [← add_conj, map_add, ← mul_conj', map_mul]
      ring

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
p : Lex (σ →₀ ℕ)
hp : ↑p = φ.lexOrder
⊢ φ.lexOrder = ↑(toLex (ofLex p))

Tactic:
by simp only [toLex_ofLex, hp]

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
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
⊢ (∃ i, True ∧ {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U) ↔ ∃ i, U ∈ 𝓟 {p | v.norm (p.1 - p.2) < ↑i}

pp: case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun x ↦ 𝓟 {p | v.norm (p.1 - p.2) < ↑x}

Tactic:
· simp only [true_and, mem_principal, Subtype.exists, gt_iff_lt, exists_prop]
        refine ⟨fun ⟨ε, hε⟩ => ?_, fun ⟨r, hr_pos, hr⟩ => ?_⟩
        · set δ : ℝ≥0 := hv.hom _ ε with hδ
          have hδ_pos : 0 < δ := by
            rw [hδ, ← map_zero hv.hom]
            exact hv.strictMono _ (Units.zero_lt ε)
          use δ, hδ_pos
          apply subset_trans _ hε
          intro x hx
          simp only [mem_ofPred_eq, Valuation.norm, hδ, NNReal.coe_lt_coe] at hx
          rw [mem_ofPred, ← neg_sub, Valuation.map_neg]
          exact (RankOne.strictMono Valued.v).lt_iff_lt.mp hx
        · have : Nontrivial Γ₀ˣ := (nontrivial_iff_exists_ne (1 : Γ₀ˣ)).mpr
            ⟨RankOne.unit val.v, RankOne.unit_ne_one val.v⟩
          obtain ⟨u, hu⟩ := Real.exists_lt_of_strictMono hv.strictMono hr_pos
          use u
          apply subset_trans _ hr
          intro x hx
          simp only [Valuation.norm, mem_ofPred_eq]
          apply lt_trans _ hu
          rw [NNReal.coe_lt_coe, ← neg_sub, Valuation.map_neg]
          exact (RankOne.strictMono Valued.v).lt_iff_lt.mpr hx

Goal state after:
case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun x ↦ 𝓟 {p | v.norm (p.1 - p.2) < ↑x}
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ ∃ n, Associated (X ^ n) f

Tactic:
use f.order.toNat

Goal state after:
case h
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Associated (X ^ f.order.toNat) f
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹¹ : Field K
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Algebra R K
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : IsFractionRing R K
v✝ : HeightOneSpectrum R
L : Type u_3
inst✝⁶ : NumberField K
inst✝⁵ : Field L
inst✝⁴ : NumberField L
inst✝³ : Algebra K L
v : HeightOneSpectrum (𝓞 K)
w : HeightOneSpectrum (𝓞 L)
inst✝² : Algebra (adicCompletion K v) (adicCompletion L w)
inst✝¹ : ContinuousSMul (adicCompletion K v) (adicCompletion L w)
inst✝ : IsScalarTower K (adicCompletion K v) (adicCompletion L w)
Φ : adicCompletion K v ⊗[K] L →ₗ[adicCompletion K v] adicCompletion L w :=
  (Algebra.TensorProduct.lift (Algebra.algHom (adicCompletion K v) (adicCompletion K v) (adicCompletion L w))
      (Algebra.algHom K L (adicCompletion L w)) ⋯).toLinearMap
l : L
⊢ (algebraMap L (adicCompletion L w)) l ∈ Set.range ⇑Φ

Tactic:
exact ⟨1 ⊗ₜ l, by simp [Φ, Algebra.algHom]⟩

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP :
  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
⊢ (u • P) y ^ 2 * (u • P) z + W'.a₁ * (u • P) x * (u • P) y * (u • P) z + W'.a₃ * (u • P) y * (u • P) z ^ 2 -
          ((u • P) x ^ 3 + W'.a₂ * (u • P) x ^ 2 * (u • P) z + W'.a₄ * (u • P) x * (u • P) z ^ 2 +
            W'.a₆ * (u • P) z ^ 3) +
        u ^ 3 * 0 -
      (0 +
        u ^ 3 *
          (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:
simp only [smul_fin3_ext]; ring1

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

Goal state before:
pp: case neg
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
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z

Goal state after:
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
⊢ W.Nonsingular (W.add P Q)

case neg
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)
⊢ W.Nonsingular (W.add P Q)
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type u_1
inst✝ : Small.{w, u_1} α
X : α → C
c : Cofan X
hc : IsColimit c
⊢ have this := ⋯;
  (piComparison F fun x ↦ op (X x)) =
    F.map (opCoproductIsoProduct' hc (productIsProduct fun x ↦ op (X x))).inv ≫
      Equalizer.Presieve.Arrows.forkMap F X c.inj

Tactic:
have : HasCoproduct X := ⟨⟨c, hc⟩⟩
  dsimp only [Equalizer.Presieve.Arrows.forkMap]
  have h : Pi.lift (fun i ↦ F.map (c.inj i).op) =
      F.map (Pi.lift (fun i ↦ (c.inj i).op)) ≫ piComparison F _ := by simp
  rw [h, ← Category.assoc, ← Functor.map_comp]
  have hh : Pi.lift (fun i ↦ (c.inj i).op) = (productIsProduct (op <| X ·)).lift c.op := by
    simp [Pi.lift, productIsProduct]
  rw [hh, ← desc_op_comp_opCoproductIsoProduct'_hom hc]
  simp

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 →
      2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0 →
        b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a + 3 * W'.a₆) = 0

Tactic:
intro h ha hb

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
h :
  b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
      (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
    0
ha : W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0
hb : 2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0
⊢ b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a + 3 * W'.a₆) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
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
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z

Goal state after:
case pos
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
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

case neg
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)
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]

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

Goal state before:
pp: case e'_1
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
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))

pp: case e'_2
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
⊢ Module.Projective (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])

Tactic:
· have := IsLocalizedModule.iso p.asIdeal.primeCompl
      (H1Cotangent.map R R A (Localization.AtPrime p.asIdeal))
    exact this.subsingleton_congr.symm

Goal state after:
case e'_2
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
⊢ Module.Projective (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ Smooth) ((algebraMap S (Localization.Away ↑r)).comp f)
this : f.FinitePresentation
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation R S
⊢ Algebra.FormallySmooth R S

Tactic:
← Algebra.smoothLocus_eq_univ_iff,

Goal state after:
R S : Type u_6
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ Smooth) ((algebraMap S (Localization.Away ↑r)).comp f)
this : f.FinitePresentation
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation R S
⊢ Algebra.smoothLocus R S = Set.univ
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: 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
⊢ FormallyEtale K L

Tactic:
refine FormallyEtale.iff_comp_bijective.mpr fun B _ _ I h ↦ ?_

Goal state after:
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 = ⊥
⊢ Function.Bijective (Ideal.Quotient.mkₐ K I).comp
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
⊢ FormallyEtale K L

Tactic:
refine FormallyEtale.iff_comp_bijective.mpr fun B _ _ I h ↦ ?_

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
⊢ Function.Bijective (Ideal.Quotient.mkₐ K I).comp
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
A : Type u
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : EssFiniteType K A
inst✝ : FormallyUnramified K A
this✝ : IsReduced A
this : IsArtinianRing A
I : MaximalSpectrum A
⊢ FormallyEtale K (A ⧸ I.asIdeal)

Tactic:
rw [FormallyEtale.iff_isSeparable, ← FormallyUnramified.iff_isSeparable]

Goal state after:
K : Type u_1
A : Type u
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : EssFiniteType K A
inst✝ : FormallyUnramified K A
this✝ : IsReduced A
this : IsArtinianRing A
I : MaximalSpectrum A
⊢ FormallyUnramified K (A ⧸ I.asIdeal)
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
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ etaleLocus R A ↔ Etale R (Localization.Away f)

Tactic:
rw [basicOpen_subset_etaleLocus_iff]
  refine ⟨fun H ↦ ⟨H, inferInstance⟩, fun _ ↦ inferInstance⟩

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (S ⊗[R] A)) (s ⊗ₜ[R] a) = (algebraMap S (S ⊗[R] A)) s • (D S (S ⊗[R] A)) ((algebraMap A (S ⊗[R] A)) a)

Tactic:
Algebra.TensorProduct.right_algebraMap_apply,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (S ⊗[R] A)) (s ⊗ₜ[R] a) = (algebraMap S (S ⊗[R] A)) s • (D S (S ⊗[R] A)) (1 ⊗ₜ[R] a)
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
⊢ map I (g ∘ₗ f) = 0

Tactic:
hfg.linearMap_comp_eq_zero,

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 0 = 0
Module: Mathlib.RingTheory.Smooth.AdicCompletion

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FormallySmooth R A
I : Ideal S
inst✝ : IsAdicComplete I S
f : A →ₐ[R] S ⧸ I
g : A →ₐ[R] AdicCompletion I S
hg : (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)).comp g = f
x : A
⊢ ((Ideal.Quotient.mkₐ R I).comp ((AlgHom.restrictScalars R ↑(AdicCompletion.ofAlgEquiv I).symm).comp g)) x = f x

Tactic:
simpa using congr($hg x)

Goal state after:
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
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
x : MvPolynomial ι R₀
⊢ (P.tensorModelOfHasCoeffsInv R₀) ((MvPolynomial.aeval P.val) ((MvPolynomial.map (algebraMap R₀ R)) x)) =
    1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) x

Tactic:
← Generators.algebraMap_apply,

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
x : MvPolynomial ι R₀
⊢ (P.tensorModelOfHasCoeffsInv R₀) ((algebraMap P.Ring S) ((MvPolynomial.map (algebraMap R₀ R)) x)) =
    1 ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (relationOfHasCoeffs R₀)))) x
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 ι σ
r x✝ : σ
⊢ P.cotangentEquiv (Cotangent.mk ⟨P.relation r, ⋯⟩) x✝ =
    P.cotangentEquiv ((P.basisDeriv.map P.cotangentEquiv.symm) r) x✝

Tactic:
Basis.map_apply,

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
r x✝ : σ
⊢ P.cotangentEquiv (Cotangent.mk ⟨P.relation r, ⋯⟩) x✝ = P.cotangentEquiv (P.cotangentEquiv.symm (P.basisDeriv r)) x✝
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 ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ (Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ⊔
        Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}) ^
      2 ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
sq,

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 ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ (Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ⊔
        Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}) *
      (Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ⊔
        Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}) ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)