mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, x + y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x - y, y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 * ∑ i ∈ range (m + 1), (2 * m + 1).choose i =
    ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, y - x} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, x - y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {y - x, y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
x : α
inst✝ : LinearOrder α
⊢ span {|x|} = span {x}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ m + 1 ≤ 2 * m + 1 + 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
⊢ y ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
x : α
s : Set α
inst✝ : LinearOrder α
⊢ span (insert |x| s) = span (insert x s)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
x y : α
inst✝ : LinearOrder α
⊢ span {x, |y|} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) =
    ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : α
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ m + 1 ≤ 2 * m + 2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : α
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} < span {y} ↔ DvdNotUnit y x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x + y * z, y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y + x * z} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 ^ (2 * m + 1) = 2 * 4 ^ m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {y * z + x, y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
⊢ I ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, x * z + y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n x : ℕ
x✝ : x ∈ range (n + 1)
⊢ 0 ≤ (2 * n + 1).choose x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x + z * y, y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y + z * x} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {z * y + x, y} = span {x, y}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r : (i : ι) → R i
⊢ (pi fun x ↦ span {r x}) = span {r}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ (2 * n + 1).choose n ≤ 4 ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ 4 ^ n = (1 + 1) ^ (2 * n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, z * x + y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ (1 + 1) ^ (2 * n) = ∑ m ∈ range (2 * n + 1), (2 * n).choose m

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
inst✝ : DecidableEq ι
i : ι
r : R i
hr : r ∈ I i
⊢ Pi.single i r ∈ pi I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x - y * z, y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x - y * z, y} = span {x, y}

Tactic:
by
  rw [← span_pair_add_right_mul, sub_add_cancel]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range (2 * n + 1), (2 * n).choose m ≤ ∑ x ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I J : (i : ι) → Ideal (R i)
le : pi I ≤ pi J
i : ι
r : R i
hr : r ∈ I i
⊢ r ∈ J i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y - x * z} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2) = (2 * n + 1) * (2 * n).choose n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x - z * y, y} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n k : ℕ
h : n < k
⊢ n + 1 < k + 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y - z * x} = span {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n✝ k n : ℕ
hmn✝ : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ k ≤ n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n✝ k n : ℕ
hmn✝ : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ n + 1 ∉ Ico k (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : x ∈ (LinearMap.toSpanSingleton R R e).ker
⊢ x * (1 - e) = x

Tactic:
by

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

Goal state before:
pp: α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ (a + b) ^ k ∈ I

Tactic:
by

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

Goal state before:
pp: α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hab : Commute a b
⊢ m + n ≤ m + n - 1 + 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x ∈ (LinearMap.toSpanSingleton R R e).ker ↔ x ∈ Ideal.span {1 - e}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ (LinearMap.toSpanSingleton R R (1 - e)).ker = Ideal.span {e}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n k : ℕ
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n k : ℕ
⊢ ∑ i ∈ range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I✝ J : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
inst✝ : I.IsTwoSided
a₁ b₁ a₂ b₂ : R
h₁ : (QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid a₁ b₁
h₂ : (QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid a₂ b₂
⊢ (QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid (a₁ * a₂) (b₁ * b₂)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R✝ : Type u
inst✝¹ : Ring R✝
I✝ J : Ideal R✝
a b : R✝
S : Type v
x y : R✝
R : Type ?u.15
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a b : R ⧸ I), a * b = b * a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
a b : R
S : Type v
x y : R
inst✝ : I.IsTwoSided
⊢ (ring I).toAddCommGroup = Submodule.Quotient.addCommGroup I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x y : R
⊢ (mk I) x = (mk I) y ↔ x - y ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ (mk I) x = 1 ↔ x - 1 ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ x_1 ∈ s, x_1 - x ∈ I
a : R
a_in : a ∈ s
h : a - x ∈ I
⊢ ↑⟨-(a - x), ⋯⟩ + a = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
⊢ ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ 2 * ∑ i ∈ range (n + 1), i * n.choose i =
    ∑ i ∈ range (n + 1), (n - i) * n.choose (n - i) + ∑ i ∈ range (n + 1), i * n.choose i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ ↑(Submonoid.powers a) → a_1 ∉ ↑I

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), (n - i) * n.choose (n - i) + ∑ i ∈ range (n + 1), i * n.choose i =
    ∑ i ∈ range (n + 1), (n - i) * n.choose i + ∑ i ∈ range (n + 1), i * n.choose i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ a - x ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
⊢ ⇑(mk I) ⁻¹' ⇑(mk I) '' s = ⋃ x, (fun y ↦ ↑x + y) '' s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), (n - i) * n.choose i + ∑ i ∈ range (n + 1), i * n.choose i = ∑ i ∈ range (n + 1), n * n.choose i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), n * n.choose i = n * 2 ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(lift I f H)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ n * 2 ^ n = 2 * (n * 2 ^ (n - 1))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ range (n + 1), i * n.choose i = n * 2 ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
S : Ideal R
inst✝ : S.IsTwoSided
⊢ factor ⋯ = RingHom.id (R ⧸ S)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n k : ℕ
⊢ ∑ i ∈ range (n + 1), k.multichoose i = (n + k).choose k

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
S T : Ideal R
inst✝¹ : S.IsTwoSided
inst✝ : T.IsTwoSided
H : S ≤ T
⊢ (factor H).comp (mk S) = mk T

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
⊢ (factor H2).comp (factor H1) = factor ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R ⧸ S
⊢ (factor H2) ((factor H1) x) = (factor ⋯) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
a b : R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
⊢ ∀ (x y : R ⧸ I),
    (↑(Submodule.quotEquivOfEq I J h)).toFun (x * y) =
      (↑(Submodule.quotEquivOfEq I J h)).toFun x * (↑(Submodule.quotEquivOfEq I J h)).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n m : ℕ
⊢ ∑ k ∈ range (m + 1), (-1) ^ k * ↑((n + 1).choose k) = (-1) ^ m * ↑(n.choose m)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
⊢ (quotEquivOfEq h).symm = quotEquivOfEq ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range (n + 1), (-1) ^ m * ↑(n.choose m) = if n = 0 then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ ∑ m ∈ range (n + 1), (-1) ^ m * ↑(n.choose m) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝¹ : Ring R
f : ι → R
inst✝ : (span (range f)).IsTwoSided
i : ι
⊢ (mk (span (range f))) (f i) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a * c * (a * d) = a * (c * d) * a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝ : Ring R
I J : Ideal R
a b x y : R
⊢ ∀ (a : R ⧸ ⊤), a = default

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_5
inst✝ : CommRing R
x y : R
⊢ (mk (span {x})) y = 0 ↔ x ∣ y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y ≤ #x

Tactic:
mem_powerset

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ⊆ x
⊢ #y ≤ #x
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ IsDomain (R ⧸ I) ↔ I.IsPrime

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
⊢ (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ x.powerset, f #m = ∑ m ∈ range (#x + 1), (#x).choose m • f m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
⊢ ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b, a * b = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ Irreducible a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m ∈ x.powerset, (-1) ^ #m = if x = ∅ then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ ∑ m ∈ x.powerset, (-1) ^ #m = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsPrincipalIdealRing α
p : α
hP : α ∙ p ≠ ⊥
h : IsPrime (α ∙ p)
x✝ : p = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsPrincipalIdealRing α
P : Ideal α
hP : P ≠ ⊥
h : P.IsPrime
⊢ ∃ p, Prime p ∧ P = span {p}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsPrincipalIdealRing α
p : α
hp : Prime p
hP : span {p} ≠ ⊥
⊢ p ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsPrincipalIdealRing α
P : Ideal α
hP : P ≠ ⊥
⊢ (∃ p, Prime p ∧ P = span {p}) → P.IsPrime

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
⊢ s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
s : Finset ι
f : ι → α
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (s.card * n + 1) ∈ span ((fun i ↦ f i ^ (n + 1)) '' ↑s)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
P : Ideal α
⊢ P.IsPrime ↔ P = ⊥ ∨ ∃ p, Prime p ∧ P = span {p}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ I.IsMaximal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i =
    (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n i : ℕ
hi : i ∈ range (n + 1)
⊢ i ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map i (f.iterateMapComap i n K) ≤ map i (comap f (map f (f.iterateMapComap i n K)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map i (comap f (map f (f.iterateMapComap i n K))) ≤ map i (comap f (map i ((fun K ↦ comap f (map i K))^[n] K)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
⊢ f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
⊢ ∀ (a₁ : R) (a₂ : ι → R) (b₁ : R) (b₂ : ι → R),
    (Submodule.quotientRel I) a₁ b₁ →
      (Submodule.quotientRel (pi fun x ↦ I)) a₂ b₂ → Submodule.Quotient.mk (a₁ • a₂) = Submodule.Quotient.mk (b₁ • b₂)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
⊢ ∀ (x y : R ⧸ I) (b : (ι → R) ⧸ pi fun x ↦ I), (x * y) • b = x • y • b

Tactic:
by

Goal state after: