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

Goal state before:
pp: case hF.refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
i : ι
hi : ContinuousOn (f i) (sphere c R)
⊢ MapsTo (circleMap c R) [[0, 2 * π]] (sphere c R)

Tactic:
simp [hR, MapsTo]

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 ⋯
⊢ ∀ (J : Box (Fin (n + 1))), 0 ≤ (volume.toBoxAdditive.restrict ↑I ⋯) J

Tactic:
exact fun J => ENNReal.toReal_nonneg

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

Goal state before:
pp: case refine_3
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
this :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ Box.Icc J
x✝ : GP.bDistortion = true → J.distortion ≤ c
⊢ dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤ ε / 2 + ε / 2

Tactic:
have Hl : J.lower i ∈ Icc (J.lower i) (J.upper i) := Set.left_mem_Icc.2 (J.lower_le_upper i)

Goal state after:
case refine_3
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
this :
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    δ ∈ Set.Ioc 0 (1 / 2) ∧
      (∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
        (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
δ : ℝ
hδ0 : 0 < δ
hδ12 : δ ≤ 1 / 2
hdfδ : ∀ y₁ ∈ closedBall x δ ∩ Box.Icc I, ∀ y₂ ∈ closedBall x δ ∩ Box.Icc I, ‖f y₁ - f y₂‖ ≤ ε / 2
hδ : (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖ ≤ ε / 2
J : Box (Fin (n + 1))
hJI : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
x✝¹ : x ∈ Box.Icc J
x✝ : GP.bDistortion = true → J.distortion ≤ c
Hl : J.lower i ∈ Set.Icc (J.lower i) (J.upper i)
⊢ dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤ ε / 2 + ε / 2
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 μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᵐ[μ.prod ν] g
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
x : α
⊢ (∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)) → ∫ (y : β), g (x, y) ∂ν = ∫ (y : β), f (x, y) ∂ν

Tactic:
hfgx

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 μ
hE : CompleteSpace E
f g : α × β → E
hfg : f =ᵐ[μ.prod ν] g
hf : ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
x : α
hfgx : ∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)
⊢ ∫ (y : β), g (x, y) ∂ν = ∫ (y : β), f (x, y) ∂ν
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p ↦ f' (e p) ∘SL ↑e
x y : ℝ
⊢ (-(I • F' (x, y))) (1, 0) + (F' (x, y)) (0, 1) = -(I • (f' (e (x, y))) 1 - (f' (e (x, y))) I)

Tactic:
simp only [F', neg_apply, smul_apply, ContinuousLinearMap.comp_apply,
      ContinuousLinearEquiv.coe_coe, he₁, he₂, neg_add_eq_sub, neg_sub]

Goal state after:
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
hy : y ∉ V
⊢ f x y = 0

Tactic:
contrapose! hy

Goal state after:
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
hy : f x y ≠ 0
⊢ y ∈ V
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 < ∞)
y : Y
hy : y ∉ V
x : X
⊢ f x y = 0

Tactic:
contrapose! hy

Goal state after:
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 < ∞)
y : Y
x : X
hy : f x y ≠ 0
⊢ y ∈ V
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
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)
⊢ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = f w

Tactic:
by
    lift R to ℝ≥0 using hR.le
    have A : ContinuousAt (fun w => (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) w := by
      have := hasFPowerSeriesOn_cauchy_integral
        ((hc.mono sphere_subset_closedBall).circleIntegrable R.coe_nonneg) hR
      refine this.continuousOn.continuousAt (Metric.isOpen_eball.mem_nhds ?_)
      rwa [Metric.eball_coe]
    have B : ContinuousAt f w := hc.continuousAt (closedBall_mem_nhds_of_mem hw)
    refine tendsto_nhds_unique_of_frequently_eq A B ((mem_closure_iff_frequently.1 this).mono ?_)
    intro z hz
    rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux hs hz hc hd,
      inv_smul_smul₀]
    simp [Real.pi_ne_zero, I_ne_zero]

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

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ + C a) + -f a)) l atTop

Tactic:
simpa using ihp hf

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

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

Tactic:
apply (coeff_le_of_roots_le i h1 h2 h4).trans

Goal state after:
case inl
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i) ≤ max B 1 ^ d * ↑(d.choose (d / 2))
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case H
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ IsCoprime (X - C ((starRingEnd ℂ) z)) (X - C z)

pp: case H1
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X - C ((starRingEnd ℂ) z) ∣ map (algebraMap ℝ ℂ) p

pp: case H2
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X - C z ∣ map (algebraMap ℝ ℂ) p

Tactic:
· exact isCoprime_X_sub_C_of_isUnit_sub <| .mk0 _ <| sub_ne_zero.2 <| mt conj_eq_iff_im.1 hz

Goal state after:
case H1
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X - C ((starRingEnd ℂ) z) ∣ map (algebraMap ℝ ℂ) p

case H2
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X - C z ∣ map (algebraMap ℝ ℂ) p
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: 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
⊢ embedRealFun (x + y) = embedRealFun x + embedRealFun y

Tactic:
rw [embedRealFun, ratLt'_add, csSup_add (ratLt'_nonempty x) (ratLt'_bddAbove x)
    (ratLt'_nonempty y) (ratLt'_bddAbove y)]

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
x y z : L
⊢ v.norm (x - y + (y - z)) ≤ v.norm (x - y) + v.norm (y - z)

Tactic:
exact le_trans (val.v.norm_add_le _ _)
        (max_le_add_of_nonneg (val.v.norm_nonneg _) (val.v.norm_nonneg _))

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
i : σ
⊢ (monomial (single i 1)) 1 ∈ (MvPowerSeries σ R)⁰

Tactic:
monomial_mem_nonzeroDivisors

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
i : σ
⊢ 1 ∈ R⁰
Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Prime X

Tactic:
← Ideal.span_singleton_prime

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (Ideal.span {X}).IsPrime

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X ≠ 0
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case h₂
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ IsOpenImmersion.precoverage ≤ Precoverage.comap forgetToTop TopCat.isOpenEmbedding.precoverage

Tactic:
rw [MorphismProperty.comap_precoverage]

Goal state after:
case h₂
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ IsOpenImmersion.precoverage ≤ (TopCat.isOpenEmbedding.inverseImage forgetToTop).precoverage
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: ⊢ ∀ {R S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified

Tactic:
intro R S _ _ e

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ e.toRingHom.FormallyUnramified
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: ⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ Smooth

Tactic:
introv R hs hf
  have : f.FinitePresentation :=
    finitePresentation_ofLocalizationSpanTarget _ s hs fun r ↦ (hf r).finitePresentation
  algebraize [f]
  refine ⟨?_, ‹_›⟩
  rw [← Algebra.smoothLocus_eq_univ_iff, ← Set.univ_subset_iff, ← TopologicalSpace.Opens.coe_top,
    ← PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs]
  simp only [TopologicalSpace.Opens.coe_iSup, Set.iUnion_subset_iff,
    Algebra.basicOpen_subset_smoothLocus_iff, ← formallySmooth_algebraMap]
  exact fun r hr ↦ (hf ⟨r, hr⟩).1

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

Goal state before:
pp: K : Type u_1
L : Type u_2
A : Type u
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K L
inst✝³ : Algebra K A
inst✝² : EssFiniteType K A
inst✝¹ : FormallyEtale K A
p : Ideal A
inst✝ : p.IsPrime
this : Module.Finite K A
⊢ Algebra.IsSeparable K (A ⧸ p)

Tactic:
have : IsArtinianRing A := isArtinian_of_tower K inferInstance

Goal state after:
K : Type u_1
L : Type u_2
A : Type u
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K L
inst✝³ : Algebra K A
inst✝² : EssFiniteType K A
inst✝¹ : FormallyEtale K A
p : Ideal A
inst✝ : p.IsPrime
this✝ : Module.Finite K A
this : IsArtinianRing A
⊢ Algebra.IsSeparable K (A ⧸ p)
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case mp
K : Type u_1
A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this✝ : Module.Finite K A
this : IsReduced A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
have : IsArtinianRing A := isArtinian_of_tower K inferInstance

Goal state after:
case mp
K : Type u_1
A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
H : FormallyEtale K A
this✝¹ : Module.Finite K A
this✝ : IsReduced A
this : IsArtinianRing A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case add
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 y : B ⊗[S] B
e₁ :
  (LinearMap.liftBaseChange S (↑R (map R S A B)))
      ((derivationTensorProduct R S A B).liftKaehlerDifferential ((D S B).tensorProductTo x)) =
    (D S B).tensorProductTo x
e₂ :
  (LinearMap.liftBaseChange S (↑R (map R S A B)))
      ((derivationTensorProduct R S A B).liftKaehlerDifferential ((D S B).tensorProductTo y)) =
    (D S B).tensorProductTo y
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B)))
      ((derivationTensorProduct R S A B).liftKaehlerDifferential ((D S B).tensorProductTo (x + y))) =
    (D S B).tensorProductTo (x + y)

Tactic:
simp only [map_add, e₁, e₂]

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
⊢ (tensorKaehlerEquiv R S A (A ⊗[R] S)).symm ((D S (A ⊗[R] S)) (a ⊗ₜ[R] s)) =
    (algebraMap S (A ⊗[R] S)) s ⊗ₜ[A] (D R A) a

Tactic:
apply (tensorKaehlerEquiv R S A _).symm_apply_eq.mpr ?_
  simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    tensorKaehlerEquiv_tmul_D]
  rw [algebraMap_smul, ← Derivation.map_smul, Algebra.smul_def,
    Algebra.TensorProduct.right_algebraMap_apply]
  simp only [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_one]

Goal state after:
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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
⊢ (lift I (fun n ↦ ↑R (reduceModIdeal (I ^ n) f) ∘ₗ eval I M n) ⋯).toFun (r • x) =
    (RingHom.id (AdicCompletion I R)) r • (lift I (fun n ↦ ↑R (reduceModIdeal (I ^ n) f) ∘ₗ eval I M n) ⋯).toFun x

Tactic:
ext
    dsimp
    rw [val_smul_eq_evalₐ_smul, val_smul_eq_evalₐ_smul, map_smul]

Goal state after:
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
⊢ ∃ x', x ≡ x' [SMOD I ^ n • ⊤] ∧ (I ^ (n + 1) • ⊤).mkQ (f x') = y'

Tactic:
obtain ⟨y0, hy0⟩ := mkQ_surjective _ y'

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'
⊢ ∃ x', x ≡ x' [SMOD I ^ n • ⊤] ∧ (I ^ (n + 1) • ⊤).mkQ (f x') = y'
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := ⋯
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p := ⋯
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := ⋯
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] := ⋯
i : κ
⊢ ((IsLocalizedModule.map p.primeCompl l₁ l₂) e) (l₁ (Finsupp.single i 1)) = (↑b.repr.symm ∘ₗ Finsupp.lsingle i) 1

Tactic:
· simp [l₂, e, hb]

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this : eₚ = ↑b.repr.symm
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
have heₚ : Function.Bijective eₚ := this ▸ b.repr.symm.bijective

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this : eₚ = ↑b.repr.symm
heₚ : Function.Bijective ⇑eₚ
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addZ P Q = 0

Tactic:
by
  apply eq_zero_of_ne_zero_of_mul_right_eq_zero <| mul_ne_zero hPz hQz
  rw [addZ_eq' hP hQ, hx, sub_self, zero_pow three_ne_zero]

Goal state after: