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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ = ∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ

Tactic:
apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    have : ∀ y, f x y = 0 := by
      intro y
      contrapose! hx
      have : (x, y) ∈ Function.support f.uncurry := hx
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x✝² x✝¹ : p.Gal
x✝ : ↑(p.rootSet p.SplittingField)
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
p q : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x✝ : ↑(p.rootSet p.SplittingField)
⊢ 1 • x✝ = x✝

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ ∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, (monomial (Finsupp.single i 1)) 1

Tactic:
← X_pow_eq_monomial,

Goal state after:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ ∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i = ∑ x ∈ powersetCard n univ, ∏ x ∈ x, X x ^ 1
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
h0 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), f z = 0

Tactic:
wlog hE : CompleteSpace E generalizing
  · simp [circleIntegral, intervalIntegral, integral, hE]
  rcases h0.eq_or_lt with (rfl | h0); · apply circleIntegral.integral_radius_zero
  calc
    (∮ z in C(c, R), f z) = ∮ z in C(c, R), (z - c)⁻¹ • (z - c) • f z :=
      (circleIntegral.integral_sub_inv_smul_sub_smul _ _ _ _).symm
    _ = (2 * ↑π * I : ℂ) • (c - c) • f c :=
      (circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable h0 hs
        ((continuousOn_id.sub continuousOn_const).smul hc) fun z hz =>
        (differentiableAt_id.sub_const _).smul (hd z hz))
    _ = 0 := by rw [sub_self, zero_smul, smul_zero]

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : ∮ (z : ℂ) in C(c, R), F z = 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun z ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z ↦ (z - w)⁻¹) (sphere c R)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) • f w

Tactic:
← circleIntegral.integral_smul_const,

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : ∮ (z : ℂ) in C(c, R), F z = 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun z ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z ↦ (z - w)⁻¹) (sphere c R)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f w
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c ↑R
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ x ∈ ball c ↑R \ s, DifferentiableAt ℂ f x
hR : 0 < ↑R
this✝ : w ∈ closure (ball c ↑R \ s)
this :
  HasFPowerSeriesOnBall (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) (cauchyPowerSeries f c ↑R) c
    ↑R
⊢ ContinuousAt (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) w

Tactic:
refine this.continuousOn.continuousAt (Metric.isOpen_eball.mem_nhds ?_)

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c ↑R
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ x ∈ ball c ↑R \ s, DifferentiableAt ℂ f x
hR : 0 < ↑R
this✝ : w ∈ closure (ball c ↑R \ s)
this :
  HasFPowerSeriesOnBall (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) (cauchyPowerSeries f c ↑R) c
    ↑R
⊢ w ∈ eball c ↑R
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr.inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
y : X
hy : y ∈ closedBall x r
hd : Disjoint (closedBall x r) (closedBall y r)
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ closedBall x r

Tactic:
simp [closedBall_eq_of_mem hy, h.not_gt] at hd

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: S : Type u_1
S' : Type u_2
ι : Type u_3
inst✝² : SeminormedGroup S
inst✝¹ : SeminormedGroup S'
inst✝ : IsUltrametricDist S
r : ℝ
hr : 0 < r
⊢ ∀ {x : S}, x ∈ ball 1 r → x⁻¹ ∈ ball 1 r

Tactic:
by simp only [Metric.mem_ball, dist_one_right, norm_inv', imp_self, implies_true]

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
hφ : ∃ a, ↑a = φ.lexOrder
⊢ ∃ d, φ.lexOrder = ↑(toLex d)

Tactic:
obtain ⟨p, hp⟩ := hφ

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
p : Lex (σ →₀ ℕ)
hp : ↑p = φ.lexOrder
⊢ ∃ d, φ.lexOrder = ↑(toLex d)
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
u v : σ →₀ ℕ
h' : (u, v) ≠ (p, q)
h : u + v = p + q
h'' : u = p ∧ v = q
⊢ (coeff (u, v).1) φ * (coeff (u, v).2) ψ = 0

Tactic:
exact False.elim (h' (by simp [h''.1, h''.2]))

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

Goal state before:
pp: case h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsLeft R
x : MvPowerSeries σ R
hx : φ * x = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
⊢ (0, e) ∉ antidiagonal e → (coeff (0, e).1) φ * (coeff (0, e).2) x = 0

Tactic:
simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff (single () n)) (MvPowerSeries.inv.aux a φ) =
    if n = 0 then a
    else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (MvPowerSeries.inv.aux a φ) else 0

Tactic:
MvPowerSeries.coeff_inv_aux

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
⊢ (if single () n = 0 then a
    else
      -a *
        ∑ x ∈ antidiagonal (single () n),
          if x.2 < single () n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (MvPowerSeries.inv.aux a φ)
          else 0) =
    if n = 0 then a
    else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (MvPowerSeries.inv.aux a φ) else 0
Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer

Goal state before:
pp: J : MulticospanShape
I : MulticospanIndex J (Type u)
s : ↑I.multicospan.sections
⊢ (fun s ↦
        ⟨fun i ↦
          match i with
          | WalkingMulticospan.left i => s.val i
          | WalkingMulticospan.right j => (ConcreteCategory.hom (I.fst j)) (s.val (J.fst j)),
          ⋯⟩)
      ((fun s ↦ { val := fun i ↦ ↑s (WalkingMulticospan.left i), property := ⋯ }) s) =
    s

Tactic:
ext (_ | r)
    · rfl
    · exact s.property (.fst r)

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : PointClass F
hP : W.NonsingularLift P
⊢ W.NonsingularLift (W.negMap P)

Tactic:
rcases P with ⟨_⟩
  exact nonsingular_neg hP

Goal state after:
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.Equation P
hQ : W.Equation 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)
hx : ¬P x * Q z = Q x * P z
⊢ W.addMap ⟦P⟧ ⟦Q⟧ =
    ⟦![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]⟧

Tactic:
rw [addMap_eq, add_of_X_ne hP hQ hPz hQz hx, smul_eq _ <| isUnit_addZ_of_X_ne hP hQ hx]

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

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
⊢ FormallyEtale R ((i : I) → A i) ↔ ∀ (i : I), FormallyEtale R (A i)

Tactic:
simp_rw [FormallyEtale.iff_formallyUnramified_and_formallySmooth, forall_and]
  rw [FormallyUnramified.pi_iff A, FormallySmooth.pi_iff A]

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - W'.negY P) * Q z + -W'.a₁ * (P x * Q z)) =
    0

Tactic:
rw [negY, negY]

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) * Q z + -W'.a₁ * (P x * Q z)) =
    0
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
⊢ FormallySmooth R S

Tactic:
let M' := M.comap f₀

Goal state after:
R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
⊢ FormallySmooth R S
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 s : AdicCompletion I R
x : AdicCompletion I M
⊢ (r * s) • x = r • s • x

Tactic:
by
    ext n
    simp only [smul_eval, val_mul, mul_smul]

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

Goal state before:
pp: case base
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
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m n : ℕ
⊢ (Ideal.Quotient.factorₐ R ⋯).comp (liftAdicCompletionAux I f m) = liftAdicCompletionAux I f m

Tactic:
| base =>

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

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
⊢ Set.SurjOn (⇑(p.projectionOnto q hpq)) (Set.range ⇑f) Set.univ

Tactic:
rw [← LinearMap.coe_range, ← Submodule.top_coe (R := R), surjOn_iff_le_map,
    ← hfg.linearMap_ker_eq]

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
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
⊢ ⊤ ≤ map (p.projectionOnto q hpq) g.ker
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : P.Ring
y : D.T
z : S
⊢ (x • y) • z = x • y • z

Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : P.Ring
z : S
y : MvPolynomial ι R
⊢ (x • (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) y) • z =
    x • (Ideal.Quotient.mk (Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))) y • z
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: 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
⊢ D.presLeft.ker ≤ P.ker

Tactic:
intro x hx
  simpa only [toExtension_commRing, toExtension_Ring, RingHom.mem_ker,
    toExtension_algebra₂, algebraMap_apply, Ideal.Quotient.algebraMap_eq,
    map_zero] using! (algebraMap D.T S).congr_arg hx

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
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
p :
  Fin (Presentation.ofFinitePresentationRels A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
homog : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (p j).IsHomogeneous 2
hp : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (eval P.relation) (p j) = (aeval h) (P.relation j)
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
have hsig (i : _) : f (h i) = P.val i := by
    rw [← AlgHom.kerSquareLift_mk]
    -- Reducible def-eq issues caused by `RingHom.ker f.toRingHom` discrepancies
    -- Can be fixed after #25138.
    exact hh i ▸ congr($hsig (P.val i))

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
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig✝ : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
p :
  Fin (Presentation.ofFinitePresentationRels A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
homog : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (p j).IsHomogeneous 2
hp : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (eval P.relation) (p j) = (aeval h) (P.relation j)
hsig : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), f (h i) = P.val i
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

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

Tactic:
rw [eq_smoothOfRelativeDimension_zero]

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
X Y : Scheme
inst✝ : P.RespectsIso
f : X ⟶ Y
x✝ : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P ((Scheme.Hom.opensRange (𝒰.f (𝒰.idx x))).ι ≫ f)

Tactic:
rw [← Scheme.Hom.isoOpensRange_inv_comp, Category.assoc, P.cancel_left_of_respectsIso]

Goal state after:
case refine_1
P : MorphismProperty Scheme
X Y : Scheme
inst✝ : P.RespectsIso
f : X ⟶ Y
x✝ : sourceLocalClosure IsOpenImmersion P f
x : ↥X
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P (𝒰.f (𝒰.idx x) ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
⊢ P f

Tactic:
obtain ⟨𝒰, h⟩ := eq_sourceLocalClosure_isOpenImmersion ▸ hf

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ P f
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case inr.refine_1
P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X Y✝ : Scheme
f : X ⟶ Spec R
g : Y✝ ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (pullback.fst f g)
this : ∀ {X : Scheme} (f : X ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → (∃ T, X = Spec T) → P g
hX : ¬∃ T, X = Spec T
x✝ : CompactSpace ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ (P' ⊓ @QuasiCompact) (Y.isoSpec.inv ≫ p ≫ f)

Tactic:
(P' ⊓ @QuasiCompact).cancel_left_of_respectsIso

Goal state after:
case inr.refine_1
P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X Y✝ : Scheme
f : X ⟶ Spec R
g : Y✝ ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (pullback.fst f g)
this : ∀ {X : Scheme} (f : X ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → (∃ T, X = Spec T) → P g
hX : ¬∃ T, X = Spec T
x✝ : CompactSpace ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ (P' ⊓ @QuasiCompact) (p ≫ f)
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
z : S
hz : z ∈ R[x]
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
this : z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) ↔ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I
⊢ z ∈ Ideal.map (algebraMap R S) I

Tactic:
Ideal.mem_comap

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
z : S
hz : z ∈ R[x]
hy : (algebraMap (↥R[x]) S) ⟨z, hz⟩ ∈ Ideal.map (algebraMap R S) I
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
this : z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) ↔ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I
⊢ z ∈ Ideal.map (algebraMap R S) I
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_4
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
p : A[X]
monic : p.Monic
deg : p.natDegree ≠ 0
hx : IsIntegral R (eval x p)
hp : ∀ (i : ℕ), IsIntegral R (p.coeff i)
q : (↥(integralClosure R A))[X]
hqp : Polynomial.map (algebraMap (↥(integralClosure R A)) A) q = p
hdeg : q.natDegree = p.natDegree
hq : q.Monic
⊢ IsIntegral (↥(integralClosure R A)) ((aeval x) q)

Tactic:
simpa [← eval_map_algebraMap, hqp] using hx.tower_top

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

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
H : ∀ (x : ↥(Spec R)), IsDiscrete (⇑(Spec.map φ) ⁻¹' {x})
inst✝ : (CommRingCat.Hom.hom φ).FiniteType
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
⊢ (CommRingCat.Hom.hom φ).QuasiFinite

Tactic:
exact (Algebra.QuasiFinite.iff_finite_comap_preimage_singleton).mpr fun x ↦
    ((Spec.map φ).isCompact_preimage_singleton _).finite (H _)

Goal state after: