mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s).Pairwise fun i j ↦ ‖f i‖ ≠ ‖f j‖
⊢ (↑s).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊

Tactic:
simpa using

Goal state after:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s).Pairwise fun i j ↦ ‖f i‖ ≠ ‖f j‖
⊢ (↑s).Pairwise fun i j ↦ ¬‖f i‖ = ‖f j‖
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
⊢ U ∈ nhds 0 ↔ ∃ γ, {x | valuation.restrict x < ↑γ} ⊆ U

Tactic:
rw [Metric.mem_nhds_iff]
      refine ⟨?_, ?_⟩
      · rintro ⟨ε, hε, h⟩
        rcases RankLeOne.exists_val_lt (valuation (K := K)) with H | H
        · use Units.mk0 (valuation.restrict 1) (by simp)
          intro x hx
          simp only [Units.val_mk0, mem_ofPred_eq, map_one] at hx
          by_cases hx0 : x = 0
          · exact h (hx0 ▸ Metric.mem_ball_self hε)
          · exfalso
            rw [← (valuation (K := K)).restrict.zero_iff, ← ne_eq, ← isUnit_iff_ne_zero] at hx0
            apply not_le.mpr hx
            apply le_of_eq
            rw [eq_comm]
            simpa only [Units.ext_iff, hx0.unit_spec, Units.val_one,
              Submonoid.mk_eq_one] using! H.elim hx0.unit 1
        · obtain ⟨x, hx, hxy⟩ := H (γ := ⟨ε, le_of_lt hε⟩) (pos_iff_ne_zero.mp hε)
          use Units.mk0 (valuation.restrict x) (by simp [Valuation.restrict_def, hx])
          intro y hy
          apply h
          simp only [Metric.mem_ball, dist_zero_right]
          simp only [Units.val_mk0, mem_ofPred_eq, restrict_lt_iff, ← NNReal.coe_lt_coe] at hy
          apply lt_trans hy
          simpa [RankLeOne.hom', valuation.restrict_def] using! hxy
      · rintro ⟨ε, hε⟩
        refine ⟨(embedding ε.1 : ℝ≥0), ?_, fun x hx ↦ hε ?_⟩
        · exact NNReal.coe_pos.mpr <| embedding_strictMono.lt_iff_lt.mpr ε.zero_lt
        · simpa [restrict_lt_iff_lt_embedding] using! (mem_ball_zero_iff.mp hx)

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 Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
hx : v.norm x = 0
⊢ x = 0

Tactic:
simpa using

Goal state after:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
hx : v.norm x = 0
⊢ x = 0
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
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
⊢ φ.lexOrder ≤ ↑(toLex u) → ¬ψ.lexOrder ≤ ↑(toLex v)

Tactic:
intro hu

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hu : φ.lexOrder ≤ ↑(toLex u)
⊢ ¬ψ.lexOrder ≤ ↑(toLex v)
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

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

Tactic:
simpa using

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
s : R
hrs : r * s = 0
this : C s = 0
⊢ s = 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
hrp : (monomial n) r * p = 0
i : σ →₀ ℕ
this : r * (coeff i) p = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0

Tactic:
simpa using

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
i : σ →₀ ℕ
this : r * (coeff i) p = (coeff (i + n)) 0
⊢ (coeff i) p = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

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

Tactic:
simpa using

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
s : R
hrs : s * r = 0
this : C s = 0
⊢ s = 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
hrp : p * (monomial n) r = 0
i : σ →₀ ℕ
this : (coeff i) p * r = (coeff (i + n)) 0
⊢ (coeff i) p = (coeff i) 0

Tactic:
simpa using

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
i : σ →₀ ℕ
this : (coeff i) p * r = (coeff (i + n)) 0
⊢ (coeff i) p = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
h : φ * ψ = 0
w✝ : LinearOrder σ
h✝ : WellFoundedGT σ
⊢ φ = 0 ∨ ψ = 0

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
h : φ * ψ = 0
w✝ : LinearOrder σ
h✝ : WellFoundedGT σ
⊢ φ.lexOrder = ⊤ ∨ ψ.lexOrder = ⊤
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = constantCoeff φ
⊢ constantCoeff φ = ↑u

Tactic:
simpa using

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = constantCoeff φ
⊢ constantCoeff φ = ↑u
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = 1 - constantCoeff φ
⊢ constantCoeff (1 - φ) = ↑u

Tactic:
simpa using

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = 1 - constantCoeff φ
⊢ 1 - constantCoeff φ = ↑u
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : φ⁻¹ = 0
⊢ constantCoeff φ = 0

Tactic:
simpa using

Goal state after:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : φ⁻¹ = 0
⊢ constantCoeff φ = 0
Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : X = 0
⊢ False

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : X = 0
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : ¬weightedOrder w f < ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g

Tactic:
rw [not_lt_top_iff] at hf

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f = ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ constantCoeff (C r) ≠ 0

Tactic:
simpa using

Goal state after:
case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ ¬r = 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h.inr.hc.refine_1
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (match (i, j) with
        | (a, b) => (single () a, single () b)).2
      PUnit.unit ≤
    (single () n) PUnit.unit

Tactic:
simpa using

Goal state after:
case neg.e_a.h.inr.hc.refine_1
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ j ≤ n
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h.inr.hc.refine_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
hh :
  single () n ≤
    (match (i, j) with
      | (a, b) => (single () a, single () b)).2
⊢ n ≤ j

Tactic:
simpa using

Goal state after:
case neg.e_a.h.inr.hc.refine_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
hh :
  single () n ≤
    (match (i, j) with
      | (a, b) => (single () a, single () b)).2
⊢ n ≤ j
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ ¬(Set.range ⇑(valuation K v)).Subsingleton

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ (Set.range ⇑(valuation K v)).Nontrivial
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ ¬(Set.range ⇑Valued.v).Subsingleton

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ (Set.range ⇑Valued.v).Nontrivial
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
⊢ ∀ {x : k⟦X⟧}, x ≠ 0 → ∃ n, Associated (X ^ n) x

Tactic:
by
        intro f hf
        use f.order.toNat
        use Unit_of_divided_by_X_pow_order f
        simp only [Unit_of_divided_by_X_pow_order_nonzero hf]
        exact X_pow_order_mul_divXPowOrder

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

Goal state before:
pp: K : Type u_1
inst✝⁵ : Field K
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : IsDedekindDomain R
inst✝¹ : IsFractionRing R K
v✝ : HeightOneSpectrum R
inst✝ : NumberField K
v : FinitePlace K
x y : K
⊢ v (x + y) ≤ v x + v y

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝⁵ : Field K
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : IsDedekindDomain R
inst✝¹ : IsFractionRing R K
v✝ : HeightOneSpectrum R
inst✝ : NumberField K
v : FinitePlace K
x y : K
⊢ ↑v (x + y) ≤ ↑v x + ↑v y
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖

Tactic:
← norm_lt_one_iff_mem K

Goal state after:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : ‖(embedding v₁) ((algebraMap (𝓞 K) K) x)‖ < 1
hx2 : x ∉ v₂.asIdeal
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x y : K
w : HeightOneSpectrum (𝓞 K)
hw : place (embedding w) = ↑v
H : ∀ (x : K), v x = (HeightOneSpectrum.adicAbv K w) x
⊢ v (x + y) ≤ max (v x) (v y)

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x y : K
w : HeightOneSpectrum (𝓞 K)
hw : place (embedding w) = ↑v
H : ∀ (x : K), v x = (HeightOneSpectrum.adicAbv K w) x
⊢ (HeightOneSpectrum.adicAbv K w) (x + y) ≤ max ((HeightOneSpectrum.adicAbv K w) x) ((HeightOneSpectrum.adicAbv K w) y)
Module: Mathlib.AlgebraicGeometry.Geometrically.Connected

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : GeometricallyConnected f
inst✝ : ConnectedSpace ↥S
hf : IsOpenMap ⇑f
⊢ ConnectedSpace ↥X

Tactic:
simpa using

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝¹ : GeometricallyConnected f
inst✝ : ConnectedSpace ↥S
hf : IsOpenMap ⇑f
⊢ _root_.IsConnected Set.univ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: 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
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.dblXYZ P =
    W.dblZ P •
      ![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:
dblXYZ_of_Z_ne_zero hP hQ hPz hQz hx hy

Goal state after:
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
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.dblZ P •
      ![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] =
    W.dblZ P •
      ![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]
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hF : Presieve.IsSheaf J F
S : Sieve X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows

Tactic:
intro Y f

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hF : Presieve.IsSheaf J F
S : Sieve X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
Y : C
f : Y ⟶ X
⊢ Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: X : TopCat
E : precoverage.ZeroHypercover X
⊢ ∀ (x : ↑X), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (E.f i))

Tactic:
simpa using

Goal state after:
X : TopCat
E : precoverage.ZeroHypercover X
⊢ ∀ (x : ↑X), ∃ i y, (ConcreteCategory.hom (E.f i)) y = x
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: X : TopCat
E : precoverage.ZeroHypercover X
⊢ ∀ (i : E.I₀), Topology.IsOpenEmbedding ⇑(ConcreteCategory.hom (E.f i))

Tactic:
simpa using

Goal state after:
X : TopCat
E : precoverage.ZeroHypercover X
⊢ ∀ (i : E.I₀), Topology.IsOpenEmbedding ⇑(ConcreteCategory.hom (E.f i))
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: X : TopCat
E : precoverage.ZeroHypercover X
⊢ ∀ (i : E.I₀), Topology.IsOpenEmbedding ⇑(ConcreteCategory.hom (E.f i))

Tactic:
simpa using E.mem₀.right

Goal state after:
Module: Mathlib.AlgebraicGeometry.GluingOneHypercover

Goal state before:
pp: D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
T : Scheme
g : T ⟶ W
x✝ : ⊤.arrows g
⊢ (g ≫ p₁) ≫ D.ι i₁ = (g ≫ p₂) ≫ D.ι i₂

Tactic:
simpa using

Goal state after:
D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
T : Scheme
g : T ⟶ W
x✝ : ⊤.arrows g
⊢ g ≫ p₁ ≫ D.ι i₁ = g ≫ p₂ ≫ D.ι i₂
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: ⊢ precoverage ≤ Precoverage.comap uliftFunctor precoverage

Tactic:
refine Precoverage.le_of_zeroHypercover fun X E ↦ ?_
  refine ⟨?_, ?_⟩
  · simp only [Presieve.map_ofArrows, Precoverage.mem_comap_iff,
      Types.ofArrows_mem_jointlySurjectivePrecoverage_iff, ConcreteCategory.hom_ofHom,
      Set.mem_range, TypeCat.Fun.coe_mk]
    intro ⟨x⟩
    obtain ⟨i, y, rfl⟩ := exists_mem_zeroHypercover_range E x
    use i, ⟨y⟩
    rfl
  · simp only [Presieve.map_ofArrows, MorphismProperty.ofArrows_mem_precoverage,
      isOpenEmbedding_iff]
    intro i
    exact (isOpenEmbedding_f_zeroHypercover _ _).uliftMap

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

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

Tactic:
simpa using

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
⊢ ∃ r ∈ s, r ∉ x.asIdeal
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
p : Ideal A
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
f : A
hxf : { asIdeal := p, isPrime := inst✝¹ } ∈ ↑(basicOpen f)
hf : ↑(basicOpen f) ⊆ smoothLocus R A
⊢ f ∉ p

Tactic:
simpa using

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
p : Ideal A
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
f : A
hxf : { asIdeal := p, isPrime := inst✝¹ } ∈ ↑(basicOpen f)
hf : ↑(basicOpen f) ⊆ smoothLocus R A
⊢ f ∉ p
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case refine_6
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
x : L
⊢ ((Ideal.Quotient.mkₐ K I).comp
        { toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯, commutes' := ⋯ })
      x =
    f x

Tactic:
simpa using

Goal state after:
case refine_6
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
x : L
⊢ (Ideal.Quotient.mk I) ((g x) (IntermediateField.AdjoinSimple.gen K x)) = f x
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
this✝² : IsArtinianRing A
this✝¹ : IsReduced A
this✝ : Field (A ⧸ p) := Ideal.Quotient.field p
this : ∀ (i : MaximalSpectrum A), FormallyEtale K (A ⧸ i.asIdeal)
⊢ FormallyEtale K (A ⧸ p)

Tactic:
exact this ⟨p, inferInstance⟩

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.tmul.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
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
  AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm) (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
      TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
y : Ω[A⁄R]
x : A
z : S
⊢ e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • (Algebra.IsPushout.equiv R A S B) (x ⊗ₜ[R] z) ⊗ₜ[A] y) =
    (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ ((Algebra.IsPushout.equiv R A S B) (x ⊗ₜ[R] z) ⊗ₜ[A] y)

Tactic:
| tmul x z =>

Goal state after:
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₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
x : ↥M'
⊢ IsUnit (((IsScalarTower.toAlgHom R P S).comp f₀) ↑x)

Tactic:
simpa using

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
P' : Type u_1 := Localization M'
x : ↥M'
⊢ IsUnit ((algebraMap P S) (f₀ ↑x))