internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ r = 0 → (algebraMap R (DividedPowerAlgebra R M)) r = 0
Tactic:
intro hr
Proof state after:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
hr : r = 0
⊢ (algebraMap R (DividedPowerAlgebra R M)) r = 0
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
hr : r = 0
⊢ (algebraMap R (DividedPowerAlgebra R M)) r = 0
Tactic:
rw [hr, map_zero]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Codisjoint (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (augIdeal R M))
Tactic:
rw [codisjoint_iff, eq_top_iff]
Proof state after:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ⊤ ≤ Subalgebra.toSubmodule ⊥ ⊔ Submodule.restrictScalars R (augIdeal R M)
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ⊤ ≤ Subalgebra.toSubmodule ⊥ ⊔ Submodule.restrictScalars R (augIdeal R M)
Tactic:
intro p _
Proof state after:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ p ∈ Subalgebra.toSubmodule ⊥ ⊔ Submodule.restrictScalars R (augIdeal R M)
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ p ∈ Subalgebra.toSubmodule ⊥ ⊔ Submodule.restrictScalars R (augIdeal R M)
Tactic:
simp only [Submodule.mem_sup, Subalgebra.mem_toSubmodule, Submodule.restrictScalars_mem]
Proof state after:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ ∃ y ∈ ⊥, ∃ z ∈ augIdeal R M, y + z = p
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ ∃ y ∈ ⊥, ∃ z ∈ augIdeal R M, y + z = p
Tactic:
refine ⟨algebraMap R _ (algebraMapInv R M p), ?_, _, ?_, add_sub_cancel _ p⟩
Proof state after:
case codisjoint.refine_1
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ ⊥

case codisjoint.refine_2
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ p - (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ augIdeal R M
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case codisjoint.refine_1
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ ⊥
Tactic:
rw [Algebra.mem_bot]
Proof state after:
case codisjoint.refine_1
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M))
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case codisjoint.refine_1
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M))
Tactic:
exact Set.mem_range_self ((algebraMapInv R M) p)
Proof state after:
no goals
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case codisjoint.refine_2
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
a✝ : p ∈ ⊤
⊢ p - (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p) ∈ augIdeal R M
Tactic:
simp only [mem_augIdeal_iff, map_sub, AlgHom.commutes, Algebra.id.map_eq_id,
RingHom.id_apply, sub_self]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_truncFun'
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m (truncFun' n φ) = if m ≤ n then (coeff R m) φ else 0
Tactic:
classical
simp [truncFun', MvPolynomial.coeff_sum]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_truncFun'
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m (truncFun' n φ) = if m ≤ n then (coeff R m) φ else 0
Tactic:
simp [truncFun', MvPolynomial.coeff_sum]
Proof state after:
no goals
Theorem: MvPowerSeries.trunc_one'
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) 1) = MvPolynomial.coeff m 1
Tactic:
rw [coeff_trunc', coeff_one]
Proof state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then 1 else 0 else 0) = MvPolynomial.coeff m 1
Theorem: MvPowerSeries.trunc_one'
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then 1 else 0 else 0) = MvPolynomial.coeff m 1
Tactic:
split_ifs with H H'
Proof state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : m = 0
⊢ 1 = MvPolynomial.coeff m 1

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ 0 = MvPolynomial.coeff m 1

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ 0 = MvPolynomial.coeff m 1
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : m = 0
⊢ 1 = MvPolynomial.coeff m 1
Tactic:
subst m
Proof state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : 0 ≤ n
⊢ 1 = MvPolynomial.coeff 0 1
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : 0 ≤ n
⊢ 1 = MvPolynomial.coeff 0 1
Tactic:
simp
Proof state after:
no goals
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ 0 = MvPolynomial.coeff m 1
Tactic:
symm
Proof state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ MvPolynomial.coeff m 1 = 0
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ MvPolynomial.coeff m 1 = 0
Tactic:
rw [MvPolynomial.coeff_one]
Proof state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ (if 0 = m then 1 else 0) = 0
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ (if 0 = m then 1 else 0) = 0
Tactic:
exact if_neg (Ne.symm H')
Proof state after:
no goals
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ 0 = MvPolynomial.coeff m 1
Tactic:
symm
Proof state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ MvPolynomial.coeff m 1 = 0
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ MvPolynomial.coeff m 1 = 0
Tactic:
rw [MvPolynomial.coeff_one]
Proof state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ (if 0 = m then 1 else 0) = 0
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ (if 0 = m then 1 else 0) = 0
Tactic:
refine' if_neg _
Proof state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ ¬0 = m
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ ¬0 = m
Tactic:
rintro rfl
Proof state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : ¬0 ≤ n
⊢ False
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : ¬0 ≤ n
⊢ False
Tactic:
apply H
Proof state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : ¬0 ≤ n
⊢ 0 ≤ n
Theorem: MvPowerSeries.trunc_one'
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : ¬0 ≤ n
⊢ 0 ≤ n
Tactic:
exact orderBot.proof_1 n
Proof state after:
no goals
Theorem: MvPowerSeries.trunc_c
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) ((C σ R) a)) = MvPolynomial.coeff m (MvPolynomial.C a)
Tactic:
classical
rw [coeff_trunc', coeff_C, MvPolynomial.coeff_C]
split_ifs with H <;> first |rfl|try simp_all
exfalso; apply H; subst m; exact orderBot.proof_1 n
Proof state after:
no goals
Theorem: MvPowerSeries.trunc_c
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) ((C σ R) a)) = MvPolynomial.coeff m (MvPolynomial.C a)
Tactic:
rw [coeff_trunc', coeff_C, MvPolynomial.coeff_C]
Proof state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then a else 0 else 0) = if 0 = m then a else 0
Theorem: MvPowerSeries.trunc_c
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then a else 0 else 0) = if 0 = m then a else 0
Tactic:
split_ifs with H <;> first |rfl|try simp_all
Proof state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ 0 = a
Theorem: MvPowerSeries.trunc_c
Proof state before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ 0 = a
Tactic:
exfalso
Proof state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ False
Theorem: MvPowerSeries.trunc_c
Proof state before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ False
Tactic:
apply H
Proof state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ m ≤ n
Theorem: MvPowerSeries.trunc_c
Proof state before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ m ≤ n
Tactic:
subst m
Proof state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
H : ¬0 ≤ n
⊢ 0 ≤ n
Theorem: MvPowerSeries.trunc_c
Proof state before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
H : ¬0 ≤ n
⊢ 0 ≤ n
Tactic:
exact orderBot.proof_1 n
Proof state after:
no goals
Theorem: MvPowerSeries.trunc_c
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : ¬0 = m
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.trunc_c
Proof state before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : m ≤ n
h✝¹ : ¬m = 0
h✝ : 0 = m
⊢ 0 = a
Tactic:
try simp_all
Proof state after:
no goals
Theorem: MvPowerSeries.trunc_c
Proof state before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : m ≤ n
h✝¹ : ¬m = 0
h✝ : 0 = m
⊢ 0 = a
Tactic:
simp_all
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_mul_trunc'
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ MvPolynomial.coeff m ((trunc' R n) f * (trunc' R n) g) = (coeff R m) (f * g)
Tactic:
classical
simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
apply Finset.sum_congr rfl
rintro ⟨i, j⟩ hij
simp only [mem_antidiagonal] at hij
rw [← hij] at h
simp only
apply congr_arg₂
rw [coeff_trunc', if_pos (le_trans le_self_add h)]
rw [coeff_trunc', if_pos (le_trans le_add_self h)]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_mul_trunc'
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ MvPolynomial.coeff m ((trunc' R n) f * (trunc' R n) g) = (coeff R m) (f * g)
Tactic:
simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
Proof state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∑ x ∈ antidiagonal m, MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g) =
    ∑ p ∈ antidiagonal m, (coeff R p.1) f * (coeff R p.2) g
Theorem: MvPowerSeries.coeff_mul_trunc'
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∑ x ∈ antidiagonal m, MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g) =
    ∑ p ∈ antidiagonal m, (coeff R p.1) f * (coeff R p.2) g
Tactic:
apply Finset.sum_congr rfl
Proof state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∀ x ∈ antidiagonal m,
    MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g) =
      (coeff R x.1) f * (coeff R x.2) g
Theorem: MvPowerSeries.coeff_mul_trunc'
Proof state before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
⊢ ∀ x ∈ antidiagonal m,
    MvPolynomial.coeff x.1 ((trunc' R n) f) * MvPolynomial.coeff x.2 ((trunc' R n) g) =
      (coeff R x.1) f * (coeff R x.2) g
Tactic:
rintro ⟨i, j⟩ hij
Proof state after:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g
Theorem: MvPowerSeries.coeff_mul_trunc'
Proof state before:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g
Tactic:
simp only [mem_antidiagonal] at hij
Proof state after:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : i + j = m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g
Theorem: MvPowerSeries.coeff_mul_trunc'
Proof state before:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m : σ →₀ ℕ
h : m ≤ n
i j : σ →₀ ℕ
hij : i + j = m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g
Tactic:
rw [← hij] at h
Proof state after:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g
Theorem: MvPowerSeries.coeff_mul_trunc'
Proof state before:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff (i, j).1 ((trunc' R n) f) * MvPolynomial.coeff (i, j).2 ((trunc' R n) g) =
    (coeff R (i, j).1) f * (coeff R (i, j).2) g
Tactic:
simp only
Proof state after:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff i ((trunc' R n) f) * MvPolynomial.coeff j ((trunc' R n) g) = (coeff R i) f * (coeff R j) g
Theorem: MvPowerSeries.coeff_mul_trunc'
Proof state before:
case mk
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff i ((trunc' R n) f) * MvPolynomial.coeff j ((trunc' R n) g) = (coeff R i) f * (coeff R j) g
Tactic:
apply congr_arg₂
Proof state after:
case mk.hx
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff i ((trunc' R n) f) = (coeff R i) f

case mk.hy
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff j ((trunc' R n) g) = (coeff R j) g
Theorem: MvPowerSeries.coeff_mul_trunc'
Proof state before:
case mk.hx
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff i ((trunc' R n) f) = (coeff R i) f

case mk.hy
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff j ((trunc' R n) g) = (coeff R j) g
Tactic:
rw [coeff_trunc', if_pos (le_trans le_self_add h)]
Proof state after:
case mk.hy
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff j ((trunc' R n) g) = (coeff R j) g
Theorem: MvPowerSeries.coeff_mul_trunc'
Proof state before:
case mk.hy
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
f g : MvPowerSeries σ R
m i j : σ →₀ ℕ
h : i + j ≤ n
hij : i + j = m
⊢ MvPolynomial.coeff j ((trunc' R n) g) = (coeff R j) g
Tactic:
rw [coeff_trunc', if_pos (le_trans le_add_self h)]
Proof state after:
no goals
Theorem: MvPowerSeries.continuous_trunc'
Proof state before:
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n : σ →₀ ℕ
⊢ Continuous ⇑(trunc' R n)
Tactic:
rw [continuous_induced_rng]
Proof state after:
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n : σ →₀ ℕ
⊢ Continuous (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n))
Theorem: MvPowerSeries.continuous_trunc'
Proof state before:
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n : σ →₀ ℕ
⊢ Continuous (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n))
Tactic:
apply continuous_pi
Proof state after:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n : σ →₀ ℕ
⊢ ∀ (i : σ →₀ ℕ), Continuous fun a => (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n)) a i
Theorem: MvPowerSeries.continuous_trunc'
Proof state before:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n : σ →₀ ℕ
⊢ ∀ (i : σ →₀ ℕ), Continuous fun a => (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n)) a i
Tactic:
intro m
Proof state after:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
⊢ Continuous fun a => (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n)) a m
Theorem: MvPowerSeries.continuous_trunc'
Proof state before:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
⊢ Continuous fun a => (MvPolynomial.toMvPowerSeries ∘ ⇑(trunc' R n)) a m
Tactic:
simp only [Function.comp_apply, MvPolynomial.coe_def, coeff_trunc']
Proof state after:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
⊢ Continuous fun a => if m ≤ n then (coeff R m) a else 0
Theorem: MvPowerSeries.continuous_trunc'
Proof state before:
case h
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
⊢ Continuous fun a => if m ≤ n then (coeff R m) a else 0
Tactic:
split_ifs with h
Proof state after:
case pos
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
h : m ≤ n
⊢ Continuous fun a => (coeff R m) a

case neg
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
h : ¬m ≤ n
⊢ Continuous fun a => 0
Theorem: MvPowerSeries.continuous_trunc'
Proof state before:
case pos
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
h : m ≤ n
⊢ Continuous fun a => (coeff R m) a
Tactic:
exact continuous_apply m
Proof state after:
no goals
Theorem: MvPowerSeries.continuous_trunc'
Proof state before:
case neg
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n✝ : σ →₀ ℕ
inst✝² inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
n m : σ →₀ ℕ
h : ¬m ≤ n
⊢ Continuous fun a => 0
Tactic:
exact continuous_const
Proof state after:
no goals
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
⊢ hJ.isDPMorphism hK g → hI.isDPMorphism hJ f → hI.isDPMorphism hK h
Tactic:
intro hg hf
Proof state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ hI.isDPMorphism hK h