mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
a : α
f : ι → α
inst✝¹ : Nonempty ι
inst✝ : Finite ι
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
ha : a ≤ ⨆ i, f i
i : ι
hi : ∀ (i_1 : ι), f (id i_1) ≤ f i
⊢ ∃ i, a ≤ f i

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
a : α
f : ι → α
inst✝¹ : Nonempty ι
inst✝ : Finite ι
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
ha : a ≤ ⨆ i, f i
i : ι
hi : ∀ (i_1 : ι), f (id i_1) ≤ f i
⊢ ∃ i, a ≤ f i
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
a : α
f : ι → α
inst✝¹ : Nonempty ι
inst✝ : Finite ι
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
i : ι
hai : a ≤ f i
⊢ a ≤ ⨆ i, f i

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
a : α
f : ι → α
inst✝¹ : Nonempty ι
inst✝ : Finite ι
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
i : ι
hai : a ≤ f i
⊢ a ≤ ⨆ i, f i
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
h : ⇑(partialSups f) ≤ f
⊢ f = ⇑(partialSups f)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
h : ⇑(partialSups f) ≤ f
⊢ f = ⇑(partialSups f)
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : Preorder ι
inst✝² : LocallyFiniteOrderBot ι
F : Type u_4
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : ι → α
g : F
x✝ : ι
⊢ (partialSups (⇑g ∘ f)) x✝ = (⇑g ∘ ⇑(partialSups f)) x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : Preorder ι
inst✝² : LocallyFiniteOrderBot ι
F : Type u_4
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : ι → α
g : F
x✝ : ι
⊢ (partialSups (⇑g ∘ f)) x✝ = (⇑g ∘ ⇑(partialSups f)) x✝
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case refine_2
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ g (x' + x) = g y

Tactic:
simp [← eq_sub_iff_add_eq.1 H, map_add, mem_ker.mp hy']

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ ∀ (r : ℕ) (i : ι), #(Iio i) ≤ r → (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
intro r

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
r : ℕ
⊢ ∀ (i : ι), #(Iio i) ≤ r → (partialSups (disjointed f)) i = (partialSups f) i
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
r : ι
⊢ r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
r : ι
⊢ r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ Nat.find ⋯ ≤ 0

Tactic:
apply Nat.find_le

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ succ^[0] i0 = i0
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ succ^[0] i0 = i0

Tactic:
rw [Function.iterate_zero, id]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ ↑(Nat.find ⋯)

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ ↑(Nat.find ⋯)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
r : ι
⊢ r ∈ univ.biUnion Iic ↔ r ∈ univ

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
r : ι
⊢ r ∈ univ.biUnion Iic ↔ r ∈ univ
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_2
inst✝ : Monoid A
H1 H2 : HasMulAntidiagonal A
⊢ H1 = H2

Tactic:
;

Goal state after:
A : Type u_2
inst✝ : Monoid A
H1 H2 : HasMulAntidiagonal A
⊢ H1 = H2
Module: Mathlib.Order.Disjointed

Goal state before:
pp: ι : Type u_2
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
α : Type u_3
f : ι → Set α
n : ι
⊢ ⋃ i ∈ Iic n, disjointed f i = (partialSups (disjointed f)) n

Tactic:
partialSups_eq_biSup

Goal state after:
ι : Type u_2
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
α : Type u_3
f : ι → Set α
n : ι
⊢ ⋃ i ∈ Iic n, disjointed f i = ⨆ j, ⨆ (_ : j ≤ n), disjointed f j
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: δ : Type u_4
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k = ∏ k ∈ range n, f k

Tactic:
;

Goal state after:
δ : Type u_4
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k = ∏ k ∈ range n, f k
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n i✝ : ℕ
a✝ : ℕ × ℕ
⊢ (map ((fun i ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n))[i✝]? = some a✝ ↔
    (map (Prod.map Nat.succ id ∘ (fun i ↦ (i, n - i)) ∘ Nat.succ) (range n))[i✝]? = some a✝

Tactic:
;

Goal state after:
n i✝ : ℕ
a✝ : ℕ × ℕ
⊢ (map ((fun i ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n))[i✝]? = some a✝ ↔
    (map (Prod.map Nat.succ id ∘ (fun i ↦ (i, n - i)) ∘ Nat.succ) (range n))[i✝]? = some a✝
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
x✝ : ι
⊢ f x✝ = (f' ∘ ⇑R) x✝

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
x✝ : ι
⊢ f x✝ = (f' ∘ ⇑R) x✝
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ (a_1 : ℕ) (a_2 : a_1 < n),
    a_1 ≤ ↑a →
      (if ⟨a_1, ⋯⟩ ≤ a then f ⟨a_1 + 1, ⋯⟩ / f ⟨a_1, ⋯⟩ else 1) = f ⟨a_1 + 1, ⋯⟩ / if h : a_1 ≤ n then f ⟨a_1, ⋯⟩ else 1

Tactic:
;

Goal state after:
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ (a_1 : ℕ) (a_2 : a_1 < n),
    a_1 ≤ ↑a →
      (if ⟨a_1, ⋯⟩ ≤ a then f ⟨a_1 + 1, ⋯⟩ / f ⟨a_1, ⋯⟩ else 1) = f ⟨a_1 + 1, ⋯⟩ / if h : a_1 ≤ n then f ⟨a_1, ⋯⟩ else 1
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ map ({ toFun := fun i ↦ (i, n - i), inj' := ⋯ }.trans { toFun := Prod.swap, inj' := ⋯ }) (range (n + 1)) =
    map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))

Tactic:
;

Goal state after:
n : ℕ
⊢ map ({ toFun := fun i ↦ (i, n - i), inj' := ⋯ }.trans { toFun := Prod.swap, inj' := ⋯ }) (range (n + 1)) =
    map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j

Tactic:
;

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏
      p ∈
        cons (0, n + 1)
          (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) (antidiagonal n))
          ⋯,
      f p =
    f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Tactic:
prod_cons,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏
        x ∈
          map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) (antidiagonal n),
        f x =
    f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏ x ∈ antidiagonal n,
        f (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) x) =
    f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏ x ∈ antidiagonal n,
        f (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) x) =
    f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
;

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j : ℕ
⊢ (∃ b a, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type w
inst✝ : Semiring α
I : Ideal α
a b a✝ x✝ : α
h : a✝ ∈ ⊥
⊢ 0 ∈ ⊥

Tactic:
;

Goal state after:
α : Type u
β : Type v
F : Type w
inst✝ : Semiring α
I : Ideal α
a b a✝ x✝ : α
h : a✝ ∈ ⊥
⊢ 0 ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: α : Type u
inst✝ : Semiring α
⊢ 1 ∈ ⊤

Tactic:
;

Goal state after:
α : Type u
inst✝ : Semiring α
⊢ 1 ∈ ⊤
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I ≤ ⊥

Tactic:
intro r

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
⊢ r ∈ I → r ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: case pos
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : r = 0
⊢ r ∈ ⊥

pp: case neg
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : ¬r = 0
⊢ r ∈ ⊥

Tactic:
;

Goal state after:
case pos
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : r = 0
⊢ r ∈ ⊥

case neg
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : ¬r = 0
⊢ r ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
a : α
inst✝ : CommSemiring α
I : Ideal α
ha : a ∈ I
c : α
⊢ a * c ∈ I

Tactic:
;

Goal state after:
α : Type u
a : α
inst✝ : CommSemiring α
I : Ideal α
ha : a ∈ I
c : α
⊢ a * c ∈ I
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + (b * c - b * d)

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + (b * c - b * d)
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : { a // IsIdempotentElem a }
⊢ ↑aᶜᶜ = ↑a

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : { a // IsIdempotentElem a }
⊢ ↑aᶜᶜ = ↑a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑0ᶜ = ↑1

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑0ᶜ = ↑1
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑1ᶜ = ↑0

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑1ᶜ = ↑0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a ∧ b * b = b

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a ∧ b * b = b
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 = a * (x + y * z) + b * y

Tactic:
;

Goal state after:
α : 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 = a * (x + y * z) + b * y
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 = a * x + b * y

Tactic:
;

Goal state after:
α : 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 = a * x + b * y
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 ^ 2) ^ m = 2 * 4 ^ m

Tactic:
;

Goal state after:
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 ^ 2) ^ m = 2 * 4 ^ m
Module: Mathlib.RingTheory.Ideal.Basic

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

Tactic:
;

Goal state after:
ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r x✝ : (i : ι) → R i
⊢ (x✝ ∈ pi fun x ↦ span {r x}) ↔ x✝ ∈ span {r}
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case h
n m : ℕ
a✝ : m ∈ range (2 * n + 1)
⊢ (2 * n).choose m ≤ (2 * n).choose (2 * n / 2)

Tactic:
;

Goal state after:
case h
n m : ℕ
a✝ : m ∈ range (2 * n + 1)
⊢ (2 * n).choose m ≤ (2 * n).choose (2 * n / 2)
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:
simpa using le (single_mem_pi hr) i

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

Goal state before:
pp: case mk.mk
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✝ : R ⧸ I
a : R
b✝ : R ⧸ I
b : R
⊢ Quot.mk (⇑(Submodule.quotientRel I)) a * Quot.mk (⇑(Submodule.quotientRel I)) b =
    Quot.mk (⇑(Submodule.quotientRel I)) b * Quot.mk (⇑(Submodule.quotientRel I)) a

Tactic:
;

Goal state after:
case mk.mk
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✝ : R ⧸ I
a : R
b✝ : R ⧸ I
b : R
⊢ Quot.mk (⇑(Submodule.quotientRel I)) a * Quot.mk (⇑(Submodule.quotientRel I)) b =
    Quot.mk (⇑(Submodule.quotientRel I)) b * Quot.mk (⇑(Submodule.quotientRel I)) a
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
⊢ -↑⟨i, hi⟩ ∈ I

Tactic:
;

Goal state after:
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
⊢ -↑⟨i, hi⟩ ∈ I
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
x : R
⊢ (factor H) ((mk S) x) = (mk T) x

Tactic:
factor_mk

Goal state after:
R : Type u
inst✝² : Ring R
S T : Ideal R
inst✝¹ : S.IsTwoSided
inst✝ : T.IsTwoSided
H : S ≤ T
x : R
⊢ (mk T) x = (mk T) x
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
x✝ : R ⧸ J
⊢ (quotEquivOfEq h).symm x✝ = (quotEquivOfEq ⋯) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
x✝ : R ⧸ J
⊢ (quotEquivOfEq h).symm x✝ = (quotEquivOfEq ⋯) x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk
ι : 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 ⧸ ⊤
x : R
⊢ Quot.mk (⇑(Submodule.quotientRel ⊤)) x = default

Tactic:
;

Goal state after:
case mk
ι : 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 ⧸ ⊤
x : R
⊢ Quot.mk (⇑(Submodule.quotientRel ⊤)) x = default
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case refine_2
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I

Tactic:
· simp only [← eq_zero_iff_mem, (mk I).map_mul] at h ⊢
    have := @IsDomain.to_noZeroDivisors (R ⧸ I) _ H
    exact eq_zero_or_eq_zero_of_mul_eq_zero h

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
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a : R ⧸ I
ha : a ≠ 0
⊢ a * Classical.choose ⋯ = 1

Tactic:
;

Goal state after:
ι : 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
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a : R ⧸ I
ha : a ≠ 0
⊢ a * Classical.choose ⋯ = 1
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ (if x = ∅ then 1 else 0) = 0

Tactic:
exact if_neg (nonempty_iff_ne_empty.mp h0)

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

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

Tactic:
;

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ x ∈ range n, f (x + 1) (n - x) ^ n.choose (x + 1)) * f (n + 1) (n - n) ^ n.choose (n + 1) * f 0 (n + 1) =
    (∏ k ∈ range n, f (k + 1) (n + 1 - (k + 1)) ^ n.choose (k + 1)) * f 0 (n + 1 - 0) ^ n.choose 0
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
⊢ ⊥.IsPrime

Tactic:
;

Goal state after:
α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
⊢ ⊥.IsPrime
Module: Mathlib.RingTheory.Ideal.Maximal

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

Tactic:
;

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊥
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case a
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 f (f.iterateMapComap i n K) ≤ map i ((fun K ↦ comap f (map i K))^[n] K)

Tactic:
;

Goal state after:
case a
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 f (f.iterateMapComap i n K) ≤ map i ((fun K ↦ comap f (map i K))^[n] K)
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk.mk.mk
ι : 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✝ : R ⧸ I
a : R
y✝ : R ⧸ I
b : R
b✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ (Quot.mk (⇑(Submodule.quotientRel I)) a * Quot.mk (⇑(Submodule.quotientRel I)) b) •
      Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c =
    Quot.mk (⇑(Submodule.quotientRel I)) a •
      Quot.mk (⇑(Submodule.quotientRel I)) b • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c

Tactic:
;

Goal state after:
case mk.mk.mk
ι : 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✝ : R ⧸ I
a : R
y✝ : R ⧸ I
b : R
b✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ (Quot.mk (⇑(Submodule.quotientRel I)) a * Quot.mk (⇑(Submodule.quotientRel I)) b) •
      Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c =
    Quot.mk (⇑(Submodule.quotientRel I)) a •
      Quot.mk (⇑(Submodule.quotientRel I)) b • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
refine span_le.mpr ?_ this

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ (fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support ⊆ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk
ι : 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
b✝ : (ι → R) ⧸ pi fun x ↦ I
a : ι → R
⊢ 1 • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a = Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a

Tactic:
;

Goal state after:
case mk
ι : 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
b✝ : (ι → R) ⧸ pi fun x ↦ I
a : ι → R
⊢ 1 • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a = Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk
ι : 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
a✝ : R ⧸ I
a : R
⊢ Quot.mk (⇑(Submodule.quotientRel I)) a • 0 = 0

Tactic:
;

Goal state after:
case mk
ι : 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
a✝ : R ⧸ I
a : R
⊢ Quot.mk (⇑(Submodule.quotientRel I)) a • 0 = 0