mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : LocallyCompactSpace G
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
i : HasFundamentalDomain (↥Γ.op) G ν
inst✝ : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
⊢ μ.IsHaarMeasure

Tactic:
rw [haarMeasure_unique μ K']

Goal state after:
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : LocallyCompactSpace G
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
i : HasFundamentalDomain (↥Γ.op) G ν
inst✝ : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
⊢ (μ ↑K' • haarMeasure K').IsHaarMeasure
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
⊢ k < n₁ + n₂ → IntervalIntegrable f volume (a k) (a (k + 1))

Tactic:
hk

Goal state after:
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ IntervalIntegrable f volume (a k) (a (k + 1))
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : SFinite ν
f : α × β → X
hf : AEStronglyMeasurable f (μ.prod ν)
⊢ ∀ᵐ (x : α) ∂μ, AEStronglyMeasurable (fun y ↦ f (x, y)) ν

Tactic:
by
  filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with x hx
  exact ⟨fun y ↦ hf.mk f (x, y),
    hf.stronglyMeasurable_mk.comp_measurable measurable_prodMk_left, hx⟩

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

Goal state before:
pp: case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ℕ), ‖f (circleMap c R t)‖ * (‖w‖ / R) ^ n) volume 0 (2 * π)

pp: case refine_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))

Tactic:
· simpa only [tsum_mul_left, tsum_geometric_of_lt_one hwR.1 hwR.2] using
      hf.norm.mul_continuousOn continuousOn_const

Goal state after:
case refine_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
hR : 0 < R
hwR : ‖w‖ / R ∈ Ico 0 1
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι 0 (2 * π) →
      HasSum (fun n ↦ deriv (circleMap c R) t • (fun z ↦ (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (circleMap c R t))
        (deriv (circleMap c R) t • (fun z ↦ (z - (c + w))⁻¹ • f z) (circleMap c R t))
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ ∀ (x : ℝ), f' x = ∑ i, (F' x) (e.symm (Pi.single i 1))

Tactic:
simp [F', e]

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
⊢ Fintype.card σ = univ.val.card

Tactic:
← Finset.card_univ,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
⊢ #univ = univ.val.card
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
⊢ Fintype.card σ = univ.val.card

Tactic:
← Finset.card_univ,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
⊢ #univ = univ.val.card
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case pos
p : ℚ[X]
hp : p = 0
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card

Tactic:
have : IsEmpty (p.rootSet ℂ) := by rw [hp, rootSet_zero]; infer_instance
    simp_rw [(galActionHom p ℂ _).support.eq_empty_of_isEmpty, hp, rootSet_zero,
      Set.toFinset_empty, Finset.card_empty]

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mpr
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
⊢ (∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a) → a ∈ ratLt (x + y)

Tactic:
· -- `u ∈ ratLt 1 x`, `v ∈ ratLt 1 y` → `u + v ∈ ratLt 1 (x + y)`
    intro ⟨u, hu, v, hv, huv⟩
    rw [← huv]
    rw [Set.mem_ofPred_eq] at hu hv ⊢
    exact num_smul_one_lt_den_smul_add hu hv

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

Goal state before:
pp: case h₀.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u ≤ e

Tactic:
simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsLeft R
⊢ φ ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)

Tactic:
classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e φ x).symm
  rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]
  · rintro ⟨_, u⟩ huv _
    suffices u < e by simp only [he u this, mul_zero, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]
    · rintro rfl
      simp_all
  · simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : Ideal (𝓞 K)
hI : I ≠ ⊥
⊢ ∏ᶠ (v : FinitePlace K), v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I = I

Tactic:
conv_rhs => rw [← finprod_heightOneSpectrum_pow_multiplicity hI]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : Ideal (𝓞 K)
hI : I ≠ ⊥
⊢ ∏ᶠ (v : FinitePlace K), v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I =
    ∏ᶠ (p : HeightOneSpectrum (𝓞 K)), p.asIdeal ^ multiplicity p.asIdeal I
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * ![P x / P z, P y / P z, 1] z + -P x * 1 - (![P x / P z, P y / P z, 1] x * P z + -P x * (P z / P z)) = 0

Tactic:
matrix_simp; ring1

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * ![P x / P z, P y / P z, 1] z + -P y * 1 - (![P x / P z, P y / P z, 1] y * P z + -P y * (P z / P z)) = 0

Tactic:
matrix_simp; 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
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
⊢ Presieve.IsSheafFor F S.arrows

Tactic:
intro t

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
⊢ t.Compatible → ∃! t_1, t.IsAmalgamation t_1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ 0 = toAffine W P

Tactic:
toAffine_of_Z_eq_zero hPz

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ 0 = 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
this :
  toAffine W
      ![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] =
    toAffine W P + toAffine W Q
hx : ¬P x * Q z = Q x * P z
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
rwa [add_of_X_ne hP.left hQ.left hPz hQz hx,
            toAffine_smul _ <| isUnit_addZ_of_X_ne hP.left hQ.left hx]

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

Goal state before:
pp: case pos
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Projective R
W : Projective F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (fromAffine (toAffine W P)).point =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.point

Tactic:
toAffine_of_Z_eq_zero hPz

Goal state after:
case pos
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Projective R
W : Projective F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (fromAffine 0).point = { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.point
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Free (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
        (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))
      have := this.extendScalarsOfIsLocalization
        p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
      exact ⟨fun H ↦ H.of_equiv' this.symm, fun H ↦ H.of_equiv' this⟩

Goal state after:
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
H : (algebraMap R T).FormallyUnramified
⊢ (algebraMap S (TensorProduct R S T)).FormallyUnramified

Tactic:
formallyUnramified_algebraMap

Goal state after:
R S T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
H : Algebra.FormallyUnramified R T
⊢ Algebra.FormallyUnramified S (TensorProduct R S T)
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ (algebraMap R S).FormallyUnramified

Tactic:
formallyUnramified_algebraMap

Goal state after:
R S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Algebra.FormallyUnramified R S
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔ (algebraMap R (Localization.Away r)).FormallyUnramified

Tactic:
formallyUnramified_algebraMap

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔ Algebra.FormallyUnramified R (Localization.Away r)
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: case ofLocalizationSpan
⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
exact ofLocalizationSpanTarget.ofLocalizationSpan
      (stableUnderComposition.stableUnderCompositionWithLocalizationAway
          holdsForLocalizationAway).1

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 σ
T : Type u_1
ι' : Type u_2
σ' : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : Finite σ'
Q : SubmersivePresentation S T ι' σ'
P : SubmersivePresentation R S ι σ
⊢ IsUnit (Q.comp P.toPreSubmersivePresentation).jacobian

Tactic:
comp_jacobian_eq_jacobian_smul_jacobian,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Finite σ
T : Type u_1
ι' : Type u_2
σ' : Type u_3
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : Finite σ'
Q : SubmersivePresentation S T ι' σ'
P : SubmersivePresentation R S ι σ
⊢ IsUnit (P.jacobian • Q.jacobian)
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
⊢ ((localizationAway T g).comp P).ker ^ 2 ≤ RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
comp_localizationAway_ker _ _ (P.σ g) (by simp),

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}) ^
      2 ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_1
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
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
⊢ ∃ p_1,
    p_1.IsHomogeneous 2 ∧
      (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p_1 =
        (aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i)

Tactic:
obtain ⟨q, hq⟩ := (D.p i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_p_subset R i)

Goal state after:
case refine_1
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
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) q = D.p i
⊢ ∃ p_1,
    p_1.IsHomogeneous 2 ∧
      (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p_1 =
        (aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i)
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
⊢ ∃ σ₀,
    (Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))).kerSquareLift.comp
        σ₀ =
      AlgHom.id (↥(subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(subalgebra R D))

Tactic:
choose p hp using fun i ↦ (D.h i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_h_subset R i)
  refine ⟨?_, ?_⟩
  · refine Ideal.Quotient.liftₐ _ ((Ideal.Quotient.mkₐ _ _).comp <| aeval p) ?_
    simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le, Set.range_subset_iff]
    intro i
    simp only [← AlgHom.comap_ker, Ideal.coe_comap, Set.mem_preimage, SetLike.mem_coe]
    rw [← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker,
      ← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker]
    have hinj : Function.Injective
        (MvPolynomial.map (σ := D.vars) (algebraMap (D.subalgebra R) A)) :=
      map_injective _ (FaithfulSMul.algebraMap_injective (D.subalgebra R) A)
    rw [Ideal.mem_span_pow_iff_exists_isHomogeneous]
    obtain ⟨q, hq⟩ := (D.p i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_p_subset R i)
    refine ⟨q, .of_map hinj ?_, hinj ?_⟩
    · rw [hq]
      exact D.hphom i
    · simp_rw [map_eval, Function.comp_def, Presentation.map_relationOfHasCoeffs,
        hq, D.hp, MvPolynomial.map_aeval, hp]
      simp [MvPolynomial.eval₂_map_comp_C, Presentation.map_relationOfHasCoeffs, aeval_def]
  · have hf₀ : Function.Surjective f₀ := Ideal.Quotient.mk_surjective
    rw [← AlgHom.cancel_right hf₀]
    refine MvPolynomial.algHom_ext fun i ↦ ?_
    suffices h : ∃ p', p'.IsHomogeneous 1 ∧ (eval (D.P.relationOfHasCoeffs (D.subalgebra R))) p' =
        p i - X i by
      -- Reducible def-eq issues caused by `RingHom.ker f.toRingHom` discrepancies
      -- Can be fixed after #25138.
      apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr
      simpa [Ideal.mem_span_iff_exists_isHomogeneous, hp]
    have hinj : Function.Injective
        (MvPolynomial.map (σ := D.vars) (algebraMap (D.subalgebra R) A)) :=
      map_injective _ (FaithfulSMul.algebraMap_injective (D.subalgebra R) A)
    obtain ⟨t, ht⟩ := (D.q i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_q_subset R i)
    refine ⟨t, .of_map hinj ?_, hinj ?_⟩
    · rw [ht]
      exact D.hqhom i
    · simp [MvPolynomial.map_eval, Function.comp_def,
        Presentation.map_relationOfHasCoeffs, ht, hq, hp]

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

Goal state before:
pp: X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
⊢ IsField ↑Γ(X, ⊤)

Tactic:
let F := (Scheme.ΓSpecIso _).inv ≫ f.appTop
  have : F.hom.IsIntegral := by
    apply RingHom.isIntegral_respectsIso.2 (e := (Scheme.ΓSpecIso _).symm.commRingCatIsoToRingEquiv)
    exact isIntegral_appTop_of_universallyClosed f
  algebraize [F.hom]
  exact isField_of_isIntegral_of_isField' (Field.toIsField K)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ Etale f ↔ SmoothOfRelativeDimension 0 f

Tactic:
eq_smoothOfRelativeDimension_zero

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ SmoothOfRelativeDimension 0 f ↔ SmoothOfRelativeDimension 0 f