mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Pi

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
ι' : Type x'
inst✝⁶ : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : (i : ι) → AddCommMonoid (ψ i)
inst✝² : (i : ι) → Module R (ψ i)
inst✝¹ : (i : ι) → AddCommMonoid (χ i)
inst✝ : (i : ι) → Module R (χ i)
e : (i : ι) → φ i ≃ₗ[R] ψ i
c : R
f : (i : ι) → φ i
x✝ : ι
⊢ (e x✝) ((c • f) x✝) = ((RingHom.id R) c • fun i ↦ (e i) (f i)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
x : M
⊢ (f.range.mkQ ∘ₛₗ f) x = 0 x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a b : α
⊢ ↑(Icc a (pred b)) = ↑(Ico a b)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a b : α
⊢ ↑(Ioc (pred a) b) = ↑(Icc a b)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
p : Submodule R M
x : M
y : M₂
⊢ (x, y) ∈ comap (fst R M M₂) p ↔ (x, y) ∈ p.prod ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a b : α
⊢ ↑(Ioo (pred a) b) = ↑(Ico a b)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a b : α
⊢ ↑(Ioc (pred a) (pred b)) = ↑(Ico a b)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ comap (snd R M M₂) q ↔ (x, y) ∈ ⊤.prod q

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
p : Submodule R M
q : Submodule R M₂
x✝ : M
⊢ x✝ ∈ comap (inl R M M₂) (p.prod q) ↔ x✝ ∈ p

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
p : Submodule R M
q : Submodule R M₂
x✝ : M₂
⊢ x✝ ∈ comap (inr R M M₂) (p.prod q) ↔ x✝ ∈ q

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
⊢ ↑(Iio (succ b)) = ↑(Iic b)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
b : α
⊢ ↑(Iic (pred b)) = ↑(Iio b)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ ↑(Ici (succ a)) = ↑(Ioi a)

Tactic:
simp

Goal state after:
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✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ ∀ (x y : ↥(fst R M M₂)), (↑(x + y)).1 = (↑x).1 + (↑y).1

Tactic:
simp

Goal state after:
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✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ ∀ (m : R) (x : ↥(fst R M M₂)), (↑(m • x)).1 = (RingHom.id R) m • (↑x).1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a : α
⊢ ↑(Ioi (pred a)) = ↑(Ici a)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1.mem
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
k : ι'
i : ι
⊢ (fun i ↦ single (Sum.inl i) 1) i (Sum.inr k) = 0

Tactic:
simp

Goal state after:
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✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x : M
⊢ (fun x ↦ (↑x).1) ((fun m ↦ ⟨(m, 0), ⋯⟩) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1.zero
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
k : ι'
⊢ 0 (Sum.inr k) = 0

Tactic:
simp

Goal state after:
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✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ ∀ (x y : ↥(snd R M M₂)), (↑(x + y)).2 = (↑x).2 + (↑y).2

Tactic:
simp

Goal state after:
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✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ ∀ (m : R) (x : ↥(snd R M M₂)), (↑(m • x)).2 = (RingHom.id R) m • (↑x).2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc a b

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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
ι' : Type x'
n : ℕ
M : Fin n.succ → Type u_1
inst✝² : Semiring R
inst✝¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝ : (i : Fin n.succ) → Module R (M i)
x y : M 0 × ((i : Fin n) → M i.succ)
⊢ ∀ (i : Fin n), (consEquiv M).toFun (x + y) i.succ = ((consEquiv M).toFun x + (consEquiv M).toFun y) i.succ

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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
ι' : Type x'
n : ℕ
M : Fin n.succ → Type u_1
inst✝² : Semiring R
inst✝¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝ : (i : Fin n.succ) → Module R (M i)
c : R
x : M 0 × ((i : Fin n) → M i.succ)
⊢ ∀ (i : Fin n), (consEquiv M).toFun (c • x) i.succ = ((RingHom.id R) c • (consEquiv M).toFun x) i.succ

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
m : M
n : M₂
⊢ (m, n) = (m, 0) + (0, n)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
m : M
n : M₂
⊢ (LinearMap.snd R M M₂) (m, 0) ∈ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
m : M
n : M₂
⊢ (LinearMap.fst R M M₂) (0, n) ∈ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), Finite ↑(f ⁻¹' {y})
val✝ : Fintype β
⊢ ∀ (x : α), x ∈ univ.biUnion fun y ↦ (f ⁻¹' {y}).toFinset

Tactic:
simp

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✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
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:
simp

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.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✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
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:
simp

Goal state after:
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✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
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✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
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:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case hl.hl.fst
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.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inl R M₁ M₂)
        x✝).1 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R M₁ M₂) x✝).1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case hl.hl.snd
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.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inl R M₁ M₂)
        x✝).2 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R M₁ M₂) x✝).2

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case hl.hr.fst
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.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inr R M₁ M₂)
        x✝).1 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R M₁ M₂) x✝).1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case hl.hr.snd
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.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
          LinearMap.inr R M₁ M₂)
        x✝).2 =
    ((((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R M₁ M₂) x✝).2

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case hr.fst
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.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).1 =
    (((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case hr.snd
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.snd R M₁ (M₂ × M₃) ∘ₗ ↑(prodAssoc R M₁ M₂ M₃)) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).2 =
    (((LinearMap.snd R M₁ M₂).prodMap LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃) x✝).2

Tactic:
simp

Goal state after:
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
N : Type ?u.19
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : R
x✝ : M × N
⊢ (-(x✝¹ • x✝).2, (x✝¹ • x✝).1) = (RingHom.id R) x✝¹ • (-x✝.2, x✝.1)

Tactic:
simp

Goal state after:
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
N : Type ?u.19
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M × N
⊢ (fun x ↦ (x.2, -x.1)) ((fun x ↦ (-x.2, x.1)) x✝) = x✝

Tactic:
simp

Goal state after:
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
N : Type ?u.19
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : N × M
⊢ (fun x ↦ (-x.2, x.1)) ((fun x ↦ (x.2, -x.1)) x✝) = x✝

Tactic:
simp

Goal state after:
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✝¹ : AddCommMonoid M₃
inst✝ : AddCommGroup M₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
f : M →ₗ[R] M₄
p : M × M₃
⊢ (fun p ↦ (e₁.symm p.1, e₂.symm (p.2 - f (e₁.symm p.1))))
      (((↑e₁ ∘ₗ LinearMap.fst R M M₃).prod (↑e₂ ∘ₗ LinearMap.snd R M M₃ + f ∘ₗ LinearMap.fst R M M₃)).toFun p) =
    p

Tactic:
simp

Goal state after:
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✝¹ : AddCommMonoid M₃
inst✝ : AddCommGroup M₄
module_M : Module R M
module_M₂ : Module R M₂
module_M₃ : Module R M₃
module_M₄ : Module R M₄
e₁ : M ≃ₗ[R] M₂
e₂ : M₃ ≃ₗ[R] M₄
f : M →ₗ[R] M₄
p : M₂ × M₄
⊢ ((↑e₁ ∘ₗ LinearMap.fst R M M₃).prod (↑e₂ ∘ₗ LinearMap.snd R M M₃ + f ∘ₗ LinearMap.fst R M M₃)).toFun
      ((fun p ↦ (e₁.symm p.1, e₂.symm (p.2 - f (e₁.symm p.1)))) p) =
    p

Tactic:
simp

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case right.a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ (partialSups f) i ≤ f j

Tactic:
exact partialSups_le _ _ _ fun k hk => hj_le k hk

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d : M
⊢ InjOn (fun x ↦ x + d) (Ici a)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d : M
⊢ InjOn (fun x ↦ x + d) (Ioi a)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ico a b) (Ico (a + d) (b + d))

Tactic:
rw [← Ici_inter_Iio, ← Ici_inter_Iio]

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ici a ∩ Iio b) (Ici (a + d) ∩ Iio (b + d))
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
⊢ a ∉ Ico (a + 1) b

Tactic:
simp

Goal state after:
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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
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:
simp

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

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

Tactic:
toZ_of_ge le_rfl

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ ↑(Nat.find ⋯) = 0
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
⊢ disjointed s 0 = s 0

Tactic:
simp

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

Goal state before:
pp: case zero
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
hn : ¬IsMin (pred^[0] i0)
⊢ toZ i0 (pred^[0] i0) = -↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝ : Monoid A
⊢ ∀ (a b : HasMulAntidiagonal A), a = b

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
A : Type u_1
inst✝ : Monoid A
a : A → Finset (A × A)
ha : ∀ {n : A} {a_1 : A × A}, a_1 ∈ a n ↔ a_1.1 * a_1.2 = n
b : A → Finset (A × A)
hb : ∀ {n : A} {a : A × A}, a ∈ b n ↔ a.1 * a.2 = n
⊢ { mulAntidiagonal := a, mem_mulAntidiagonal := ha } = { mulAntidiagonal := b, mem_mulAntidiagonal := hb }
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: M : Type u_2
inst✝¹ : Monoid M
inst✝ : HasMulAntidiagonal M
a : M
⊢ (1, a) ∈ mulAntidiagonal a

Tactic:
simp

Goal state after:
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 = ⨆ j, ⨆ (_ : j ≤ n), disjointed f j

Tactic:
simp

Goal state after: