internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.Quotient.OfSurjective.isDPMorphism
Proof state before:
case left
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ Ideal.map f I ≤ Ideal.map f I

case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ ∀ (n : ℕ), ∀ a ∈ I, (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)
Tactic:
exact le_refl (Ideal.map f I)
Proof state after:
case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ ∀ (n : ℕ), ∀ a ∈ I, (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)
Theorem: DividedPowers.Quotient.OfSurjective.isDPMorphism
Proof state before:
case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ ∀ (n : ℕ), ∀ a ∈ I, (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)
Tactic:
intro n a ha
Proof state after:
case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)
Theorem: DividedPowers.Quotient.OfSurjective.isDPMorphism
Proof state before:
case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)
Tactic:
rw [dpow_apply hI hf hIf ha]
Proof state after:
no goals
Theorem: DividedPowers.Quotient.OfSurjective.unique
Proof state before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers (Ideal.map f I)
hm : hI.isDPMorphism hquot f
n : ℕ
x : B
hx : x ∈ Ideal.map f I
⊢ hquot.dpow n x = (dividedPowers hI hf hIf).dpow n x
Tactic:
obtain ⟨a, ha, rfl⟩ := (Ideal.mem_map_iff_of_surjective f hf).mp hx
Proof state after:
case intro.intro
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers (Ideal.map f I)
hm : hI.isDPMorphism hquot f
n : ℕ
a : A
ha : a ∈ I
hx : f a ∈ Ideal.map f I
⊢ hquot.dpow n (f a) = (dividedPowers hI hf hIf).dpow n (f a)
Theorem: DividedPowers.Quotient.OfSurjective.unique
Proof state before:
case intro.intro
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers (Ideal.map f I)
hm : hI.isDPMorphism hquot f
n : ℕ
a : A
ha : a ∈ I
hx : f a ∈ Ideal.map f I
⊢ hquot.dpow n (f a) = (dividedPowers hI hf hIf).dpow n (f a)
Tactic:
rw [hm.2 n a ha, dpow_apply hI hf hIf ha]
Proof state after:
no goals
Theorem: DividedPowers.Quotient.isSubDPIdeal_aux
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
⊢ hI.isSubDPIdeal (RingHom.ker (Ideal.Quotient.mk J) ⊓ I)
Tactic:
simpa [Ideal.mk_ker] using hIJ
Proof state after:
no goals
Theorem: mchoose_zero
Proof state before:
n : ℕ
⊢ mchoose 0 n = 1
Tactic:
rw [mchoose, Finset.range_zero, Finset.prod_empty]
Proof state after:
no goals
Theorem: mchoose_zero'
Proof state before:
m : ℕ
⊢ mchoose m 0 = 1
Tactic:
simp only [mchoose, MulZeroClass.mul_zero, Nat.choose_self, Finset.prod_const_one]
Proof state after:
no goals
Theorem: mchoose_succ
Proof state before:
m n : ℕ
⊢ mchoose (m + 1) n = (m * n + n - 1).choose (n - 1) * mchoose m n
Tactic:
simp only [mchoose, Finset.prod_range_succ, mul_comm]
Proof state after:
no goals
Theorem: mchoose_one
Proof state before:
n : ℕ
⊢ mchoose 1 n = 1
Tactic:
simp only [mchoose, Finset.range_one, Finset.prod_singleton, zero_mul,
  zero_add, Nat.choose_self]
Proof state after:
no goals
Theorem: mchoose_one'
Proof state before:
m : ℕ
⊢ mchoose m 1 = 1
Tactic:
simp only [mchoose, mul_one, add_tsub_cancel_right, ge_iff_le, le_refl,
  tsub_eq_zero_of_le, Nat.choose_zero_right, Finset.prod_const_one]
Proof state after:
no goals
Theorem: mchoose_lemma
Proof state before:
m n : ℕ
hn : n ≠ 0
⊢ m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
Tactic:
rw [← zero_lt_iff] at hn
Proof state after:
m n : ℕ
hn : 0 < n
⊢ m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
Theorem: mchoose_lemma
Proof state before:
m n : ℕ
hn : 0 < n
⊢ m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
Tactic:
induction' m  with m ih
Proof state after:
case zero
n : ℕ
hn : 0 < n
⊢ Nat.factorial 0 * n.factorial ^ 0 * mchoose 0 n = (0 * n).factorial

case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
⊢ (m + 1).factorial * n.factorial ^ (m + 1) * mchoose (m + 1) n = ((m + 1) * n).factorial
Theorem: mchoose_lemma
Proof state before:
case zero
n : ℕ
hn : 0 < n
⊢ Nat.factorial 0 * n.factorial ^ 0 * mchoose 0 n = (0 * n).factorial
Tactic:
rw [mchoose_zero, mul_one, MulZeroClass.zero_mul, Nat.factorial_zero, pow_zero, mul_one]
Proof state after:
no goals
Theorem: mchoose_lemma
Proof state before:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
⊢ (m + 1).factorial * n.factorial ^ (m + 1) * mchoose (m + 1) n = ((m + 1) * n).factorial
Tactic:
have hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n :=
  by
  rw [←
    mul_left_inj' (Nat.mul_ne_zero (Nat.factorial_ne_zero (m * n)) (Nat.factorial_ne_zero n)), ←
    mul_assoc, ← mul_assoc, Nat.add_choose_mul_factorial_mul_factorial, ←
    Nat.mul_factorial_pred hn, mul_comm n _, ← mul_assoc, Nat.add_sub_assoc hn (m * n),
    mul_comm, mul_assoc ((m + 1) * (m * n + (n - 1)).choose (n - 1)), mul_assoc (m + 1), ←
    mul_assoc ((m * n + (n - 1)).choose (n - 1)), Nat.add_choose_mul_factorial_mul_factorial, ←
    Nat.mul_factorial_pred (Nat.add_pos_right _ hn), ← Nat.add_sub_assoc hn (m * n)]
  ring
Proof state after:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1).factorial * n.factorial ^ (m + 1) * mchoose (m + 1) n = ((m + 1) * n).factorial
Theorem: mchoose_lemma
Proof state before:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1).factorial * n.factorial ^ (m + 1) * mchoose (m + 1) n = ((m + 1) * n).factorial
Tactic:
rw [mchoose_succ, Nat.factorial_succ, pow_succ, ← mul_assoc]
Proof state after:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    ((m + 1) * n).factorial
Theorem: mchoose_lemma
Proof state before:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    ((m + 1) * n).factorial
Tactic:
conv_rhs => rw [Nat.succ_mul]
Proof state after:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    (m * n + n).factorial
Theorem: mchoose_lemma
Proof state before:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    (m * n + n).factorial
Tactic:
rw [← Nat.add_choose_mul_factorial_mul_factorial, ← ih, ← hmn]
Proof state after:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    (m + 1) * (m * n + n - 1).choose (n - 1) * (m.factorial * n.factorial ^ m * mchoose m n) * n.factorial
Theorem: mchoose_lemma
Proof state before:
case add_one
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
hmn : (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
⊢ (m + 1) * m.factorial * (n.factorial ^ m * n.factorial) * (m * n + n - 1).choose (n - 1) * mchoose m n =
    (m + 1) * (m * n + n - 1).choose (n - 1) * (m.factorial * n.factorial ^ m * mchoose m n) * n.factorial
Tactic:
ring_nf
Proof state after:
no goals
Theorem: mchoose_lemma
Proof state before:
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
⊢ (m + 1) * (m * n + n - 1).choose (n - 1) = (m * n + n).choose n
Tactic:
rw [←
  mul_left_inj' (Nat.mul_ne_zero (Nat.factorial_ne_zero (m * n)) (Nat.factorial_ne_zero n)), ←
  mul_assoc, ← mul_assoc, Nat.add_choose_mul_factorial_mul_factorial, ←
  Nat.mul_factorial_pred hn, mul_comm n _, ← mul_assoc, Nat.add_sub_assoc hn (m * n),
  mul_comm, mul_assoc ((m + 1) * (m * n + (n - 1)).choose (n - 1)), mul_assoc (m + 1), ←
  mul_assoc ((m * n + (n - 1)).choose (n - 1)), Nat.add_choose_mul_factorial_mul_factorial, ←
  Nat.mul_factorial_pred (Nat.add_pos_right _ hn), ← Nat.add_sub_assoc hn (m * n)]
Proof state after:
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
⊢ n * ((m + 1) * (m * n + n - Nat.succ 0).factorial) = (m * n + n) * (m * n + n - 1).factorial
Theorem: mchoose_lemma
Proof state before:
n : ℕ
hn : 0 < n
m : ℕ
ih : m.factorial * n.factorial ^ m * mchoose m n = (m * n).factorial
⊢ n * ((m + 1) * (m * n + n - Nat.succ 0).factorial) = (m * n + n) * (m * n + n - 1).factorial
Tactic:
ring
Proof state after:
no goals
Theorem: DirectSum.mk_apply_of_mem
Proof state before:
ι : Type v
inst✝¹ : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∈ s
⊢ ((mk β s) f) n = f ⟨n, hn⟩
Tactic:
dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]
Proof state after:
ι : Type v
inst✝¹ : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∈ s
⊢ (if H : n ∈ s then f ⟨n, H⟩ else 0) = f ⟨n, hn⟩
Theorem: DirectSum.mk_apply_of_mem
Proof state before:
ι : Type v
inst✝¹ : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∈ s
⊢ (if H : n ∈ s then f ⟨n, H⟩ else 0) = f ⟨n, hn⟩
Tactic:
rw [dif_pos hn]
Proof state after:
no goals
Theorem: DirectSum.mk_apply_of_not_mem
Proof state before:
ι : Type v
inst✝¹ : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∉ s
⊢ ((mk β s) f) n = 0
Tactic:
dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]
Proof state after:
ι : Type v
inst✝¹ : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∉ s
⊢ (if H : n ∈ s then f ⟨n, H⟩ else 0) = 0
Theorem: DirectSum.mk_apply_of_not_mem
Proof state before:
ι : Type v
inst✝¹ : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∉ s
⊢ (if H : n ∈ s then f ⟨n, H⟩ else 0) = 0
Tactic:
rw [dif_neg hn]
Proof state after:
no goals
Theorem: DirectSum.coeAddMonoidHom_eq_dfinsupp_sum
Proof state before:
ι : Type v
inst✝⁴ : DecidableEq ι
M✝ : Type w
inst✝³ : DecidableEq M✝
inst✝² : AddCommMonoid M✝
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
⊢ (DirectSum.coeAddMonoidHom A) x = DFinsupp.sum x fun i x => ↑x
Tactic:
simp only [DirectSum.coeAddMonoidHom, DirectSum.toAddMonoid,
  DFinsupp.liftAddHom, AddEquiv.coe_mk, Equiv.coe_fn_mk]
Proof state after:
ι : Type v
inst✝⁴ : DecidableEq ι
M✝ : Type w
inst✝³ : DecidableEq M✝
inst✝² : AddCommMonoid M✝
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => AddSubmonoidClass.subtype (A i)) x = DFinsupp.sum x fun i x => ↑x
Theorem: DirectSum.coeAddMonoidHom_eq_dfinsupp_sum
Proof state before:
ι : Type v
inst✝⁴ : DecidableEq ι
M✝ : Type w
inst✝³ : DecidableEq M✝
inst✝² : AddCommMonoid M✝
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => AddSubmonoidClass.subtype (A i)) x = DFinsupp.sum x fun i x => ↑x
Tactic:
exact DFinsupp.sumAddHom_apply _ x
Proof state after:
no goals
Theorem: DirectSum.coeLinearMap_eq_dfinsupp_sum
Proof state before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u
inst✝¹ : Semiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (coeLinearMap A) x = DFinsupp.sum x fun i x => ↑x
Tactic:
simp only [coeLinearMap, toModule, DFinsupp.lsum, LinearEquiv.coe_mk, LinearMap.coe_mk,
  AddHom.coe_mk]
Proof state after:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u
inst✝¹ : Semiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => (A i).subtype.toAddMonoidHom) x = DFinsupp.sum x fun i x => ↑x
Theorem: DirectSum.coeLinearMap_eq_dfinsupp_sum
Proof state before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u
inst✝¹ : Semiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => (A i).subtype.toAddMonoidHom) x = DFinsupp.sum x fun i x => ↑x
Tactic:
rw [DFinsupp.sumAddHom_apply]
Proof state after:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u
inst✝¹ : Semiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sum x fun x => ⇑(A x).subtype.toAddMonoidHom) = DFinsupp.sum x fun i x => ↑x
Theorem: DirectSum.coeLinearMap_eq_dfinsupp_sum
Proof state before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u
inst✝¹ : Semiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sum x fun x => ⇑(A x).subtype.toAddMonoidHom) = DFinsupp.sum x fun i x => ↑x
Tactic:
simp only [LinearMap.toAddMonoidHom_coe, Submodule.coeSubtype]
Proof state after:
no goals
Theorem: DirectSum.support_subset
Proof state before:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
⊢ (Function.support fun i => ↑(x i)) ⊆ ↑(DFinsupp.support x)
Tactic:
intro m
Proof state after:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ (m ∈ Function.support fun i => ↑(x i)) → m ∈ ↑(DFinsupp.support x)
Theorem: DirectSum.support_subset
Proof state before:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ (m ∈ Function.support fun i => ↑(x i)) → m ∈ ↑(DFinsupp.support x)
Tactic:
rw [Function.mem_support, Finset.mem_coe, DFinsupp.mem_support_toFun, not_imp_not]
Proof state after:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ x m = 0 → ↑(x m) = 0
Theorem: DirectSum.support_subset
Proof state before:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ x m = 0 → ↑(x m) = 0
Tactic:
intro hm'
Proof state after:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
hm' : x m = 0
⊢ ↑(x m) = 0
Theorem: DirectSum.support_subset
Proof state before:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
hm' : x m = 0
⊢ ↑(x m) = 0
Tactic:
rw [hm', AddSubmonoid.coe_zero]
Proof state after:
no goals
Theorem: DirectSum.support_subset_submodule
Proof state before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
⊢ (Function.support fun i => ↑(x i)) ⊆ ↑(DFinsupp.support x)
Tactic:
intro m
Proof state after:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ (m ∈ Function.support fun i => ↑(x i)) → m ∈ ↑(DFinsupp.support x)
Theorem: DirectSum.support_subset_submodule
Proof state before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ (m ∈ Function.support fun i => ↑(x i)) → m ∈ ↑(DFinsupp.support x)
Tactic:
rw [Function.mem_support, Finset.mem_coe, DFinsupp.mem_support_toFun, not_imp_not]
Proof state after:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ x m = 0 → ↑(x m) = 0
Theorem: DirectSum.support_subset_submodule
Proof state before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ x m = 0 → ↑(x m) = 0
Tactic:
intro hm'
Proof state after:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
m : ι
hm' : x m = 0
⊢ ↑(x m) = 0
Theorem: DirectSum.support_subset_submodule
Proof state before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
m : ι
hm' : x m = 0
⊢ ↑(x m) = 0
Tactic:
simp only [hm', Submodule.coe_zero]
Proof state after:
no goals
Theorem: LinearMap.map_finsum
Proof state before:
α : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module S N
f : α → M
g : M →ₛₗ[σ] N
hf : (Function.support f).Finite
⊢ g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)
Tactic:
rw [← LinearMap.toAddMonoidHom_coe]
Proof state after:
α : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module S N
f : α → M
g : M →ₛₗ[σ] N
hf : (Function.support f).Finite
⊢ g.toAddMonoidHom (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g.toAddMonoidHom (f i)
Theorem: LinearMap.map_finsum
Proof state before:
α : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
σ : R →+* S
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module S N
f : α → M
g : M →ₛₗ[σ] N
hf : (Function.support f).Finite
⊢ g.toAddMonoidHom (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g.toAddMonoidHom (f i)
Tactic:
exact AddMonoidHom.map_finsum _ hf
Proof state after:
no goals
Theorem: TensorProduct.congr'_coe
Proof state before:
R : Type u
M : Type v
N : Type w
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
S : Type u_1
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
P : Type u_2
inst✝³ : AddCommMonoid P
inst✝² : Module R P
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
e : M ≃ₗ[S] N
f : P ≃ₗ[R] Q
⊢ ⇑(congr' e f) = ⇑(congr (LinearEquiv.restrictScalars R e) f)
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.mem_basis
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f ∈ basis σ α d ↔ ∀ e ≤ d, (coeff α e) f = 0
Tactic:
simp only [basis, Submodule.mem_mk, AddSubmonoid.mem_mk, Set.mem_setOf_eq]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f ∈ { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ↔ ∀ e ≤ d, (coeff α e) f = 0
Theorem: MvPowerSeries.mem_basis
Proof state before:
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f ∈ { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ↔ ∀ e ≤ d, (coeff α e) f = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.basis_le_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
⊢ basis σ α d ≤ basis σ α e ↔ e ≤ d
Tactic:
refine' ⟨_, basis_le _ _⟩
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : CommRing α
inst✝ : Nontrivial α
d e : σ →₀ ℕ
⊢ basis σ α d ≤ basis σ α e → e ≤ d
Theorem: MvPowerSeries.basis_le_iff
Proof 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]
Proof 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
Theorem: MvPowerSeries.basis_le_iff
Proof 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
Proof 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
Theorem: MvPowerSeries.basis_le_iff
Proof 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]
Proof 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