mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ ∀ᵐ (a : α) ∂μ, ‖∫ (y : β), f (a, y) ∂ν‖ ≤ ‖∫ (y : β), ‖f (a, y)‖ ∂ν‖

Tactic:
filter_upwards with x

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
f : α × β → E
hf : Integrable f (μ.prod ν)
x : α
⊢ ‖∫ (y : β), f (x, y) ∂ν‖ ≤ ‖∫ (y : β), ‖f (x, y)‖ ∂ν‖
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε

Tactic:
calc
    ‖(∮ z in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ =
        ‖(∮ z in C(c, r), (z - c)⁻¹ • f z) - ∮ z in C(c, r), (z - c)⁻¹ • y‖ := by
      congr 2
      · exact circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable hr0
          hrR hs (hc.mono hsub) fun z hz => hd z ⟨hsub' hz.1, hz.2⟩
      · simp [hr0.ne']
    _ = ‖∮ z in C(c, r), (z - c)⁻¹ • (f z - y)‖ := by
      simp only [smul_sub]
      have hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r) :=
        (continuousOn_id.sub continuousOn_const).inv₀ fun z hz => sub_ne_zero.2 <| hzne _ hz
      rw [circleIntegral.integral_sub] <;> refine (hc'.smul ?_).circleIntegrable hr0.le
      · exact hc.mono <| subset_inter
          (sphere_subset_closedBall.trans <| closedBall_subset_closedBall hrR) hzne
      · exact continuousOn_const
    _ ≤ 2 * π * r * (r⁻¹ * (ε / (2 * π))) := by
      refine circleIntegral.norm_integral_le_of_norm_le_const hr0.le fun z hz => ?_
      specialize hzne z hz
      rw [mem_sphere, dist_eq_norm] at hz
      rw [norm_smul, norm_inv, hz, ← dist_eq_norm]
      refine mul_le_mul_of_nonneg_left (hδ _ ⟨?_, hzne⟩).le (inv_nonneg.2 hr0.le)
      rwa [mem_closedBall_iff_norm, hz]
    _ = ε := by field

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 σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (esymm σ R n).support = image (fun t ↦ ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)

Tactic:
rw [support_esymm']
  exact biUnion_singleton

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

Goal state before:
pp: case refine_2
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✝ : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f (p✝ * X).leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ * X))) l atTop

Tactic:
rw [leadingCoeff_mul_X] at hf

Goal state after:
case refine_2
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✝ : 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✝ * X))) l atTop
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
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun x ↦ w + ↑x
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
⊢ (Ioo l u \ g ⁻¹' s).Nonempty

Tactic:
by
    refine sdiff_nonempty.2 fun hsub => ?_
    have : (Ioo l u).Countable :=
      (hs.preimage ((add_right_injective w).comp ofReal_injective)).mono hsub
    rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this
    exact this.not_gt Cardinal.aleph0_lt_continuum

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

Goal state before:
pp: 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)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
⊢ ∫ (x : ℝ) in Set.Icc a b, f' x =
    ∑ i,
      ((∫ (x : Fin 0 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), f (e.symm (i.insertNth (e b i) x))) -
        ∫ (x : Fin 0 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), f (e.symm (i.insertNth (e a i) x)))

Tactic:
by
      simp only [← interior_Icc] at Hd
      refine
        integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ (fun _ => f)
          (fun _ => F') s hs a b hle (fun _ => Hc) (fun x hx _ => Hd x hx) _ ?_ ?_
      · exact fun x y => (OrderIso.funUnique (Fin 1) ℝ).symm.le_iff_le
      · exact (volume_preserving_funUnique (Fin 1) ℝ).symm _
      · simp [F', e]
      · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi
        exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm

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

Goal state before:
pp: p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
w : ℝ
hw : (aeval w) p = 0
⊢ (IsScalarTower.toAlgHom ℚ ℝ ℂ) ((aeval w) p) = 0

Tactic:
hw,

Goal state after:
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
w : ℝ
hw : (aeval w) p = 0
⊢ (IsScalarTower.toAlgHom ℚ ℝ ℂ) 0 = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊
this :
  (⋃ f,
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C),
        ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ ↑|(minpoly ℤ x).coeff i| = ‖↑((minpoly ℤ x).coeff i)‖

Tactic:
Int.norm_cast_rat,

Goal state after:
case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊
this :
  (⋃ f,
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C),
        ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ ↑|(minpoly ℤ x).coeff i| = ‖(minpoly ℤ x).coeff i‖
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case inr.inr
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 : M
hxpos : 0 < x
⊢ (ratLt x).Nonempty

Tactic:
obtain ⟨n, hn⟩ := Archimedean.arch 1 hxpos

Goal state after:
case inr.inr
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 : M
hxpos : 0 < x
n : ℕ
hn : 1 ≤ n • x
⊢ (ratLt x).Nonempty
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : (ofClass v).ValueGroup₀
hx : (hom v) x = 0
⊢ x = 0

Tactic:
refine (eq_of_le_of_not_lt (zero_le (a := x)) fun h_lt ↦ ?_).symm

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : (ofClass v).ValueGroup₀
hx : (hom v) x = 0
h_lt : 0 < x
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : 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
⊢ (coeff e) x * constantCoeff φ = 0

Tactic:
← map_zero (f := coeff e),

Goal state after:
σ : 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
⊢ (coeff e) x * constantCoeff φ = (coeff e) 0
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
x : MvPowerSeries σ R
hx : φ * x = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
⊢ constantCoeff φ * (coeff e) x = 0

Tactic:
← map_zero (f := coeff e),

Goal state after:
σ : 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
⊢ constantCoeff φ * (coeff e) x = (coeff e) 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsLeft R
p : MvPowerSeries σ R
⊢ (monomial n) r * p = 0 → p = 0

Tactic:
hrp

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsLeft R
p : MvPowerSeries σ R
hrp : (monomial n) r * p = 0
⊢ p = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsRight R
p : MvPowerSeries σ R
⊢ p * (monomial n) r = 0 → p = 0

Tactic:
hrp

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : r ∈ nonZeroDivisorsRight R
p : MvPowerSeries σ R
hrp : p * (monomial n) r = 0
⊢ p = 0
Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors

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

Tactic:
rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
k : Type u_3
inst✝ : Field k
⊢ 1⁻¹ = 1

Tactic:
rw [MvPowerSeries.inv_eq_iff_mul_eq_one, mul_one]

Goal state after:
σ : Type u_1
R : Type u_2
k : Type u_3
inst✝ : Field k
⊢ constantCoeff 1 ≠ 0
Module: Mathlib.AlgebraicGeometry.Geometrically.Connected

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : GeometricallyConnected f
inst✝² : GeometricallyConnected g
inst✝¹ : UniversallyOpen f
inst✝ : UniversallyOpen g
⊢ GeometricallyConnected (f ≫ g)

Tactic:
refine ⟨geometrically_iff_of_isClosedUnderIsomorphisms.mpr fun K _ x ↦ ?_⟩
  rw [← (pullbackRightPullbackFstIso g x f).hom.homeomorph.connectedSpace_iff]
  infer_instance

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.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
⊢ (ConcreteCategory.hom (F.map g₁.op)) (x i₁) = (ConcreteCategory.hom (F.map g₂.op)) (x i₂)

Tactic:
refine (h.isSeparatedFor_sieve₁ g₁ g₂ heq).ext fun W f ⟨T, u, h₁, h₂⟩ ↦ ?_

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.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
W : C
f : W ⟶ Z
x✝ : (E.sieve₁ g₁ g₂).arrows f
T : E.I₁ i₁ i₂
u : W ⟶ E.Y T
h₁ : f ≫ g₁ = u ≫ E.p₁ T
h₂ : f ≫ g₂ = u ≫ E.p₂ T
⊢ (ConcreteCategory.hom (F.map f.op)) ((ConcreteCategory.hom (F.map g₁.op)) (x i₁)) =
    (ConcreteCategory.hom (F.map f.op)) ((ConcreteCategory.hom (F.map g₂.op)) (x i₂))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ P = (↑hu.unit⁻¹ * u) • P

Tactic:
hu.val_inv_mul,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ P = 1 • P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ {u : R}, IsUnit u → ∀ {P : Fin 3 → R}, W'.Nonsingular (u • P) → W'.Nonsingular P
h : W'.Nonsingular P
⊢ W'.Nonsingular ((↑hu.unit⁻¹ * u) • P)

Tactic:
hu.val_inv_mul,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
hP : ∀ {u : R}, IsUnit u → ∀ {P : Fin 3 → R}, W'.Nonsingular (u • P) → W'.Nonsingular P
h : W'.Nonsingular P
⊢ W'.Nonsingular (1 • P)
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case e'_5
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Sieve.generate (Presieve.ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a) = ⊥

Tactic:
rw [eq_bot_iff]

Goal state after:
case e'_5
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Sieve.generate (Presieve.ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a) ≤ ⊥
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case refine_2
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ _root_.Pairwise fun i j ↦
    IsPullback (initial.to (unop (X i))) (initial.to (unop (X j)))
      (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
      (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) j)

pp: case refine_3
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows (fun x ↦ unop (X x)) (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X)))))

Tactic:
· intro i j
    exact CoproductDisjoint.isPullback_of_isInitial
      (coproductIsCoproduct' <| Discrete.functor <| unop ∘ X) initialIsInitial

Goal state after:
case refine_3
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows (fun x ↦ unop (X x)) (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X)))))
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✝ : FinitePresentation R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ FormallySmooth R (Localization.Away f)

Tactic:
rw [smoothLocus_eq_compl_support_inter, Set.subset_inter_iff, Set.subset_compl_comm,
    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
    ← LocalizedModule.subsingleton_iff_support_subset,
    Algebra.formallySmooth_iff, iff_comm, and_comm]

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Subsingleton (H1Cotangent R (Localization.Away f)) ∧
      Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ∧ (PrimeSpectrum.zeroLocus {f})ᶜ ⊆ Module.freeLocus A Ω[A⁄R]
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: case e'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])

Tactic:
have := IsLocalizedModule.iso (.powers f)
        (KaehlerDifferential.map R R A (Localization.Away f))

Goal state after:
case e'_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
⊢ Module.Projective (Localization.Away f) Ω[Localization.Away f⁄R] ↔
    Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr
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
⊢ J ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R J).comp

Tactic:
hJ

Goal state after:
case intro.mpr
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 = ⊥
⊢ Function.Injective (Ideal.Quotient.mkₐ R J).comp
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
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
r : R
x✝ : S
y✝ : Ω[A⁄R]
⊢ (algebraMap R A) r • x✝ ⊗ₜ[R] y✝ = r • x✝ ⊗ₜ[R] y✝

Tactic:
rw [mulActionBaseChange_smul_tmul, algebraMap_smul, tmul_smul]

Goal state after:
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
this : IsArtinianRing A
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
let v (i : MaximalSpectrum A) : A := (IsArtinianRing.equivPi A).symm (Pi.single i 1)

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
v : MaximalSpectrum A → A := fun i ↦ (IsArtinianRing.equivPi A).symm (Pi.single i 1)
⊢ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: case hg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Surjective ⇑(Ideal.Quotient.factorₐ R ⋯)

Tactic:
exact factor_surjective Ideal.mul_le_left

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
S : Type u_6
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsPrecomplete I R
haus : IsHausdorff (Ideal.map f I) S
x✝ : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := (Algebra.ofId R S).toLinearMap
h : Function.Surjective ⇑((restrictScalars R (Ideal.map f I)).mkQ ∘ₗ fₗ)
this : I • ⊤ = restrictScalars R (Ideal.map f I)
⊢ Function.Surjective ⇑f

Tactic:
have _ := IsHausdorff.map_algebraMap_iff.mp haus

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
S : Type u_6
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsPrecomplete I R
haus : IsHausdorff (Ideal.map f I) S
x✝¹ : Algebra R S := f.toAlgebra
fₗ : R →ₗ[R] S := (Algebra.ofId R S).toLinearMap
h : Function.Surjective ⇑((restrictScalars R (Ideal.map f I)).mkQ ∘ₗ fₗ)
this : I • ⊤ = restrictScalars R (Ideal.map f I)
x✝ : IsHausdorff I S
⊢ Function.Surjective ⇑f
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 : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
⊢ ⟨fun n ↦ (factor ⋯) ((f n) 1), ⋯⟩ = 1

Tactic:
simp only [map_one]

Goal state after:
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 : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : CommRing S
I : Ideal S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m
⊢ ⟨fun n ↦ (factor ⋯) 1, ⋯⟩ = 1
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
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
hli : LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))
hsp : Submodule.span S (Set.range fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) = ⊤
⊢ Submodule.span S (Set.range (⇑P.aevalDifferential ∘ ⇑(Pi.basisFun S σ))) = ⊤

Tactic:
convert! hsp; simp

Goal state after: