mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
⊢ ∃ i' fi'i, ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2

Tactic:
choose k fk hk using fun j ↦ exists_map_preimage_le_map_preimage D c hc (h𝒱𝒰 j).1.isCompact
      (V := t.app i ⁻¹ᵁ j.1.1.2.1.2.1) (by
      rw [← Hom.comp_preimage, ← NatTrans.comp_app, ha]
      exact (h𝒱𝒰 j).2.symm.trans_le (j.1.prop.2.trans (a.preimage_mono j.1.1.2.prop.2)))

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
k : ↥s → I
fk : (j : ↥s) → k j ⟶ i
hk : ∀ (j : ↥s), D.map (fk j) ⁻¹ᵁ 𝒱 j ≤ D.map (fk j) ⁻¹ᵁ t.app i ⁻¹ᵁ ↑(↑(↑↑j).2).2
⊢ ∃ i' fi'i, ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₃
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 3 * (E.a₃ + 0 * E.a₁ + 2 * 0) = E'.a₃

Tactic:
a₃_of_isCharTwoJNeZeroNF

Goal state after:
case h.a₃
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 3 * (0 + 0 * E.a₁ + 2 * 0) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : W.IsCharThreeNF
⊢ W.IsCharNeTwoNF

Tactic:
cases ‹W.IsCharThreeNF›

Goal state after:
case of_j_ne_zero
R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : W.IsCharThreeJNeZeroNF
⊢ W.IsCharNeTwoNF

case of_j_eq_zero
R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.IsCharNeTwoNF
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.a₃ ^ 2 + 4 * W.a₆ = 4 * W.a₆

Tactic:
a₃_of_isCharTwoJNeZeroNF

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 0 ^ 2 + 4 * W.a₆ = 4 * W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case of_j_ne_zero.of_j_ne_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharTwoJNeZeroNF
⊢ ∃ C, C • E = E'

Tactic:
simp_rw [← variableChange_j E C, ← variableChange_j E' C',
        j_of_isCharTwoJNeZeroNF_of_char_two, one_div, inv_inj] at heq
      obtain ⟨C'', hC⟩ := exists_variableChange_of_char_two_of_j_ne_zero _ _ heq
      use C'⁻¹ * C'' * C
      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ u • P ≈ v • Q ↔ P ≈ Q

Tactic:
by
  rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : u ^ 4 = E.a₄ / E'.a₄
⊢ u ^ 6 = E.a₆ / E'.a₆

Tactic:
rw [pow_mul u 2 3, hu]

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : u ^ 4 = E.a₄ / E'.a₄
⊢ (E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)) ^ 3 = E.a₆ / E'.a₆
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y ≤ᵥ z
⊢ x * y ≤ᵥ x * z

Tactic:
grw [veq_mul_comm, veq_mul_comm (x := x)]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y ≤ᵥ z
⊢ y * x ≤ᵥ z * x
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

Tactic:
· absurd hx
      apply vle_mul_cancel t.prop
      simpa using vle_trans h₁ (mul_vle_mul_left hy s)

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map (fun x ↦ ↑x⁻¹) (Filter.comap coe' (𝓝 y)))

Tactic:
rw [this, ← Filter.map_map]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map (fun y ↦ ↑y) (map (fun x ↦ x⁻¹) (Filter.comap coe' (𝓝 y))))
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
⊢ ContinuousAt Inv.inv x

Tactic:
have : { y | hatInv y = y⁻¹ } ∈ 𝓝 x :=
        haveI : {(0 : hat K)}ᶜ ⊆ { y : hat K | hatInv y = y⁻¹ } := by
          intro y y_ne
          rw [mem_compl_singleton_iff] at y_ne
          dsimp [Inv.inv]
          rw [if_neg y_ne]
        mem_of_superset (compl_singleton_mem_nhds x_ne) this

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : {y | y.hatInv = y⁻¹} ∈ 𝓝 x
⊢ ContinuousAt Inv.inv x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b a : G
h : b = |a|ₘ ∧ 1 < b
ha : 1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

Tactic:
rw [mabs, sup_eq_left.mpr ((inv_le_one'.mpr ha).trans ha)] at h

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b a : G
h : b = a ∧ 1 < b
ha : 1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : 1 < b ^ k
⊢ b ≤ b ^ k

Tactic:
rw [← zpow_one b, ← zpow_mul, one_mul, zpow_le_zpow_iff_right h, ← zero_add 1,
          ← Int.lt_iff_add_one_le]

Goal state after:
case refine_2
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : 1 < b ^ k
⊢ 0 < k
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
x : G₀
hx : x ≠ 0
⊢ x ∈ {x | g⁻¹ ≤ x} → (fun x ↦ x⁻¹) x ∈ {x | x ≤ g} \ {0}

Tactic:
simp only [mem_ofPred_eq, mem_sdiff, mem_singleton_iff, inv_eq_zero, hx, not_false_eq_true,
      and_true]

Goal state after:
case refine_1.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
x : G₀
hx : x ≠ 0
⊢ g⁻¹ ≤ x → x⁻¹ ≤ g
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ = (X * mk fun p ↦ (coeff (p + 1)) φ) + C (constantCoeff φ)

Tactic:
by
  ext (_ | n)
  · simp
  · simp only [coeff_succ_X_mul, coeff_mk, map_add, coeff_C, n.succ_ne_zero,
      if_false, add_zero]

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = k - n + n
⊢ a * b = 0

Tactic:
tsub_add_cancel_of_le h₁

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = k
⊢ a * b = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : single s 1 = single t 1
h : 1 = 1
⊢ s = t

pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ s = t

Tactic:
· rw [Finsupp.single_eq_single_iff] at H
      rcases H with H | H
      · exact H.1
      · exfalso
        exact one_ne_zero H.1

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
H : ¬single s 1 = single t 1
h : 1 = 0
⊢ s = t
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
⊢ v.intValuation r = 1 ↔ r ∈ v.asIdeal.primeCompl

Tactic:
simp [Ideal.primeCompl, ← intValuation_lt_one_iff_mem, LE.le.ge_iff_eq (intValuation_le_one v r)]

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

Goal state before:
pp: A : Type u_2
inst✝ : CommRing A
a : A
⊢ (rescale a) X = C a * X

Tactic:
by
  ext
  simp only [coeff_rescale, coeff_C_mul, coeff_X]
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (MvPowerSeries.coeff m) ↑((monomial n) a) = (MvPowerSeries.coeff m) ((MvPowerSeries.monomial n) a)

Tactic:
rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
    split_ifs with h₁ h₂ <;> first | rfl | subst m; contradiction

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ min (weightedOrder w f) (weightedOrder w g) ≤ weightedOrder w (f + g)

Tactic:
by
  apply le_weightedOrder w
  simp +contextual only
    [coeff_eq_zero_of_lt_weightedOrder w, lt_min_iff, map_add, add_zero,
      imp_true_iff]

Goal state after:
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f g : ι →₀ α
⊢ #(Ioc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]

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

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
this :
  ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
    weightedOrder w f ≠ weightedOrder w g →
      weightedOrder w f < weightedOrder w g → weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)

Tactic:
rw [add_comm f g, inf_comm]

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
this :
  ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
    weightedOrder w f ≠ weightedOrder w g →
      weightedOrder w f < weightedOrder w g → weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (g + f) ≤ min (weightedOrder w g) (weightedOrder w f)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : ↑((weight w) i) < weightedOrder w f
⊢ (coeff (i, j).1) f * (coeff (i, j).2) g = 0

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : weightedOrder w f ≤ ↑((weight w) i)
⊢ (coeff (i, j).1) f * (coeff (i, j).2) g = 0

Tactic:
· rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : weightedOrder w f ≤ ↑((weight w) i)
⊢ (coeff (i, j).1) f * (coeff (i, j).2) g = 0
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: case inl
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 * x2) (0, ⊤)

pp: case inr
a : ℕ∞
ha : 0 < a
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 * x2) (a, ⊤)

Tactic:
· simp [ContinuousAt, nhds_prod_eq]

Goal state after:
case inr
a : ℕ∞
ha : 0 < a
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 * x2) (a, ⊤)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
h : Function.Surjective ⇑Valued.v
⊢ Function.Surjective ⇑Valued.v

Tactic:
exact h.comp (adicCompletion.toCompletion_surjective K v)

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ (MonoidWithZeroHom.ofClass Valued.v).valueGroup = (MonoidWithZeroHom.ofClass (valuation K v)).valueGroup

Tactic:
by
  ext n
  simp only [MonoidWithZeroHom.mem_valueGroup_iff_of_comm, ne_eq, MonoidWithZeroHom.coe_ofClass]
  refine ⟨fun ⟨a, ha0, x, hx⟩ ↦ ?_, fun ⟨a, ha0, x, hx⟩ ↦
    ⟨↑a, by simpa using ha0, ↑x, by simpa using hx⟩⟩
  obtain ⟨b, hb⟩ := valuation_surjective K v (Valued.v a)
  obtain ⟨y, hy⟩ := valuation_surjective K v (Valued.v x)
  exact ⟨b, by rw [hb]; exact ha0, y, by rw [hb, hy]; exact hx⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (trunc (n + 2)) X = Polynomial.X

Tactic:
by
  ext d
  rw [coeff_trunc, coeff_X]
  split_ifs with h₁ h₂
  · rw [h₂, coeff_X_one]
  · rw [coeff_X_of_ne_one h₂]
  · rw [coeff_X_of_ne_one]
    intro hd
    apply h₁
    rw [hd]
    exact n.one_lt_succ_succ

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ constantCoeff φ = 0 → 1 ≤ φ.order

Tactic:
· intro h
    refine le_order _ _ fun d hd ↦ ?_
    rw [Nat.cast_lt_one] at hd
    simp [hd, h]

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

Goal state before:
pp: case succ
R : Type u_2
inst✝ : CommSemiring R
f : R⟦X⟧
n a : ℕ
ih : (trunc n) (↑((trunc n) f) ^ a) = (trunc n) (f ^ a)
⊢ (trunc n) (↑((trunc n) f) ^ (a + 1)) = (trunc n) (f ^ (a + 1))

Tactic:
rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
      ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case a.convert_1
⊢ ℝ

Tactic:
exact 1 / 3

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x ↦ a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠

Tactic:
exact one_lt_aleph0.trans (cantor _)

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f g : R⟦X⟧
⊢ subst a (f * g) = subst a f * subst a g

Tactic:
by
  rw [← coe_substAlgHom ha, map_mul]

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

Goal state before:
pp: case pos.hnc
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
j : ℕ
hj : n = k * j
⊢ j = n / k

Tactic:
rw [hj, Nat.mul_div_cancel_left j hk.pos]

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
hc : c ≠ 0
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ

Tactic:
refine ENNReal.mul_le_of_le_div' <| le_trans ?_ ENNReal.coe_div_le

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑(‖a‖₊ / ‖c‖₊)
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑(‖a‖₊ / ‖c‖₊)

Tactic:
rw [div_eq_inv_mul, ← nnnorm_inv, ← nnnorm_mul]

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑‖c⁻¹ * a‖₊
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝³ : RingHomIsometric σ
inst✝² : RingHomInvPair σ σ'
F' : Type u_1
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
⊢ HasDerivAt (⇑L ∘ f ∘ ⇑σ') (L f') (σ x)

Tactic:
let R : 𝕜 →SL[σ'] 𝕜 := ⟨σ'.toSemilinearMap, σ'.isometry.continuous⟩

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝³ : RingHomIsometric σ
inst✝² : RingHomInvPair σ σ'
F' : Type u_1
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
⊢ HasDerivAt (⇑L ∘ f ∘ ⇑σ') (L f') (σ x)
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
n : ℕ
x✝ : Fin n → E
⊢ (constFormalMultilinearSeries 𝕜 E 0 n) x✝ = (0 n) x✝

Tactic:
induction n

Goal state after:
case zero
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
x✝ : Fin 0 → E
⊢ (constFormalMultilinearSeries 𝕜 E 0 0) x✝ = (0 0) x✝

case succ
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
n✝ : ℕ
a✝ : ∀ (x : Fin n✝ → E), (constFormalMultilinearSeries 𝕜 E 0 n✝) x = (0 n✝) x
x✝ : Fin (n✝ + 1) → E
⊢ (constFormalMultilinearSeries 𝕜 E 0 (n✝ + 1)) x✝ = (0 (n✝ + 1)) x✝
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h₀ : 0 < ↑r
a✝ : ℝ
ha✝ : a✝ ∈ Ioo (-1) 1
hp✝ : (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a✝ ^ x
this✝ :
  (∃ a ∈ Ioo (-1) 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a ^ x) ↔
    ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : ↑a ∈ Ioo 0 1
hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n
this : r < r / a
⊢ ↑r < p.radius

Tactic:
← ENNReal.coe_lt_coe

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h₀ : 0 < ↑r
a✝ : ℝ
ha✝ : a✝ ∈ Ioo (-1) 1
hp✝ : (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a✝ ^ x
this✝ :
  (∃ a ∈ Ioo (-1) 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =O[atTop] fun x ↦ a ^ x) ↔
    ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : ↑a ∈ Ioo 0 1
hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n
this : ↑r < ↑(r / a)
⊢ ↑r < p.radius