mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2

Tactic:
let n := (galActionHom p ℂ (restrict p ℂ (Complex.conjAe.restrictScalars ℚ))).support.card

Goal state after:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)
p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3
n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
⊢ Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H : Nontrivial (ofClass v).ValueGroup₀ˣ
⊢ ∃ x, v x ≠ 0 ∧ v x ≠ 1

Tactic:
by_contra! H'
    rw [nontrivial_iff_exists_ne 1] at H
    obtain ⟨x, hx⟩ := H
    obtain ⟨k, hk⟩ := ValueGroup₀.restrict₀_surjective _ x.val
    have h0 : v k ≠ 0 := by
      apply_fun embedding at hk
      simp only [embedding_restrict₀, MonoidWithZeroHom.coe_ofClass] at hk
      simp [hk]
    have h1 : v k ≠ 1 := by
      apply_fun embedding at hk
      simp only [embedding_restrict₀, MonoidWithZeroHom.coe_ofClass] at hk
      apply_fun Units.val at hx using
          Units.val_injective (α := (MonoidWithZeroHom.ofClass v).ValueGroup₀)
      intro h
      apply_fun embedding at hx using embedding_injective (f := .ofClass v)
      simp [← hk, h] at hx
    exact h1 (H' k h0)

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

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

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 : ¬(ofClass v) x = 0
⊢ (map' ↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm) ↑⟨Units.mk0 ((ofClass v) x) h0, ⋯⟩ = v x

Tactic:
<;>

Goal state after:
case pos
R : Type u_2
inst✝ : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective ⇑v
x : R
h0 : (ofClass v) x = 0
⊢ (map' ↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm) 0 = v x

case neg
R : Type u_2
inst✝ : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective ⇑v
x : R
h0 : ¬(ofClass v) x = 0
⊢ (map' ↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm) ↑⟨Units.mk0 ((ofClass v) x) h0, ⋯⟩ = v x
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
⊢ dist a x < r → dist a y < r

pp: case mpr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
⊢ dist a y < r → dist a x < r

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
⊢ dist a x < r → dist a y < r

case mpr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
⊢ dist a y < r → dist a x < r
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
h' : dist a x < r
⊢ dist a y < r

pp: case mpr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
h' : dist a y < r
⊢ dist a x < r

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
h' : dist a x < r
⊢ dist a y < r

case mpr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
h' : dist a y < r
⊢ dist a x < r
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
⊢ dist x✝ x ≤ r → dist x✝ y ≤ r

pp: case mpr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
⊢ dist x✝ y ≤ r → dist x✝ x ≤ r

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
⊢ dist x✝ x ≤ r → dist x✝ y ≤ r

case mpr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
⊢ dist x✝ y ≤ r → dist x✝ x ≤ r
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
h' : dist x✝ x ≤ r
⊢ dist x✝ y ≤ r

pp: case mpr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
h' : dist x✝ y ≤ r
⊢ dist x✝ x ≤ r

Tactic:
<;>

Goal state after:
case mp
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
h' : dist x✝ x ≤ r
⊢ dist x✝ y ≤ r

case mpr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
x✝ : X
h : dist y x ≤ r
h' : dist x✝ y ≤ r
⊢ dist x✝ x ≤ r
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

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

Tactic:
cases ball_eq_or_disjoint x y r with
    | inl hd =>
      rw [hd] at hy
      simp [h.not_ge] at hy
    | inr hd =>
      use r
      simp [h, le_compl_iff_disjoint_left, hd]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case e'_4.e_a
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) x = dist 0 x

pp: case e_a
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) y = dist x (x + y)

Tactic:
<;>

Goal state after:
case e'_4.e_a
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) x = dist 0 x

case e_a
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x ↦ ‖x‖) y = dist x (x + y)
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖₊ ≠ ‖y‖₊
⊢ ‖x * y‖₊ = max ‖x‖₊ ‖y‖₊

Tactic:
simpa only [← NNReal.coe_inj, NNReal.coe_max] using!
    norm_mul_eq_max_of_norm_ne_norm (NNReal.coe_injective.ne h)

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case ofNat
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
a✝ : ℕ
⊢ ‖x ^ Int.ofNat a✝‖₊ ≤ ‖x‖₊

pp: case negSucc
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
a✝ : ℕ
⊢ ‖x ^ Int.negSucc a✝‖₊ ≤ ‖x‖₊

Tactic:
<;>

Goal state after:
case ofNat
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
a✝ : ℕ
⊢ ‖x ^ Int.ofNat a✝‖₊ ≤ ‖x‖₊

case negSucc
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
a✝ : ℕ
⊢ ‖x ^ Int.negSucc a✝‖₊ ≤ ‖x‖₊
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case cons.refine_1
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
⊢ ‖∏ i ∈ t, f i‖ ≤ ‖f j‖ → ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖

pp: case cons.refine_2
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
⊢ ‖f j‖ ≤ ‖∏ i ∈ t, f i‖ → ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖

Tactic:
<;>

Goal state after:
case cons.refine_1
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
⊢ ‖∏ i ∈ t, f i‖ ≤ ‖f j‖ → ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖

case cons.refine_2
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
⊢ ‖f j‖ ≤ ‖∏ i ∈ t, f i‖ → ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖
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
hφ : φ ≠ 0
⊢ ∃ (ne : (⇑toLex '' Function.support φ).Nonempty), φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)

Tactic:
suffices ne : Set.Nonempty (toLex '' φ.support) by
    use ne
    unfold lexOrder
    simp only [dif_neg hφ]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ (⇑toLex '' Function.support φ).Nonempty
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

pp: case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
· -- Silly case #2 : the product is divergent
    rw [tprod_eq_one_of_not_multipliable h, norm_one']
    by_cases h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)
    · exact le_ciSup_of_le h_bd hι.some (norm_nonneg' _)
    · rw [Real.iSup_of_not_bddAbove h_bd]

Goal state after:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case cons.inr.a
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ a ∈ ↑(Finset.cons a s ha)

pp: case cons.inr.a
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ j ∈ ↑(Finset.cons a s ha)

pp: case cons.inr.a
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ a ≠ j

Tactic:
<;>

Goal state after:
case cons.inr.a
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ a ∈ ↑(Finset.cons a s ha)

case cons.inr.a
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ j ∈ ↑(Finset.cons a s ha)

case cons.inr.a
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ a ≠ j
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 : σ →₀ ℕ
⊢ (coeff d) x = (coeff d) 0

Tactic:
apply WellFoundedLT.induction d

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 : σ →₀ ℕ
⊢ ∀ (x_1 : σ →₀ ℕ), (∀ y < x_1, (coeff y) x = (coeff y) 0) → (coeff x_1) x = (coeff x_1) 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 : σ →₀ ℕ
⊢ (coeff d) x = (coeff d) 0

Tactic:
apply WellFoundedLT.induction d

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 : σ →₀ ℕ
⊢ ∀ (x_1 : σ →₀ ℕ), (∀ y < x_1, (coeff y) x = (coeff y) 0) → (coeff x_1) x = (coeff x_1) 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ False

pp: case inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ False

Tactic:
<;>

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ False

case inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit (constantCoeff φ) → IsUnit φ

Tactic:
· intro ⟨u, hu⟩
    exact ⟨⟨_, φ.invOfUnit u, mul_invOfUnit φ u hu.symm, invOfUnit_mul φ u hu.symm⟩, rfl⟩

Goal state after:
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 φ
⊢ IsUnit φ

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

Tactic:
<;>

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 φ
⊢ IsUnit φ

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
⊢ IsUnit φ ∨ IsUnit (1 - φ)

Tactic:
obtain ⟨u, h⟩ | ⟨u, h⟩ := IsLocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff φ) <;>
        [left; right] <;>
      · refine .of_mul_eq_one _ (mul_invOfUnit _ u ?_)
        simpa using h.symm

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

Goal state before:
pp: case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
h✝ : n = 0
⊢ (constantCoeff φ)⁻¹ = (coeff n) 0

pp: case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
h✝ : ¬n = 0
⊢ (-(constantCoeff φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) φ⁻¹ else 0) = (coeff n) 0

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
h✝ : n = 0
⊢ (constantCoeff φ)⁻¹ = (coeff n) 0

case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
h✝ : ¬n = 0
⊢ (-(constantCoeff φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) φ⁻¹ else 0) = (coeff n) 0
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case pos.inl
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff φ = 0
⊢ 0 = ψ⁻¹ * φ⁻¹

pp: case pos.inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff ψ = 0
⊢ 0 = ψ⁻¹ * φ⁻¹

Tactic:
<;>

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

case pos.inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff ψ = 0
⊢ 0 = ψ⁻¹ * φ⁻¹
Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
⊢ φ = 0 ∨ ψ = 0

Tactic:
simp_rw [← order_eq_top, order_mul] at h ⊢

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ.order + ψ.order = ⊤
⊢ φ.order = ⊤ ∨ ψ.order = ⊤
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
⊢ X = normalize X

Tactic:
by
  simp only [normalize_apply, normUnit_X, Units.val_one, mul_one]

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

Goal state before:
pp: k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), ↑c ≤ emultiplicity X ↑P ↔ ↑c ≤ emultiplicity Polynomial.X P

pp: k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ↑P ≠ 0

Tactic:
<;>

Goal state after:
k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), ↑c ≤ emultiplicity X ↑P ↔ ↑c ≤ emultiplicity Polynomial.X P

k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ↑P ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
this : Fact (IsUnit 2)
⊢ (ofJ j).IsElliptic

Tactic:
h0,

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
this : Fact (IsUnit 2)
⊢ (ofJ 0).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ j).IsElliptic

Tactic:
h0,

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ 0).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
this : Fact (IsUnit 2)
⊢ (ofJ j).j = j

Tactic:
h0,

Goal state after:
case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
this : Fact (IsUnit 2)
⊢ (ofJ 0).j = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ j).j = j

Tactic:
h0,

Goal state after:
case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
this : Fact (IsUnit 3)
⊢ (ofJ 0).j = 0
Module: Mathlib.AlgebraicGeometry.Geometrically.Connected

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyConnected f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : _root_.IsConnected s
hs' : IsClosed s
⊢ _root_.IsConnected (⇑f ⁻¹' s)

Tactic:
by
  refine Topology.IsCoinducing.isConnected_preimage_of_isClosed f.isConnected_preimage_singleton
    ?_ hs' hs
  exact (hf.isQuotientMap f.continuous f.surjective).isCoinducing

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

Goal state before:
pp: case «0»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨0, ⋯⟩) = P ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨1, ⋯⟩) = P ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨2, ⋯⟩) = P ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨0, ⋯⟩) = P ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨1, ⋯⟩) = P ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] ((fun i ↦ i) ⟨2, ⋯⟩) = P ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![0, -W'.dblZ P, W'.addZ P (W'.neg P)] = -W'.dblZ P • ![0, 1, 0]

Tactic:
addZ_neg,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![0, -W'.dblZ P, 0] = -W'.dblZ P • ![0, 1, 0]