mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (0, n + 1 + 1) ::ₘ ((n + 1).succ, id 0) ::ₘ map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)

Tactic:
]

Goal state after:
n : ℕ
⊢ (0, n + 1 + 1) ::ₘ ((n + 1).succ, id 0) ::ₘ map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ ↑(List.Nat.antidiagonal n) = ↑(List.Nat.antidiagonal n)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ x ∈ (range n).sigma fun m ↦ range (m + 1), f x.snd (x.fst - x.snd) =
    ∏ x ∈ (range n).sigma fun m ↦ range (n - m), f x.fst x.snd

Tactic:
]

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ x ∈ (range n).sigma fun m ↦ range (m + 1), f x.snd (x.fst - x.snd) =
    ∏ x ∈ (range n).sigma fun m ↦ range (n - m), f x.fst x.snd
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ (↑n).toNat = n

Tactic:
]

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ (↑n).toNat = n
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
f : ℕ → M
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
⊢ f n / f m = f n / f m

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ f (n + 1) / f m = f (n + 1) / f m

pp: case hmn
M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ m ≤ n + 1

Tactic:
]

Goal state after:
case hmn
M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ m ≤ n + 1
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Icc a b then f ⟨i, h⟩ else 1 else 1) =
    ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Icc a b then f ⟨i, h⟩ else 1 else 1) =
    ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i j : ι
⊢ toZ ⊥ i ≤ toZ ⊥ j ↔ toZ ⊥ i ≤ toZ ⊥ j

Tactic:
]

Goal state after:
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
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Iic a then f ⟨i, h⟩.succ / f ⟨i, h⟩.castSucc else 1 else 1) =
    f a.succ / f 0

Tactic:
]

Goal state after:
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Iic a then f ⟨i, h⟩.succ / f ⟨i, h⟩.castSucc else 1 else 1) =
    f a.succ / f 0
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ toZ ⊥ (succ^[↑n] ⊥) ≤ ↑↑n

Tactic:
]

Goal state after:
case refine_1
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ toZ ⊥ (succ^[↑n] ⊥) ≤ ↑↑n
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ (∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩.succ / f ⟨i, h⟩.castSucc else 1) = f b.succ / f a.castSucc

Tactic:
]

Goal state after:
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ (∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩.succ / f ⟨i, h⟩.castSucc else 1) = f b.succ / f a.castSucc
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : succ^[↑n] ⊥ = ⊤
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat

Tactic:
]

Goal state after:
case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : succ^[↑n] ⊥ = ⊤
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : succ^[↑n] ⊥ = ⊤
⊢ ↑n ≤ (toZ ⊥ ⊤).toNat

Tactic:
]

Goal state after:
case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : succ^[↑n] ⊥ = ⊤
⊢ ↑n ≤ (toZ ⊥ ⊤).toNat
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case neg
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : ¬IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (↑↑n).toNat

Tactic:
]

Goal state after:
case neg
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : ¬IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (↑↑n).toNat
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
xy : ℕ × ℕ
⊢ xy.1 + xy.2 = n ↔ xy.1 + xy.2 = n

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
i j : ι
⊢ toZ ⊥ i ≤ toZ ⊥ j ↔ toZ ⊥ i ≤ toZ ⊥ j

Tactic:
]

Goal state after:
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 : ℕ
⊢ (antidiagonal (n + 1)).val =
    (0, n + 1) ::ₘ
      Multiset.map (⇑({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)))
        (antidiagonal n).val

Tactic:
]

Goal state after:
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (0, n + 1) ::ₘ
      Multiset.map (⇑({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)))
        (antidiagonal n).val
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map (⇑((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }))
        (antidiagonal n).val

Tactic:
]

Goal state after:
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map (⇑((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }))
        (antidiagonal n).val
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ i = i

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + k = n

Tactic:
]

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + k = n
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.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 a b : ℕ
⊢ a + b = k ∧ a = i ∧ b + (n - k) = j ↔ a + b = k ∧ a = i ∧ b + (n - k) = j

Tactic:
]

Goal state after:
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
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (antidiagonal n) | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)

Tactic:
]

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (antidiagonal n) | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)
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.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1).swap * ∏ p ∈ antidiagonal n, f (p.swap.1 + 1, p.swap.2).swap =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1).swap * ∏ p ∈ antidiagonal n, f (p.swap.1 + 1, p.swap.2).swap =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → ℕ → M
p : ℕ × ℕ
hp : p ∈ antidiagonal n
⊢ f p n = f p n

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ k ≤ i
⊢ n - k = n - k

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ n - k + k = n

Tactic:
]

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ n - k + k = n
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.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 a b : ℕ
⊢ a + b = n - k ∧ a = i ∧ b + k = j ↔ a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
]

Goal state after:
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
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (antidiagonal n) | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
]

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (antidiagonal n) | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : x ∈ I
⊢ x ∈ I

Tactic:
]

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : x ∈ I
⊢ x ∈ I
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 α
I : Ideal α
x y : α
hx : x ∈ I
h : y * x = 1
z : α
x✝ : z ∈ ⊤
⊢ z = z

Tactic:
]

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

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬I = ⊤ → I = ⊥

Tactic:
]

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬I = ⊤ → I = ⊥
Module: Mathlib.RingTheory.Ideal.Lattice

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I ≤ ⊥
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ (n - m) * a ^ m ∈ I

Tactic:
]

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ (n - m) * a ^ m ∈ 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.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ n = n

pp: n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ i ≤ n

Tactic:
]

Goal state after:
n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ i ≤ n
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 - b) * c + b * (c - d) ∈ I

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 - b) * c + b * (c - d) ∈ I
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: case zero
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
H : 1 ∈ I
⊢ r ∈ I

Tactic:
]

Goal state after:
case zero
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
H : 1 ∈ I
⊢ r ∈ I
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: case succ
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ n * r ∈ I
⊢ r ∈ I

Tactic:
]

Goal state after:
case succ
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ n * r ∈ I
⊢ r ∈ I
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
β : Type v
F : Type w
inst✝² : Semiring α
I : Ideal α
a b : α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
h : 1 = 0
⊢ 1 = 0

Tactic:
]

Goal state after:
α : Type u
β : Type v
F : Type w
inst✝² : Semiring α
I : Ideal α
a b : α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
h : 1 = 0
⊢ 1 = 0
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : y ∉ I
⊢ x ∈ I ∨ y ∈ I ↔ x ∈ I

pp: case hI
α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : y ∉ I
⊢ I.IsPrime

Tactic:
]

Goal state after:
α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : y ∉ I
⊢ x ∈ I ∨ y ∈ I ↔ x ∈ I

case hI
α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : y ∉ I
⊢ I.IsPrime
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ 1 - a = 1 - a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ a * a = a ↔ a * a = a

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i) + x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i) + x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x * (x ^ i * (y ^ (n - i) * ↑(n.choose i))) = x * (x ^ i * (y ^ (n - i) * ↑(n.choose i)))

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ b * a = b * a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a + b * a + (a * b + b) = a + (0 + b)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a + b * a + (a * b + b) = a + (0 + b)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
]

Goal state after:
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ (1 + 1) • (a * b * a) = 0

Tactic:
]

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ (1 + 1) • (a * b * a) = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * y ^ (n - i.succ).succ * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * y ^ (n - i.succ).succ * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
this : a * b = 0
⊢ a * b = 0

Tactic:
]

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
this : a * b = 0
⊢ a * b = 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * (y * (y ^ (n - i.succ) * ↑(n.choose i.succ))) =
    x ^ i.succ * (y * (y ^ (n - i.succ) * ↑(n.choose i.succ)))

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
⊢ 0 = 0

Tactic:
]

Goal state after: