mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ WellFounded ((fun x1 x2 ↦ x1 > x2) on ⇑v ∘ ⇑(algebraMap O F)) ↔
    Nonempty (↥(MonoidHom.mrange v) ≃*o WithZero (Multiplicative ℤ))

Tactic:
rw [←
    LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete_of_ne_zero
    one_ne_zero, ← Set.wellFoundedOn_range]

Goal state after:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
⊢ ((Set.range (⇑v ∘ ⇑(algebraMap O F))).WellFoundedOn fun x1 x2 ↦ x1 > x2) ↔
    {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this : IsDomain O
⊢ IsPrincipalIdealRing O

Tactic:
have : ValuationRing O := ValuationRing.of_integers v hv

Goal state after:
case inr
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝ : IsDomain O
this : ValuationRing O
⊢ IsPrincipalIdealRing O
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
hxi : IsIntegral ℤ 0
hx : ∀ (φ : K →+* A), ‖φ 0‖ = 1
⊢ False

Tactic:
map_zero,

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
hxi : IsIntegral ℤ 0
hx : ∀ (φ : K →+* A), ‖0‖ = 1
⊢ False
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
x : Multiplicative ℝ
⊢ 0 ≤ 2 ^ (↑x).log

Tactic:
by positivity

Goal state after:
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
h_lt : 0 < x
hs : (hom v) 0 < (hom v) x
⊢ False

Tactic:
map_zero,

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
hs : 0 < (hom v) x
⊢ False
Module: Mathlib.RingTheory.Valuation.Discrete.RankOne

Goal state before:
pp: case neg
R : Type u_2
inst✝ : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective ⇑v
x : R
h0 : ¬v x = 0
⊢ ↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm ⟨Units.mk0 ((ofClass v) x) h0, ⋯⟩ = unzero h0

Tactic:
← (MulEquiv.injective (intEquivOfZPowersEqTop _
    (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top))).eq_iff

Goal state after:
case neg
R : Type u_2
inst✝ : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective ⇑v
x : R
h0 : ¬v x = 0
⊢ (intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯)
      (↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm ⟨Units.mk0 ((ofClass v) x) h0, ⋯⟩) =
    (intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯) (unzero h0)
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 : ℝ
h : ∀ (y : ℚ), y.num • 1 < ↑y.den • 1 → ↑y ≤ x
y : ℚ
hy : y < 1
⊢ y.num < ↑y.den

Tactic:
by simpa using (Rat.lt_iff _ _).mp hy

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ ∀ x_1 ∈ (ball x r)ᶜ, ∃ ε > 0, ball x_1 ε ⊆ (ball x r)ᶜ

Tactic:
push _ ∈ _

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ ∀ x_1 ∉ ball x r, ∃ ε > 0, ball x_1 ε ⊆ (ball x r)ᶜ
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case pos
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : x = 0
⊢ x ∈ U

pp: case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : ¬x = 0
⊢ x ∈ U

Tactic:
· exact h (hx0 ▸ Metric.mem_ball_self hε)

Goal state after:
case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : ¬x = 0
⊢ x ∈ U
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 [← NNReal.coe_inj] using hs

Goal state after:
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 = (coeff e) 0

Tactic:
map_zero,

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 = 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
⊢ (coeff e) x = (coeff e) 0

Tactic:
map_zero,

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
⊢ (coeff e) x = 0
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
by_cases h : constantCoeff (φ * ψ) = 0

Goal state after:
case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : span {x} ≠ ⊥
⊢ ‖(embedding v.maximalIdeal) ↑x‖ *
      ↑(absNorm (v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (span {x}))) =
    1

Tactic:
← maxPowDividing_eq_pow_multiplicity hnz

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : FinitePlace K
x : 𝓞 K
hx : x ≠ 0
hnz : span {x} ≠ ⊥
⊢ ‖(embedding v.maximalIdeal) ↑x‖ * ↑(absNorm (v.maximalIdeal.maxPowDividing (span {x}))) = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : 3 = 0
⊢ ofJ 1728 = ofJ1728 F

Tactic:
exact ofJ_1728_of_three_eq_zero h3

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialX / P z ^ 2 = Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialX

Tactic:
linear_combination (norm := (rw [eval_polynomialX, Affine.evalEval_polynomialX]; ring1))
    W.a₁ * P y / P z * div_self hPz - 2 * W.a₂ * P x / P z * div_self hPz
      - W.a₄ * div_self (pow_ne_zero 2 hPz)

Goal state after:
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.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ ¬(P x / P z = Q x / Q z ∧ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z))

Tactic:
← X_eq_iff hPz hQz,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ ¬(P x * Q z = Q x * P z ∧ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z))
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
⊢ ∀ (k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit),
    (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₁
          ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit)) k) =
      (E.sigmaOfIsColimit hc).toPreOneHypercover.p₁ k ≫
        (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X PUnit.unit)).hom

Tactic:
k

Goal state after:
case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit
⊢ (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k)).hom ≫
      (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₁
        ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit)) k) =
    (E.sigmaOfIsColimit hc).toPreOneHypercover.p₁ k ≫
      (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X PUnit.unit)).hom
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
⊢ ∀ (k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit),
    (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k)).hom ≫
        (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₂
          ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit)) k) =
      (E.sigmaOfIsColimit hc).toPreOneHypercover.p₂ k ≫
        (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X PUnit.unit)).hom

Tactic:
k

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
k : (E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit
⊢ (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y k)).hom ≫
      (E.toPreOneHypercover.sigmaOfIsColimit hc hc').p₂
        ((Equiv.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.I₁ PUnit.unit PUnit.unit)) k) =
    (E.sigmaOfIsColimit hc).toPreOneHypercover.p₂ k ≫
      (Iso.refl ((E.sigmaOfIsColimit hc).toPreOneHypercover.X PUnit.unit)).hom
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
i : I
c : B ⧸ J
hix : (ι i) ((Ideal.Quotient.mk J) (1 - e i) * c) = 0
⊢ (Ideal.Quotient.mk J) 0 * c = 0

Tactic:
map_zero,

Goal state after:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
i : I
c : B ⧸ J
hix : (ι i) ((Ideal.Quotient.mk J) (1 - e i) * c) = 0
⊢ 0 * c = 0
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case w
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite 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
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ 1 * (aeval x) (minpoly K pb.gen) + (aeval x) (derivative (minpoly K pb.gen)) * u * (aeval x) (minpoly K pb.gen) = 0

pp: case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite 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
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (u * (aeval x) (minpoly K pb.gen)) ^ 2 = 0

Tactic:
← add_mul,

Goal state after:
case w
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite 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
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (1 + (aeval x) (derivative (minpoly K pb.gen)) * u) * (aeval x) (minpoly K pb.gen) = 0

case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite 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
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (u * (aeval x) (minpoly K pb.gen)) ^ 2 = 0
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case refine_5
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⟮α⟯
⊢ ∀ (r : K),
    (↑↑{ toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ }).toFun
        ((algebraMap K L) r) =
      (algebraMap K B) r

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⟮α⟯
⊢ (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' := ?refine_5 } =
    f

Tactic:
· intro r
    change g _ (algebraMap K _ r) = _
    rw [AlgHom.commutes]

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⟮α⟯
⊢ (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' := ⋯ } =
    f