mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) 0 = vecCons (vecHead v + y) (vecTail v + w) 0

pp: case refine_2
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (v + vecCons y w) i.succ = vecCons (vecHead v + y) (vecTail v + w) i.succ

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) 0 = vecCons (vecHead v + y) (vecTail v + w) 0

case refine_2
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (v + vecCons y w) i.succ = vecCons (vecHead v + y) (vecTail v + w) i.succ
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) 0 = vecCons (x - vecHead w) (v - vecTail w) 0

pp: case refine_2
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (vecCons x v - w) i.succ = vecCons (x - vecHead w) (v - vecTail w) i.succ

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) 0 = vecCons (x - vecHead w) (v - vecTail w) 0

case refine_2
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (vecCons x v - w) i.succ = vecCons (x - vecHead w) (v - vecTail w) i.succ
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) 0 = vecCons (vecHead v - y) (vecTail v - w) 0

pp: case refine_2
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (v - vecCons y w) i.succ = vecCons (vecHead v - y) (vecTail v - w) i.succ

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) 0 = vecCons (vecHead v - y) (vecTail v - w) 0

case refine_2
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (v - vecCons y w) i.succ = vecCons (vecHead v - y) (vecTail v - w) i.succ
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) 0 = vecCons (-x) (-v) 0

pp: case refine_2
α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (-vecCons x v) i.succ = vecCons (-x) (-v) i.succ

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) 0 = vecCons (-x) (-v) 0

case refine_2
α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (-vecCons x v) i.succ = vecCons (-x) (-v) i.succ
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
← encard_eq_four,

Goal state after:
α : Type u_1
s : Set α
⊢ s.ncard = 4 ↔ s.encard = 4
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

pp: case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

pp: case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

pp: case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

pp: case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inl R M M₂) y = x) → (snd R M M₂) x = 0

pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (snd R M M₂) x = 0 → ∃ y, (inl R M M₂) y = x

Tactic:
· rintro ⟨y, rfl⟩
    rfl

Goal state after:
case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (snd R M M₂) x = 0 → ∃ y, (inl R M M₂) y = x
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inr R M M₂) y = x) → (fst R M M₂) x = 0

pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (fst R M M₂) x = 0 → ∃ y, (inr R M M₂) y = x

Tactic:
· rintro ⟨y, rfl⟩
    rfl

Goal state after:
case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (fst R M M₂) x = 0 → ∃ y, (inr R M M₂) y = x
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
⊢ f.coprod g ∘ₗ inr R M M₂ = g

Tactic:
by
  ext; simp only [map_zero, coprod_apply, inr_apply, zero_add, comp_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case fst
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (((inl R M M₂).coprod (inr R M M₂)) x✝).1 = (id x✝).1

pp: case snd
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (((inl R M M₂).coprod (inr R M M₂)) x✝).2 = (id x✝).2

Tactic:
<;>

Goal state after:
case fst
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (((inl R M M₂).coprod (inr R M M₂)) x✝).1 = (id x✝).1

case snd
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (((inl R M M₂).coprod (inr R M M₂)) x✝).2 = (id x✝).2
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : Semiring S
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : AddCommMonoid M₄
inst✝⁹ : AddCommMonoid M₅
inst✝⁸ : AddCommMonoid M₆
inst✝⁷ : Module R M
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Module R M₄
inst✝³ : Module R M₅
inst✝² : Module R M₆
f✝ : M →ₗ[R] M₂
inst✝¹ : Module S M₃
inst✝ : SMulCommClass R S M₃
f : M × M₂ →ₗ[R] M₃
⊢ (fun f ↦ f.1.coprod f.2) ((fun f ↦ (f ∘ₗ inl R M M₂, f ∘ₗ inr R M M₂)) f) = f

Tactic:
simp only [← comp_coprod, comp_id, coprod_inl_inr]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ (f.prod g).ker = f.ker ⊓ g.ker

Tactic:
rw [ker, ← prod_bot, comap_prod_prod]; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case inl
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
j : ι
x : φ j
hx : x ∈ p j
⊢ (single R φ j) x j ∈ p j

pp: case inr
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
j : ι
hne : j ≠ i
⊢ (single R φ i) x j ∈ p j

Tactic:
<;>

Goal state after:
case inl
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
j : ι
x : φ j
hx : x ∈ p j
⊢ (single R φ j) x j ∈ p j

case inr
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
j : ι
hne : j ≠ i
⊢ (single R φ i) x j ∈ p j
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
by
  simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc_of_not_isMax ha b

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case hl
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M
⊢ ((LinearMap.fst R M₂ M ∘ₗ ↑(prodComm R M M₂)) ∘ₗ LinearMap.inl R M M₂) x✝ =
    (LinearMap.snd R M M₂ ∘ₗ LinearMap.inl R M M₂) x✝

pp: case hr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M₂
⊢ ((LinearMap.fst R M₂ M ∘ₗ ↑(prodComm R M M₂)) ∘ₗ LinearMap.inr R M M₂) x✝ =
    (LinearMap.snd R M M₂ ∘ₗ LinearMap.inr R M M₂) x✝

Tactic:
<;>

Goal state after:
case hl
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M
⊢ ((LinearMap.fst R M₂ M ∘ₗ ↑(prodComm R M M₂)) ∘ₗ LinearMap.inl R M M₂) x✝ =
    (LinearMap.snd R M M₂ ∘ₗ LinearMap.inl R M M₂) x✝

case hr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M₂
⊢ ((LinearMap.fst R M₂ M ∘ₗ ↑(prodComm R M M₂)) ∘ₗ LinearMap.inr R M M₂) x✝ =
    (LinearMap.snd R M M₂ ∘ₗ LinearMap.inr R M M₂) x✝
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case hl
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M
⊢ ((LinearMap.snd R M₂ M ∘ₗ ↑(prodComm R M M₂)) ∘ₗ LinearMap.inl R M M₂) x✝ =
    (LinearMap.fst R M M₂ ∘ₗ LinearMap.inl R M M₂) x✝

pp: case hr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M₂
⊢ ((LinearMap.snd R M₂ M ∘ₗ ↑(prodComm R M M₂)) ∘ₗ LinearMap.inr R M M₂) x✝ =
    (LinearMap.fst R M M₂ ∘ₗ LinearMap.inr R M M₂) x✝

Tactic:
<;>

Goal state after:
case hl
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M
⊢ ((LinearMap.snd R M₂ M ∘ₗ ↑(prodComm R M M₂)) ∘ₗ LinearMap.inl R M M₂) x✝ =
    (LinearMap.fst R M M₂ ∘ₗ LinearMap.inl R M M₂) x✝

case hr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M₂
⊢ ((LinearMap.snd R M₂ M ∘ₗ ↑(prodComm R M M₂)) ∘ₗ LinearMap.inr R M M₂) x✝ =
    (LinearMap.fst R M M₂ ∘ₗ LinearMap.inr R M M₂) x✝
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case hl.hl
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₁
⊢ (((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R M₁ M₂)
      x✝ =
    (((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R M₁ M₂)
      x✝

pp: case hl.hr
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₂
⊢ (((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R M₁ M₂)
      x✝ =
    (((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R M₁ M₂)
      x✝

pp: case hr
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₃
⊢ ((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝ =
    ((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝

Tactic:
<;>

Goal state after:
case hl.hl
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₁
⊢ (((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R M₁ M₂)
      x✝ =
    (((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R M₁ M₂)
      x✝

case hl.hr
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₂
⊢ (((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R M₁ M₂)
      x✝ =
    (((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R M₁ M₂)
      x✝

case hr
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝ : M₃
⊢ ((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝ =
    ((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
c : R
x : M × M₂
hx : x.2 = f x.1
⊢ c • x.2 = f (c • x.1)

Tactic:
rw [map_smul, hx]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ disjointed f i = f i

Tactic:
by
  rw [disjointed_apply, sdiff_eq_left, disjoint_iff, sup_inf_distrib_left,
    sup_congr rfl <| fun j hj ↦ disjoint_iff.mp <| (hf _ (mem_Iio.mp hj)).symm]
  exact sup_bot _

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
⊢ False

Tactic:
have h_lt : ∀ n, succ^[n] i < j := fun n ↦ by
      induction n with
      | zero => simpa only [Function.iterate_zero, id] using hij
      | succ n hn =>
        refine lt_of_le_of_ne ?_ (h _)
        rw [Function.iterate_succ', Function.comp_apply]
        exact succ_le_of_lt hn

Goal state after:
case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
⊢ False
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case e_a.refine_1
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Ioi, ⟨a.snd, a.fst⟩ ∈ univ.sigma Iio

pp: case e_a.refine_2
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Iio, ⟨a.snd, a.fst⟩ ∈ univ.sigma Ioi

pp: case e_a.refine_3
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Ioi, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

pp: case e_a.refine_4
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Iio, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

pp: case e_a.refine_5
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Ioi, f a.fst a.snd = f ⟨a.snd, a.fst⟩.snd ⟨a.snd, a.fst⟩.fst

Tactic:
<;>

Goal state after:
case e_a.refine_1
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Ioi, ⟨a.snd, a.fst⟩ ∈ univ.sigma Iio

case e_a.refine_2
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Iio, ⟨a.snd, a.fst⟩ ∈ univ.sigma Ioi

case e_a.refine_3
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Ioi, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

case e_a.refine_4
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Iio, ⟨⟨a.snd, a.fst⟩.snd, ⟨a.snd, a.fst⟩.fst⟩ = a

case e_a.refine_5
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∀ a ∈ univ.sigma Ioi, f a.fst a.snd = f ⟨a.snd, a.fst⟩.snd ⟨a.snd, a.fst⟩.fst
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun n ↦ ⟨succ^[n] i, ⋯⟩
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
h_le : n ≤ m
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i

pp: case inr
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun n ↦ ⟨succ^[n] i, ⋯⟩
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
h_le : m ≤ n
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i

Tactic:
· exact ⟨n, m, lt_of_le_of_ne h_le hnm_ne, hnm_eq⟩

Goal state after:
case inr
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun n ↦ ⟨succ^[n] i, ⋯⟩
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
h_le : m ≤ n
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ (∏ i ∈ Ioc a b, f i) * ∏ i ∈ Ioc b b.succ, f i = (∏ k ∈ Ioc a b, f k) * f (b + 1)

Tactic:
Nat.Ioc_succ_singleton,

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ (∏ i ∈ Ioc a b, f i) * ∏ i ∈ {b + 1}, f i = (∏ k ∈ Ioc a b, f k) * f (b + 1)