Theorem: MvPowerSeries.basis_le_iff (DividedPowers/ForMathlib/MvPowerSeries/LinearTopology.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
⊢ basis σ α d ≤ basis σ α e ↔ e ≤ d
Tactic:
refine' ⟨_, basis_le _ _⟩
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
⊢ basis σ α d ≤ basis σ α e → e ≤ d

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
⊢ basis σ α d ≤ basis σ α e → e ≤ d
Tactic:
simp only [basis, Submodule.mk_le_mk, AddSubmonoid.mk_le_mk, setOf_subset_setOf]
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
⊢ { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
      { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ } →
    e ≤ d

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
⊢ { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
      { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ } →
    e ≤ d
Tactic:
intro h
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d
Tactic:
rw [← inf_eq_right]
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ d ⊓ e = e

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ d ⊓ e = e
Tactic:
apply le_antisymm
State after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ d ⊓ e ≤ e

case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d ⊓ e

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ d ⊓ e ≤ e

case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d ⊓ e
Tactic:
. exact inf_le_right
State after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d ⊓ e

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d ⊓ e
Tactic:
. by_contra h'
  simp only [AddSubsemigroup.mk_le_mk, setOf_subset_setOf] at h
  specialize h (monomial α e 1) _
  . intro e' he'
    apply coeff_monomial_ne
    intro hee'
    rw [hee'] at he'
    apply h'
    exact le_inf_iff.mpr ⟨he', le_rfl⟩
  apply one_ne_zero' α
  convert h e le_rfl
  rw [coeff_monomial_same]
State after:
no goals

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ d ⊓ e ≤ e
Tactic:
exact inf_le_right
State after:
no goals

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
⊢ e ≤ d ⊓ e
Tactic:
by_contra h'
State after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
h' : ¬e ≤ d ⊓ e
⊢ False

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h :
  { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ≤
    { carrier := {f | ∀ e_1 ≤ e, (coeff α e_1) f = 0}, add_mem' := ⋯ }
h' : ¬e ≤ d ⊓ e
⊢ False
Tactic:
simp only [AddSubsemigroup.mk_le_mk, setOf_subset_setOf] at h
State after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
⊢ False

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
⊢ False
Tactic:
specialize h (monomial α e 1) _
State after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
⊢ ∀ e_1 ≤ d, (coeff α e_1) ((monomial α e) 1) = 0

case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ False

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
⊢ ∀ e_1 ≤ d, (coeff α e_1) ((monomial α e) 1) = 0

case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ False
Tactic:
. intro e' he'
  apply coeff_monomial_ne
  intro hee'
  rw [hee'] at he'
  apply h'
  exact le_inf_iff.mpr ⟨he', le_rfl⟩
State after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ False

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ False
Tactic:
apply one_ne_zero' α
State after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ 1 = 0

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ 1 = 0
Tactic:
convert h e le_rfl
State after:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ 1 = (coeff α e) ((monomial α e) 1)

State before:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ e_1 ≤ e, (coeff α e_1) ((monomial α e) 1) = 0
⊢ 1 = (coeff α e) ((monomial α e) 1)
Tactic:
rw [coeff_monomial_same]
State after:
no goals

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
⊢ ∀ e_1 ≤ d, (coeff α e_1) ((monomial α e) 1) = 0
Tactic:
intro e' he'
State after:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
⊢ (coeff α e') ((monomial α e) 1) = 0

State before:
case a
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
⊢ (coeff α e') ((monomial α e) 1) = 0
Tactic:
apply coeff_monomial_ne
State after:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
⊢ e' ≠ e

State before:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
⊢ e' ≠ e
Tactic:
intro hee'
State after:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
hee' : e' = e
⊢ False

State before:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e' ≤ d
hee' : e' = e
⊢ False
Tactic:
rw [hee'] at he'
State after:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e ≤ d
hee' : e' = e
⊢ False

State before:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e ≤ d
hee' : e' = e
⊢ False
Tactic:
apply h'
State after:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e ≤ d
hee' : e' = e
⊢ e ≤ d ⊓ e

State before:
case a.h
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
h' : ¬e ≤ d ⊓ e
h : ∀ (a : MvPowerSeries σ α), (∀ e ≤ d, (coeff α e) a = 0) → ∀ e_1 ≤ e, (coeff α e_1) a = 0
e' : σ →₀ ℕ
he' : e ≤ d
hee' : e' = e
⊢ e ≤ d ⊓ e
Tactic:
exact le_inf_iff.mpr ⟨he', le_rfl⟩
State after:
no goals