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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : CircleIntegrable f c R
⊢ IntervalIntegrable (fun θ ↦ deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
simp only [CircleIntegrable, deriv_circleMap, intervalIntegrable_iff] at *
  refine (hf.norm.const_mul |R|).mono' ?_ ?_
  · exact ((continuous_circleMap _ _).aestronglyMeasurable.mul_const I).smul hf.aestronglyMeasurable
  · simp [norm_smul]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Iio a).indicator f a_1‖ ≤ (Iio a₀).indicator (norm ∘ f) a_1

Tactic:
refine ae_of_all _ fun x ↦ ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
x : ℝ
⊢ ‖(Iio a).indicator f x‖ ≤ (Iio a₀).indicator (norm ∘ f) x
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun n ↦ (Iio n).indicator f a) (𝓝[≤] a₀) (𝓝 ((Iio a₀).indicator f a))

Tactic:
refine ae_of_all _ fun x ↦ ?_

Goal state after:
case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
⊢ Tendsto (fun n ↦ (Iio n).indicator f x) (𝓝[≤] a₀) (𝓝 ((Iio a₀).indicator f x))
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
x : α
⊢ ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖

Tactic:
filter_upwards with y using norm_nonneg _

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2

Tactic:
· have : ContinuousWithinAt (fun δ : ℝ => (2 * δ) ^ (n + 1) * ‖f' x (Pi.single i 1)‖)
            (Ioi 0) 0 := ((continuousWithinAt_id.const_mul _).pow _).mul_const _
        refine this.eventually (ge_mem_nhds ?_)
        simpa using half_pos ε0

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ Tendsto (fun i ↦ ∫⁻ (x : α), ∫⁻ (y : β), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂ν ∂μ) (𝓝 g) (𝓝 0)

Tactic:
have (i : α × β →₁[μ.prod ν] E) : Measurable fun z => ‖i z - g z‖ₑ :=
    ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ ∫⁻ (x : α), ∫⁻ (y : β), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂ν ∂μ) (𝓝 g) (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ ∫⁻ (z : α × β), ‖↑↑i z - ↑↑g z‖ₑ ∂μ.prod ν) (𝓝 g) (𝓝 0)

Tactic:
← L1.ofReal_norm_sub_eq_lintegral,

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 0)
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
⊢ f x = g x

Tactic:
· have : Fact ((q.map (algebraMap F (p * q).SplittingField)).Splits) :=
      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
        ((map_dvd_map' _).mpr (dvd_mul_left q p))⟩
    have key :
      x =
        algebraMap q.SplittingField (p * q).SplittingField
          ((rootsEquivRoots q _).invFun
            ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
      Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots q _) ⟨x, _⟩).symm
    rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
    exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.2 _)

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 : ℕ
⊢ (esymm σ R n).IsSymmetric

Tactic:
intro
  rw [rename_esymm]

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
fa : AnalyticAt ℂ f c
⊢ ∀ (a : ℂ), AnalyticAt ℂ f a → DifferentiableAt ℂ f a

Tactic:
apply AnalyticAt.differentiableAt

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

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ B ^ (Multiset.map (⇑↑nnnormHom) s).card = B ^ ((map f p).natDegree - i)

Tactic:
by rw [card_map, hs.2]

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
ψ : K →+* ℂ
inst✝ : Algebra K L
φ : ComplexEmbedding.Extension L ψ
h : ¬IsReal ψ
⊢ (conjugate ↑φ).comp (algebraMap K L) ≠ ψ

Tactic:
simp_all [ComplexEmbedding.isReal_iff, comp_eq]

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
x y : (ofClass v).ValueGroup₀
⊢ x < y → (valueGroup₀_equiv_withZeroMulInt v) x < (valueGroup₀_equiv_withZeroMulInt v) y

Tactic:
hxy

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
x y : (ofClass v).ValueGroup₀
hxy : x < y
⊢ (valueGroup₀_equiv_withZeroMulInt v) x < (valueGroup₀_equiv_withZeroMulInt v) y
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this : ∀ (x y : X) (r s : ℝ), r ≤ s → ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : s < r
⊢ (ball y s ⊆ ball x r ∨ ball x r ⊆ ball y s) ∨ Disjoint (ball y s) (ball x r)

Tactic:
or_assoc

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this : ∀ (x y : X) (r s : ℝ), r ≤ s → ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s)
hrs : s < r
⊢ ball y s ⊆ ball x r ∨ ball x r ⊆ ball y s ∨ Disjoint (ball y s) (ball x r)
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this :
  ∀ (x y : X) (r s : ℝ),
    r ≤ s →
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : s < r
⊢ (closedBall y s ⊆ closedBall x r ∨ closedBall x r ⊆ closedBall y s) ∨ Disjoint (closedBall y s) (closedBall x r)

Tactic:
or_assoc

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
this :
  ∀ (x y : X) (r s : ℝ),
    r ≤ s →
      closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)
hrs : s < r
⊢ closedBall y s ⊆ closedBall x r ∨ closedBall x r ⊆ closedBall y s ∨ Disjoint (closedBall y s) (closedBall x r)
Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ : R⟦X⟧
⊢ φ ∈ Ideal.span {X} ↔ constantCoeff φ = 0

Tactic:
Ideal.mem_span_singleton,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ : R⟦X⟧
⊢ X ∣ φ ↔ constantCoeff φ = 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case right
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : f ∉ Ideal.span {X}
hfI : f ∈ I
⊢ 1 ∈ I

Tactic:
Ideal.mem_span_singleton,

Goal state after:
case right
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬X ∣ f
hfI : f ∈ I
⊢ 1 ∈ I
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬constantCoeff f = 0
hfI : f ∈ I
this : C (f 0) = f - (f - C (f 0))
⊢ f - (f - C (f 0)) ∈ I

Tactic:
apply Ideal.sub_mem I hfI

Goal state after:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬constantCoeff f = 0
hfI : f ∈ I
this : C (f 0) = f - (f - C (f 0))
⊢ f - C (f 0) ∈ I
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬constantCoeff f = 0
hfI : f ∈ I
this : C (f 0) = f - (f - C (f 0))
⊢ f - C (f 0) ∈ Ideal.span {X}

Tactic:
Ideal.mem_span_singleton,

Goal state after:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬constantCoeff f = 0
hfI : f ∈ I
this : C (f 0) = f - (f - C (f 0))
⊢ X ∣ f - C (f 0)
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
x✝ : k⟦X⟧
⊢ constantCoeff x✝ = 0 ↔ x✝ ∈ Ideal.span {X}

Tactic:
Ideal.mem_span_singleton,

Goal state after:
k : Type u_2
inst✝ : Field k
x✝ : k⟦X⟧
⊢ constantCoeff x✝ = 0 ↔ X ∣ x✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ (ofJ j).IsElliptic

Tactic:
have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h2 : 2 ≠ 0
⊢ (ofJ j).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ (ofJ j).j = j

Tactic:
have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)

Goal state after:
case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
h2 : 2 ≠ 0
⊢ (ofJ j).j = j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] =
    ![P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] x,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]

Tactic:
mul_div_cancel₀ _ hPz,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] =
    ![P x, P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] = ![P x, P z * ![P x / P z, W.negY P / P z, 1] y, P z * ![P x / P z, W.negY P / P z, 1] z]

Tactic:
mul_div_cancel₀ _ hPz,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] = ![P x, W.negY P, P z * ![P x / P z, W.negY P / P z, 1] z]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomial / P z ^ 3 +
        (P y ^ 2 / P z ^ 2 * 1 + W.a₁ * P x * P y / P z ^ 2 * 1 + W.a₃ * P y / P z * 1 +
              W.a₂ * P x ^ 2 / P z ^ 2 * (P z / P z) +
            W.a₄ * P x / P z * (P z ^ 2 / P z ^ 2) +
          W.a₆ * (P z ^ 3 / P z ^ 3)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial +
        (P y ^ 2 / P z ^ 2 * (P z / P z) + W.a₁ * P x * P y / P z ^ 2 * (P z / P z) +
                W.a₃ * P y / P z * (P z ^ 2 / P z ^ 2) +
              W.a₂ * P x ^ 2 / P z ^ 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0

Tactic:
rw [eval_polynomial, Affine.evalEval_polynomial]

Goal state after:
case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (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)) /
          P z ^ 3 +
        (P y ^ 2 / P z ^ 2 * 1 + W.a₁ * P x * P y / P z ^ 2 * 1 + W.a₃ * P y / P z * 1 +
              W.a₂ * P x ^ 2 / P z ^ 2 * (P z / P z) +
            W.a₄ * P x / P z * (P z ^ 2 / P z ^ 2) +
          W.a₆ * (P z ^ 3 / P z ^ 3)) -
      ((P y / P z) ^ 2 + W.toAffine.a₁ * (P x / P z) * (P y / P z) + W.toAffine.a₃ * (P y / P z) -
          ((P x / P z) ^ 3 + W.toAffine.a₂ * (P x / P z) ^ 2 + W.toAffine.a₄ * (P x / P z) + W.toAffine.a₆) +
        (P y ^ 2 / P z ^ 2 * (P z / P z) + W.a₁ * P x * P y / P z ^ 2 * (P z / P z) +
                W.a₃ * P y / P z * (P z ^ 2 / P z ^ 2) +
              W.a₂ * P x ^ 2 / P z ^ 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
s : Set ↑(uliftFunctor.mapCocone c).pt
a✝ : J✝
⊢ IsOpen (⇑(ConcreteCategory.hom (c.ι.app a✝)) ⁻¹' ⇑Homeomorph.ulift.symm ⁻¹' s) ↔ IsOpen s

Tactic:
Homeomorph.ulift.isOpenEmbedding.isOpen_iff_preimage_isOpen (by simp)

Goal state after:
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cocone K
hc : IsColimit c
s : Set ↑(uliftFunctor.mapCocone c).pt
a✝ : J✝
⊢ IsOpen (⇑Homeomorph.ulift ⁻¹' ⇑(ConcreteCategory.hom (c.ι.app a✝)) ⁻¹' ⇑Homeomorph.ulift.symm ⁻¹' s) ↔ IsOpen s
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: case g.map_mul
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✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ ∀ (x y : A i),
    ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
        (x * y) =
      ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
          x *
        ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
          y

Tactic:
intro x y
      change Ideal.Quotient.mk _ _ = Ideal.Quotient.mk _ _ * Ideal.Quotient.mk _ _
      simp +instances only [AlgHom.toRingHom_eq_coe, LinearMap.coe_single, Pi.single_mul, map_mul]

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

Goal state before:
pp: case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
⊢ 1 - f₂ (Pi.single x 1) ∈ J'

Tactic:
Ideal.mem_span_singleton,

Goal state after:
case map_one
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
⊢ 1 - f₁ e ∣ 1 - f₂ (Pi.single x 1)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.zero
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x : B
⊢ x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) 0) = x • (D S B) 0

Tactic:
simp only [map_zero, smul_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Flat R S
inst✝⁴ : FinitePresentation R S
p : Ideal R
q : Ideal S
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := ⋯
Sp : Type u_2 := ⋯
Sq : Type u_2 := ⋯
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
f : Sp →ₐ[S] Sq := ⋯
algInst✝ : Algebra Sp Sq := ⋯
this : IsScalarTower R Sp Sq
⊢ (algebraMap Rp Sq).comp (algebraMap R Rp) = ((algebraMap Sp Sq).comp (algebraMap Rp Sp)).comp (algebraMap R Rp)

Tactic:
simp only [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ↑((sum I M) ((sumInv I M) ((mk I (⨁ (j : ι), M j)) f))) n = Submodule.Quotient.mk (↑f n)

Tactic:
← DirectSum.sum_univ_of (((sumInv I M) ((AdicCompletion.mk I (⨁ (j : ι), M j)) f)))

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : AdicCauchySequence I (⨁ (j : ι), M j)
n : ℕ
⊢ ↑((sum I M) (∑ i, (DirectSum.of (fun i ↦ AdicCompletion I (M i)) i) (((sumInv I M) ((mk I (⨁ (j : ι), M j)) f)) i)))
      n =
    Submodule.Quotient.mk (↑f n)
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ I ^ n • ⊤
y2 : N
hy2 : y2 ∈ I ^ n • ⊤
x1 : M
hx1 : x1 ∈ I ^ n • ⊤
hx1' : f x1 ≡ y1 [SMOD I ^ (n + 1) • ⊤]
x2 : M
hx2 : x2 ∈ I ^ n • ⊤
hx2' : f x2 ≡ y2 [SMOD I ^ (n + 1) • ⊤]
⊢ ∃ x ∈ I ^ n • ⊤, f x ≡ y1 + y2 [SMOD I ^ (n + 1) • ⊤]

Tactic:
use x1 + x2, add_mem hx1 hx2

Goal state after:
case right
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : N
n : ℕ
y1 : N
hy1 : y1 ∈ I ^ n • ⊤
y2 : N
hy2 : y2 ∈ I ^ n • ⊤
x1 : M
hx1 : x1 ∈ I ^ n • ⊤
hx1' : f x1 ≡ y1 [SMOD I ^ (n + 1) • ⊤]
x2 : M
hx2 : x2 ∈ I ^ n • ⊤
hx2' : f x2 ≡ y2 [SMOD I ^ (n + 1) • ⊤]
⊢ f (x1 + x2) ≡ y1 + y2 [SMOD I ^ (n + 1) • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ (I ^ n • ⊤).mkQ (f x) = y

Tactic:
hxy

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ y = y