mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case refine_1
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ a_1 ∈ (Ico a b).sigma fun i ↦ Ico i b, ⟨a_1.snd, a_1.fst⟩ ∈ (Ico a b).sigma fun j ↦ Ico a (j + 1)

pp: case refine_2
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ a_1 ∈ (Ico a b).sigma fun j ↦ Ico a (j + 1), ⟨a_1.snd, a_1.fst⟩ ∈ (Ico a b).sigma fun i ↦ Ico i b

Tactic:
<;>

Goal state after:
case refine_1
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ a_1 ∈ (Ico a b).sigma fun i ↦ Ico i b, ⟨a_1.snd, a_1.fst⟩ ∈ (Ico a b).sigma fun j ↦ Ico a (j + 1)

case refine_2
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ a_1 ∈ (Ico a b).sigma fun j ↦ Ico a (j + 1), ⟨a_1.snd, a_1.fst⟩ ∈ (Ico a b).sigma fun i ↦ Ico i b
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case refine_1
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≤ b_1 ∧ b_1 < b → (a ≤ b_1 ∧ b_1 < b) ∧ a ≤ a_1 ∧ a_1 < b_1 + 1

pp: case refine_2
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a ≤ b_1 ∧ b_1 < a_1 + 1 → (a ≤ b_1 ∧ b_1 < b) ∧ b_1 ≤ a_1 ∧ a_1 < b

Tactic:
<;>

Goal state after:
case refine_1
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≤ b_1 ∧ b_1 < b → (a ≤ b_1 ∧ b_1 < b) ∧ a ≤ a_1 ∧ a_1 < b_1 + 1

case refine_2
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a ≤ b_1 ∧ b_1 < a_1 + 1 → (a ≤ b_1 ∧ b_1 < b) ∧ b_1 ≤ a_1 ∧ a_1 < b
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
⊢ i ≤ j

pp: case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
⊢ i ≤ j

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
⊢ i ≤ j

case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
⊢ i ≤ j
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case refine_1
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ a_1 ∈ (Ico a b).sigma fun i ↦ Ico (i + 1) b, ⟨a_1.snd, a_1.fst⟩ ∈ (Ico a b).sigma (Ico a)

pp: case refine_2
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ a_1 ∈ (Ico a b).sigma (Ico a), ⟨a_1.snd, a_1.fst⟩ ∈ (Ico a b).sigma fun i ↦ Ico (i + 1) b

Tactic:
<;>

Goal state after:
case refine_1
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ a_1 ∈ (Ico a b).sigma fun i ↦ Ico (i + 1) b, ⟨a_1.snd, a_1.fst⟩ ∈ (Ico a b).sigma (Ico a)

case refine_2
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ a_1 ∈ (Ico a b).sigma (Ico a), ⟨a_1.snd, a_1.fst⟩ ∈ (Ico a b).sigma fun i ↦ Ico (i + 1) b
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case refine_1
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 + 1 ≤ b_1 ∧ b_1 < b → (a ≤ b_1 ∧ b_1 < b) ∧ a ≤ a_1 ∧ a_1 < b_1

pp: case refine_2
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a ≤ b_1 ∧ b_1 < a_1 → (a ≤ b_1 ∧ b_1 < b) ∧ b_1 + 1 ≤ a_1 ∧ a_1 < b

Tactic:
<;>

Goal state after:
case refine_1
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 + 1 ≤ b_1 ∧ b_1 < b → (a ≤ b_1 ∧ b_1 < b) ∧ a ≤ a_1 ∧ a_1 < b_1

case refine_2
M : Type u_4
inst✝ : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a ≤ b_1 ∧ b_1 < a_1 → (a ≤ b_1 ∧ b_1 < b) ∧ b_1 + 1 ≤ a_1 ∧ a_1 < b
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
hn : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ f i

Tactic:
rwa [disjointed_succ, hf.partialSups_eq]

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

Goal state before:
pp: case pos
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
← Nat.Ico_zero_eq_range,

Goal state after:
case pos
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ Ico 0 (n - m), f (m + k)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case refine_1
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1), ⟨a.snd, a.fst - a.snd⟩ ∈ (range n).sigma fun m ↦ range (n - m)

pp: case refine_2
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (n - m), ⟨a.fst + a.snd, a.fst⟩ ∈ (range n).sigma fun m ↦ range (m + 1)

pp: case refine_3
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1),
    ⟨⟨a.snd, a.fst - a.snd⟩.fst + ⟨a.snd, a.fst - a.snd⟩.snd, ⟨a.snd, a.fst - a.snd⟩.fst⟩ = a

pp: case refine_4
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (n - m),
    ⟨⟨a.fst + a.snd, a.fst⟩.snd, ⟨a.fst + a.snd, a.fst⟩.fst - ⟨a.fst + a.snd, a.fst⟩.snd⟩ = a

pp: case refine_5
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1),
    f a.snd (a.fst - a.snd) = f ⟨a.snd, a.fst - a.snd⟩.fst ⟨a.snd, a.fst - a.snd⟩.snd

Tactic:
<;>

Goal state after:
case refine_1
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1), ⟨a.snd, a.fst - a.snd⟩ ∈ (range n).sigma fun m ↦ range (n - m)

case refine_2
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (n - m), ⟨a.fst + a.snd, a.fst⟩ ∈ (range n).sigma fun m ↦ range (m + 1)

case refine_3
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1),
    ⟨⟨a.snd, a.fst - a.snd⟩.fst + ⟨a.snd, a.fst - a.snd⟩.snd, ⟨a.snd, a.fst - a.snd⟩.fst⟩ = a

case refine_4
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (n - m),
    ⟨⟨a.fst + a.snd, a.fst⟩.snd, ⟨a.fst + a.snd, a.fst⟩.fst - ⟨a.fst + a.snd, a.fst⟩.snd⟩ = a

case refine_5
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1),
    f a.snd (a.fst - a.snd) = f ⟨a.snd, a.fst - a.snd⟩.fst ⟨a.snd, a.fst - a.snd⟩.snd
Module: Mathlib.Algebra.BigOperators.Intervals

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

pp: case h₂
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ Icc ↑a ↑b, a_1 ∉ range n → (if h : a_1 < n then f ⟨a_1, h⟩ else 1) = 1

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

Tactic:
<;>

Goal state after:
case h₁
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ range n, a_1 ∉ Icc ↑a ↑b → (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Icc a b then f ⟨a_1, h⟩ else 1 else 1) = 1

case h₂
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ Icc ↑a ↑b, a_1 ∉ range n → (if h : a_1 < n then f ⟨a_1, h⟩ else 1) = 1

case h
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ range n,
    a_1 ∈ Icc ↑a ↑b →
      (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Icc a b then f ⟨a_1, h⟩ else 1 else 1) = if h : a_1 < n then f ⟨a_1, h⟩ else 1
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:
convert! prod_range_div (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1) (a + 1) using 1 with k
    hk

Goal state after:
case e'_2
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) =
    ∏ i ∈ range (↑a + 1), (if hi : i + 1 < n + 1 then f ⟨i + 1, hi⟩ else 1) / if hi : i < n + 1 then f ⟨i, hi⟩ else 1

case e'_3
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ f a.succ / f 0 = (if hi : ↑a + 1 < n + 1 then f ⟨↑a + 1, hi⟩ else 1) / if hi : 0 < n + 1 then f ⟨0, hi⟩ else 1
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ {a ∈ antidiagonal n | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
by
  have aux₁ : fun a ↦ k ≤ a.snd = (fun a ↦ k ≤ a.fst) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
  have 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 :=
    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
  rw [← map_prodComm_antidiagonal]
  simp_rw [aux₁, ← map_filter, antidiagonal_filter_le_fst_of_le h,
    map_map]
  ext ⟨i, j⟩
  simpa using aux₂ i j

Goal state after:
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
⊢ IsIdempotentElem (1 - a)

Tactic:
by
  rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]

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

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

Tactic:
ha.eq,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ a + b * a + (a * b + b * b) = a + b
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ b * b - a - (a - a * a) = b - a

Tactic:
ha.eq,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ b * b - a - (a - a) = b - a
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
this : a * (a * (b * a)) + a * (b * (a * a)) = 0
⊢ (1 + 1) • (a * b * a) = 0

Tactic:
ha.eq,

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
this : a * (a * (b * a)) + a * (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
this : a * a * b * a + a * b * a = 0
⊢ (1 + 1) • (a * b * a) = 0

Tactic:
ha.eq,

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
this : a * b * a + a * b * a = 0
⊢ (1 + 1) • (a * b * a) = 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)

Tactic:
rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']

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

Goal state before:
pp: case h₁
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {y} ≤ span {x} ↔ x ∣ y

pp: case h₂
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} ≤ span {y} ↔ y ∣ x

Tactic:
<;>

Goal state after:
case h₁
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {y} ≤ span {x} ↔ x ∣ y

case h₂
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} ≤ span {y} ↔ y ∣ x
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
span_pair_add_right,

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {y, x} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

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

pp: case inr
α : Type u
inst✝¹ : Ring α
x : α
inst✝ : LinearOrder α
h : |x| = -x
⊢ span {|x|} = span {x}

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝¹ : Ring α
x : α
inst✝ : LinearOrder α
h : |x| = x
⊢ span {|x|} = span {x}

case inr
α : Type u
inst✝¹ : Ring α
x : α
inst✝ : LinearOrder α
h : |x| = -x
⊢ span {|x|} = span {x}
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:
congr! 2 with _ h'

Goal state after:
case a
n : ℕ
h : ¬n = 0
x✝ : ℕ
h' : x✝ ∈ range (n + 1)
⊢ (n - x✝) * n.choose (n - x✝) = (n - x✝) * n.choose x✝
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case isUnit_or_isUnit.refine_1.a
α : 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)
⊢ span {a} ≤ span {a * (c * d)}

pp: case a
α : 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)
⊢ span {a * (c * d)} ≤ span {a}

Tactic:
<;>

Goal state after:
case isUnit_or_isUnit.refine_1.a
α : 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)
⊢ span {a} ≤ span {a * (c * d)}

case a
α : 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)
⊢ span {a * (c * d)} ≤ span {a}
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:
rw [Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
ι : Type u_1
R : Type u_3
inst✝¹ : Ring R
f : ι → R
inst✝ : (span (range f)).IsTwoSided
i : ι
⊢ f i ∈ span (range f)
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:
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]

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

Goal state before:
pp: case left
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite ↥?m.9

pp: case right
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite (R ⧸ ?m.9)

Tactic:
<;>

Goal state after:
case left
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite ↥?m.9

case right
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite (R ⧸ ?m.9)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ![⊥, ⊤] ((fun I ↦ if I = ⊥ then 0 else 1) ⊥) = ⊥

pp: case inr
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ![⊥, ⊤] ((fun I ↦ if I = ⊥ then 0 else 1) ⊤) = ⊤

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ![⊥, ⊤] ((fun I ↦ if I = ⊥ then 0 else 1) ⊥) = ⊥

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ![⊥, ⊤] ((fun I ↦ if I = ⊥ then 0 else 1) ⊤) = ⊤
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case «0»
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ (fun I ↦ if I = ⊥ then 0 else 1) (![⊥, ⊤] ((fun i ↦ i) ⟨0, ⋯⟩)) = (fun i ↦ i) ⟨0, ⋯⟩

pp: case «1»
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ (fun I ↦ if I = ⊥ then 0 else 1) (![⊥, ⊤] ((fun i ↦ i) ⟨1, ⋯⟩)) = (fun i ↦ i) ⟨1, ⋯⟩

Tactic:
<;>

Goal state after:
case «0»
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ (fun I ↦ if I = ⊥ then 0 else 1) (![⊥, ⊤] ((fun i ↦ i) ⟨0, ⋯⟩)) = (fun i ↦ i) ⟨0, ⋯⟩

case «1»
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
⊢ (fun I ↦ if I = ⊥ then 0 else 1) (![⊥, ⊤] ((fun i ↦ i) ⟨1, ⋯⟩)) = (fun i ↦ i) ⟨1, ⋯⟩
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬IsField R ↔ ∃ I, ⊥ < I ∧ I < ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot.ne' h_top.ne⟩
  obtain ⟨I, hI, hIm⟩ := exists_maximal_of_not_isField h
  exact ⟨I, bot_lt_iff_ne_bot.mpr hI, lt_top_iff_ne_top.mpr hIm.ne_top⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inl
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ p i
⊢ ((lsingle i) x) i ∈ p i

pp: case inr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ p i
j : α
h : i ≠ j
⊢ ((lsingle i) x) j ∈ p j

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ p i
⊢ ((lsingle i) x) i ∈ p i

case inr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ p i
j : α
h : i ≠ j
⊢ ((lsingle i) x) j ∈ p j
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: case he
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ⋂ i ∈ ∅, s i ∈ f ↔ ∀ i ∈ ∅, s i ∈ f

pp: case h₁
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ∀ (x : β), ⋂ i ∈ {x}, s i ∈ f ↔ ∀ i ∈ {x}, s i ∈ f

Tactic:
<;>

Goal state after:
case he
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ⋂ i ∈ ∅, s i ∈ f ↔ ∀ i ∈ ∅, s i ∈ f

case h₁
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ∀ (x : β), ⋂ i ∈ {x}, s i ∈ f ↔ ∀ i ∈ {x}, s i ∈ f
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mpr.mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ i ∈ x.support → y i ≠ 0

pp: case mpr.mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ y i ≠ 0 → i ∈ x.support

Tactic:
<;>

Goal state after:
case mpr.mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ i ∈ x.support → y i ≠ 0

case mpr.mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ y i ≠ 0 → i ∈ x.support
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mpr.mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ y i = 0 → i ∉ x.support

pp: case mpr.mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ i ∉ x.support → y i = 0

Tactic:
<;>

Goal state after:
case mpr.mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ y i = 0 → i ∉ x.support

case mpr.mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ i ∉ x.support → y i = 0
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t

Tactic:
rcases hq i hpi with ⟨j, hpj, hqj, hji⟩

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
j : ι
hpj : p j
hqj : q j
hji : s j ⊆ s i
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
X : Type u_7
inst✝ : Finite X
⊢ linearMap R M _root_.id = LinearMap.id

Tactic:
classical
  aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_5
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
X : Type u_7
Y : Type u_8
Z : Type u_9
inst✝² : Finite X
inst✝¹ : Finite Y
inst✝ : Finite Z
f : X → Y
g : Y → Z
⊢ linearMap R M (g ∘ f) = linearMap R M g ∘ₗ linearMap R M f

Tactic:
classical
  aesop

Goal state after: