mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
hyc : closure {y} = closure {y'}
Hx : ∀ (z : ↥(closure {x})), z ∈ zpowers ⟨x', ⋯⟩
Hy : ∀ (z : ↥(closure {y})), z ∈ zpowers ⟨y', ⋯⟩
a : ↥(closure {x})
⊢ ∀ {b : ↥(closure {x})}, (mulEquivOfOrderOfEq Hx Hy ⋯).toFun a ≤ (mulEquivOfOrderOfEq Hx Hy ⋯).toFun b ↔ a ≤ b

Tactic:
b

Goal state after:
case refine_2
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
hyc : closure {y} = closure {y'}
Hx : ∀ (z : ↥(closure {x})), z ∈ zpowers ⟨x', ⋯⟩
Hy : ∀ (z : ↥(closure {y})), z ∈ zpowers ⟨y', ⋯⟩
a b : ↥(closure {x})
⊢ (mulEquivOfOrderOfEq Hx Hy ⋯).toFun a ≤ (mulEquivOfOrderOfEq Hx Hy ⋯).toFun b ↔ a ≤ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
⊢ G ≃+o ℤ

Tactic:
have : IsLeast {y : G | y ∈ (⊤ : AddSubgroup G) ∧ 0 < y} x := by simpa using h
  replace this := AddSubgroup.cyclic_of_min this
  let e : G ≃+o (⊤ : AddSubgroup G) := ⟨AddSubsemigroup.topEquiv.symm,
    (AddEquiv.strictMono_symm AddSubsemigroup.strictMono_topEquiv).le_iff_le⟩
  let e' : (⊤ : AddSubgroup G) ≃+o AddSubgroup.closure {x} :=
    ⟨AddEquiv.subsemigroupCongr (by simp [this]),
     (AddEquiv.strictMono_subsemigroupCongr _).le_iff_le⟩
  let g : (⊤ : AddSubgroup ℤ) ≃+o ℤ := ⟨AddSubsemigroup.topEquiv,
    (AddSubsemigroup.strictMono_topEquiv).le_iff_le⟩
  let g' : AddSubgroup.closure ({1} : Set ℤ) ≃+o (⊤ : AddSubgroup ℤ) :=
    ⟨(.subsemigroupCongr (by simp)),
     (AddEquiv.strictMono_subsemigroupCongr _).le_iff_le⟩
  let f := closure_equiv_closure x (1 : ℤ) (by simp [h.left.ne'])
  exact ((((e.trans e').trans f).trans g').trans g : G ≃+o ℤ)

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a : G₀
⊢ ∀ {b : G₀},
    (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
        (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
      a ≤ b

Tactic:
b

Goal state after:
case refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
⊢ (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
    a ≤ b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
h : IsIntegral R W
⊢ (valuation K (maximalIdeal R)) W.Δ ≤ 1

Tactic:
choose r hr using Δ_integral_of_isIntegral R W

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
h : IsIntegral R W
r : R
hr : (algebraMap R K) r = W.Δ
⊢ (valuation K (maximalIdeal R)) W.Δ ≤ 1
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
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
a : G₀
ha : g⁻¹ ≤ a
⊢ ∀ (b : G₀), g⁻¹ ≤ b → a < b → b⁻¹ < a⁻¹

Tactic:
b

Goal state after:
case refine_2
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
a : G₀
ha : g⁻¹ ≤ a
b : G₀
⊢ g⁻¹ ≤ b → a < b → b⁻¹ < a⁻¹
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
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
⊢ ∀ (a : G₀), g⁻¹ ≤ a → ∀ (b : G₀), g⁻¹ ≤ b → a < b → b⁻¹ < a⁻¹

Tactic:
intro a ha b _

Goal state after:
case refine_2
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
a : G₀
ha : g⁻¹ ≤ a
b : G₀
x✝ : g⁻¹ ≤ b
⊢ a < b → b⁻¹ < a⁻¹
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
hW : IsMinimal R W
h :
  ¬(valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) (integralModel R W).Δ) < 1 ↔
    (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R
⊢ IsMinimal R W ∧ (valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) (integralModel R W).Δ) = 1 ↔
    ¬(valuation K (IsDiscreteValuationRing.maximalIdeal R)) ((algebraMap R K) (integralModel R W).Δ) < 1

Tactic:
simpa [hW] using (valuation_le_one (R := R) (K := K) _ _).ge_iff_eq.symm

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
hW : IsMinimal R W
⊢ HasGoodReduction R W ↔ (reduction R W).IsElliptic

Tactic:
by
  refine Iff.trans ?_ (W.reduction R).isElliptic_iff.symm
  simp only [reduction, map_Δ, isUnit_iff_ne_zero, ne_eq, residue_eq_zero_iff]
  have h :
      ¬(valuation K (maximalIdeal R) (algebraMap R K (integralModel R W).Δ) < 1)
      ↔ (integralModel R W).Δ ∉ IsLocalRing.maximalIdeal R :=
    not_iff_not.mpr <| valuation_lt_one_iff_mem _ _
  refine ((integralModel_Δ_eq R W ▸ hasGoodReduction_iff _ _).trans ?_).trans h
  simpa [hW] using (valuation_le_one (R := R) (K := K) _ _).ge_iff_eq.symm

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a : G₀
a✝¹ : a ≤ g
a✝ : ¬a = 0
⊢ ∀ b ≤ g, ¬b = 0 → b < a → a⁻¹ < b⁻¹

Tactic:
b

Goal state after:
case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a : G₀
a✝¹ : a ≤ g
a✝ : ¬a = 0
b : G₀
⊢ b ≤ g → ¬b = 0 → b < a → a⁻¹ < b⁻¹
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a : (ofClass v).ValueGroup₀
⊢ ∀ ⦃a₂ : (ofClass v).ValueGroup₀⦄,
    valueGroup₀_hom_extensionValuation a = valueGroup₀_hom_extensionValuation a₂ → a = a₂

Tactic:
b

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
⊢ valueGroup₀_hom_extensionValuation a = valueGroup₀_hom_extensionValuation b → a = b
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
a : R
⊢ ∀ ⦃a₂ : R⦄, C a = C a₂ → a = a₂

Tactic:
b

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
a b : R
⊢ C a = C b → a = b
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ (if 0 = single s 1 then 1 else 0) = 0

Tactic:
if_neg

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ 0 = 0

case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ ¬0 = single s 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : R
φ : MvPowerSeries σ A
⊢ ((map (algebraMap R A)).comp C) a * φ = φ * ((map (algebraMap R A)).comp C) a

Tactic:
by
    ext n
    simp [Algebra.commutes]

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

Goal state before:
pp: case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ (if b = d then a else 0) = 0

Tactic:
if_neg

Goal state after:
case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ 0 = 0

case neg.right.hnc
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ ¬b = d
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
s : Finset (σ →₀ ℕ)
inst✝ : CommSemiring S
f : R →+* S
p : MvPowerSeries σ R
⊢ (truncFinset S s) ((map f) p) = (MvPolynomial.map f) ((truncFinset R s) p)

Tactic:
ext x
  by_cases x ∈ s <;> grind [coeff_map, MvPolynomial.coeff_map]

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

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ weightedOrder w (p.toSubring T hp) = weightedOrder w p

Tactic:
refine eq_of_le_of_ge ?_ ?_
  · refine le_weightedOrder w fun d hd => by
      simp [coeff_eq_zero_of_lt_weightedOrder w hd, ← p.coeff_toSubring T hp]
  · refine le_weightedOrder w fun d hd => by
      exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_eq_zero_of_lt_weightedOrder w hd)

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

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
h : 1 ≤ f.order
⊢ ↑(degree 0) < f.order

Tactic:
simpa using Order.one_le_iff_pos.mp h

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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ ¬Valued.v a = 0

Tactic:
exact ha0

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ Tendsto (fun i ↦ (coeff d) ↑((trunc' R i) f)) atTop (𝓝 ((coeff d) f))

Tactic:
exact tendsto_atTop_of_eventually_const fun n (hdn : d ≤ n) ↦ (by simp [coeff_trunc', hdn])

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
⊢ uR • S = uR • ↑J ∪ (uR * uR) • ↑J

Tactic:
S,

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
⊢ uR • (↑J ∪ uR • ↑J) = uR • ↑J ∪ (uR * uR) • ↑J
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
⊢ uR' • S = uR' • ↑J ∪ uR • uR' • ↑J

Tactic:
S,

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
⊢ uR' • (↑J ∪ uR • ↑J) = uR' • ↑J ∪ uR • uR' • ↑J
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
⊢ uR' • S = uR' • ↑J ∪ uR • uR' • ↑J

Tactic:
simp_rw [S, smul_union, smul_comm]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
⊢ (if m < n then (coeff m) (φ + ψ) else 0) = (if m < n then (coeff m) φ else 0) + if m < n then (coeff m) ψ else 0

Tactic:
split_ifs with H

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : m < n
⊢ (coeff m) (φ + ψ) = (coeff m) φ + (coeff m) ψ

case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : ¬m < n
⊢ 0 = 0 + 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0

Tactic:
split_ifs with H

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : m < n + 1
h✝ : m = 0
⊢ a = a

case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : m < n + 1
h✝ : ¬m = 0
⊢ 0 = 0

case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : m = 0
⊢ 0 = a

case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : ¬m = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : 1 ≤ φ.order
⊢ ↑0 < φ.order

Tactic:
simpa using Order.one_le_iff_pos.mp h

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ 0 = Polynomial.X.coeff d

Tactic:
· 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 neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ (if i = n then a else 0) = 0

Tactic:
if_neg

Goal state after:
case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ 0 = 0

case neg.right.hnc
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ ¬i = n
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
this : (coeff n) (φ * ψ) = ∑ p ∈ antidiagonal n, 0
⊢ (coeff n) (φ * ψ) = 0

Tactic:
by rw [this, Finset.sum_const_zero]

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

Goal state before:
pp: R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
⊢ Summable fun x ↦ ∏ i ∈ x, f i

Tactic:
rcases isEmpty_or_nonempty ι with hempty | hempty
  · apply Summable.of_finite
  refine (summable_iff_summable_coeff _).mpr fun n ↦ summable_of_hasFiniteSupport ?_
  simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, eventually_atTop] at h
  obtain ⟨i, hi⟩ := h n
  apply (Finset.Iio i).powerset.finite_toSet.subset
  suffices ∀ s : Finset ι, coeff n (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa
  intro s hs
  contrapose hs
  obtain ⟨x, hxs, hxi⟩ := Set.not_subset.mp hs
  rw [Set.mem_Iio, not_lt] at hxi
  refine coeff_of_lt_order _ <| (hi x hxi).trans_le <| le_trans ?_ (le_order_prod _ _)
  apply Finset.single_le_sum (by simp) hxs

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

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
k : ℕ
hk : k < n
⊢ f k = g k

Tactic:
apply of_not_not

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := ⋯
k : ℕ
hk : k < n
⊢ ¬¬f k = g k
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ constantCoeff (subst a f) = 0

Tactic:
rw [constantCoeff_subst ha, finsum_eq_zero_of_forall_eq_zero]
  intro d
  by_cases hd : d = 0
  · simp [hd, hf]
  · have : constantCoeff (d.prod fun s e ↦ a s ^ e) = 0 := by
      obtain ⟨i, hi⟩ : ∃ i : σ, d i ≠ 0 := by
        by_contra! hc
        exact hd <| Finsupp.ext hc
      simpa [map_finsuppProd, ha'] using!
        Finset.prod_eq_zero (i := i) (by simp [hi]) (by simp [zero_pow hi])
    rw [this, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: ⊢ Cardinal.lift.{u, 0} ↑(finrank ℝ ℂ) = 2

Tactic:
finrank_real_complex,

Goal state after:
⊢ Cardinal.lift.{u, 0} ↑2 = 2
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
i j : ℕ
hk : (q ^ i, q ^ j) ∈ n.divisorsAntidiagonal
hab : (q ^ i, q ^ j).1 * (q ^ i, q ^ j).2 = n
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i, q ^ j).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ i, q ^ j).2 =
    0

Tactic:
rw [← pow_add] at hab

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
i j : ℕ
hk : (q ^ i, q ^ j) ∈ n.divisorsAntidiagonal
hab : q ^ (i + j) = n
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (q ^ i, q ^ j).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (q ^ i, q ^ j).2 =
    0
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f : PowerSeries R
hq : 1 < q
⊢ ((ofPowerSeries q) f) 1 = PowerSeries.constantCoeff f

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f : PowerSeries R
hq : ¬1 < q
⊢ ((ofPowerSeries q) f) 1 = PowerSeries.constantCoeff f

Tactic:
· rw [← pow_zero q, ofPowerSeries_apply_pow hq, PowerSeries.coeff_zero_eq_constantCoeff]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f : PowerSeries R
hq : ¬1 < q
⊢ ((ofPowerSeries q) f) 1 = PowerSeries.constantCoeff f
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ CompleteSpace (ArithmeticFunction R)

Tactic:
by
  let : UniformSpace R := ⊥
  apply IsUniformInducing.completeSpace ⟨rfl⟩
  apply IsClosed.isComplete
  have : Set.range ((↑) : ArithmeticFunction R → (ℕ → R)) = {f | f 0 = 0} := by
    ext f
    exact ⟨by rintro ⟨f, rfl⟩; simp, fun hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩
  rw [ArithmeticFunction.range_coe]
  apply isClosed_setOfPred_map_zero

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ

Tactic:
by
  refine le_antisymm ?_ (le_egauge_smul_left _ _ _)
  rw [ENNReal.le_div_iff_mul_le (by simp [*]) (by simp)]
  calc
    egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ := by
      rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
    _ ≤ egauge 𝕜 (c⁻¹ • c • s) x := le_egauge_smul_left _ _ _
    _ = egauge 𝕜 s x := by rw [inv_smul_smul₀ hc]

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
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
⊢ egauge 𝕜 s (c • x) ≤ ‖c‖ₑ * egauge 𝕜 s x

Tactic:
rw [mul_comm, ← ENNReal.div_le_iff_le_mul (.inl <| by simpa) (.inl enorm_ne_top),
      ENNReal.div_eq_inv_mul, ← enorm_inv (by simpa)]
    refine (le_egauge_smul_right _ _ _).trans_eq ?_
    rw [inv_smul_smul₀ hc]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (n.prod fun s m ↦ a s ^ m) * (coeff n) f = (coeff n) f * (coeff n) (n.prod fun s e ↦ (a s • X s) ^ e)

pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ n → (coeff b) f * (coeff n) (b.prod fun s e ↦ (a s • X s) ^ e) = 0

pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ n ∉ ⋯.toFinset → (coeff n) f * (coeff n) (n.prod fun s e ↦ (a s • X s) ^ e) = 0

Tactic:
· simp [mul_comm, ← monomial_eq]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ n → (coeff b) f * (coeff n) (b.prod fun s e ↦ (a s • X s) ^ e) = 0

σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ n ∉ ⋯.toFinset → (coeff n) f * (coeff n) (n.prod fun s e ↦ (a s • X s) ^ e) = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
inst✝ : Invertible ((coeff 1) P)
⊢ constantCoeff P.substInv = 0

Tactic:
by
  simp [substInv, substInvFun]

Goal state after: