mathlib-initiative/mathlib-tactics huggingface dataset:
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₃
S : Submodule R M
S' : Submodule R M₂
⊢ ⇑(f.coprod g) '' ↑(S.prod S') = Set.image2 (fun a b ↦ f a + g b) ↑S ↑S'

Tactic:
]

Goal state after:
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₃
S : Submodule R M
S' : Submodule R M₂
⊢ ⇑(f.coprod g) '' ↑(S.prod S') = Set.image2 (fun a b ↦ f a + g b) ↑S ↑S'
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ a ≤ x ∧ x < b ↔ a ≤ x ∧ x < b

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ico a b = Ico a b

Tactic:
]

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 × M₂ →ₗ[R] M₃
⊢ (f ∘ₗ inl R M M₂).coprod (f ∘ₗ inr R M M₂) = f

Tactic:
← comp_coprod,

Goal state after:
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 × M₂ →ₗ[R] M₃
⊢ f ∘ₗ (inl R M M₂).coprod (inr R M M₂) = f
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 × M₂ →ₗ[R] M₃
⊢ f = f

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
h' : f.ker ≤ p
⊢ ⊥ = ⊥

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ Icc a b = Icc a b

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ Ioc a b = Ioc a b

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ Ico a b = Ico a b

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ map q.mkQ f.range = map q.mkQ f.range

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ ∅ = ∅

pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ ¬succ a ≤ pred b

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ ¬succ a ≤ pred b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
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
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hjJ : j ∈ J
this : j ∉ I
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : ¬IsMin b
⊢ Ioo a b = Ioo a b

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M
⊢ p'.mkQ x = p'.mkQ x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x ≤ b ↔ x ≤ b

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x < b ↔ x < b

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
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₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
⊢ Submodule.comap (f.prodMap g) ⊥ = Submodule.comap (f.prodMap g) ⊥

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ (factor H2 ∘ₗ factor H1) x = (factor ⋯) x

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ (factor H2 ∘ₗ factor H1) x = (factor ⋯) x
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
x : α
⊢ a < x ↔ a < x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ a ≤ x ↔ a ≤ x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ∃ y ∈ f.range, ⇑f ⁻¹' {y} ⊆ ↑(span R (⇑f ⁻¹' s))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ∃ y ∈ f.range, ⇑f ⁻¹' {y} ⊆ ↑(span R (⇑f ⁻¹' s))
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case disjoint
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 ∈ (inl R M M₂).range, x ∈ (inr R M M₂).range → x = 0

Tactic:
]

Goal state after:
case disjoint
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 ∈ (inl R M M₂).range, x ∈ (inr R M M₂).range → x = 0
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case right
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
hy : {y} ⊆ s
⊢ ⇑f ⁻¹' {y} ⊆ ↑(span R (⇑f ⁻¹' s))

Tactic:
]

Goal state after:
case right
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
hy : {y} ⊆ s
⊢ ⇑f ⁻¹' {y} ⊆ ↑(span R (⇑f ⁻¹' s))
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case codisjoint
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₂
⊢ ⊤ ≤ (inl R M M₂).range ⊔ (inr R M M₂).range

Tactic:
]

Goal state after:
case codisjoint
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₂
⊢ ⊤ ≤ (inl R M M₂).range ⊔ (inr R M M₂).range
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)
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₂
⊢ p.prod q = p.prod q

Tactic:
]

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₂
s : Set M
t : Set M₂
⊢ span R (⇑(inl R M M₂) '' s) ⊔ span R (⇑(inr R M M₂) '' t) = span R (⇑(inl R M M₂) '' s) ⊔ span R (⇑(inr R M M₂) '' t)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ f.range ⊓ span R₂ s ≤ span R₂ s

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ f.range ⊓ span R₂ s ≤ span R₂ s
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₃
⊢ comap f ⊥ ⊓ comap g ⊥ = f.ker ⊓ g.ker

Tactic:
]

Goal state after:
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₃
⊢ comap f ⊥ ⊓ comap g ⊥ = f.ker ⊓ g.ker
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ b c = b c

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (f j) c = (f j) c

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i j : ι
⊢ diag j i = diag j i

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
x✝¹ : ι
x✝ : x✝¹ ∈ Finset.univ
⊢ (x x✝¹ • f fun j ↦ if x✝¹ = j then 1 else 0) = x x✝¹ • f fun j ↦ if x✝¹ = j then 1 else 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case h
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
⊢ f y + g z = 0

Tactic:
]

Goal state after:
case h
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
⊢ f y + g z = 0
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
this : f y = 0
⊢ f y = 0 ∧ g z = 0

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
this : f y = 0
⊢ f y = 0 ∧ g z = 0
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: 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
⊢ ∀ i_1 ∈ I, (single R φ i) x i_1 ∈ p i_1

Tactic:
]

Goal state after:
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
⊢ ∀ i_1 ∈ I, (single R φ i) x i_1 ∈ p i_1
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : 0 + g z = 0
this : f y = 0
⊢ f y = 0 ∧ g z = 0

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : 0 + g z = 0
this : f y = 0
⊢ f y = 0 ∧ g z = 0
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case intro
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi Set.univ p
⊢ ∑ i, Pi.single i (x i) ∈ ⨆ i, map (single R φ i) (p i)

Tactic:
]

Goal state after:
case intro
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi Set.univ p
⊢ ∑ i, Pi.single i (x i) ∈ ⨆ i, map (single R φ i) (p i)
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
R₃ : Type u_5
M₃ : Type u_6
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ g.ker ≤ f.range ↔ g.ker ≤ f.range

Tactic:
]

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₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v
h₁ : 0 ∘ₛₗ f = 0
⊢ ker 0 = ⊤

Tactic:
]

Goal state after:
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₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v
h₁ : 0 ∘ₛₗ f = 0
⊢ ker 0 = ⊤
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₂
⊢ ⊥ = ⊥

Tactic:
]

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₂
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this✝ : Fintype ι
this : x = ∑ i, x (Sum.inl i) • single (Sum.inl i) 1
⊢ ∑ i, x (Sum.inl i) • single (Sum.inl i) 1 ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)

Tactic:
]

Goal state after:
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this✝ : Fintype ι
this : x = ∑ i, x (Sum.inl i) • single (Sum.inl i) 1
⊢ ∑ i, x (Sum.inl i) • single (Sum.inl i) 1 ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = ⨆ a_1 ∈ s.toFinset, a ⊓ id a_1

Tactic:
]

Goal state after:
case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = ⨆ a_1 ∈ s.toFinset, a ⊓ id a_1
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
⊢ Iio (b + 1) = Iic b

Tactic:
simpa [succ_eq_add_one] using Iio_succ_eq_Iic_of_not_isMax hb

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₂
⊢ ⊤ ≤ fst R M M₂ ⊔ snd R M M₂

Tactic:
]

Goal state after:
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₂
⊢ ⊤ ≤ fst R M M₂ ⊔ snd R M M₂
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b = ⨅ a_1 ∈ s.toFinset, a ⊔ id a_1

Tactic:
]

Goal state after:
case e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b = ⨅ a_1 ∈ s.toFinset, a ⊔ id a_1
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, 0) + (0, n) ∈ fst R M M₂ ⊔ snd R M M₂

Tactic:
]

Goal state after:
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, 0) + (0, n) ∈ fst R M M₂ ⊔ snd R M M₂
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
x✝ a✝ : γ
⊢ a✝ ∈ s → r (f a✝) (f x✝) ↔ a✝ ∈ s → r (f a✝) (f x✝)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : ConditionallyCompleteLattice β
inst✝¹ : Finite ι
inst✝ : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
j : ι
hj : f j = ⨆ i, f i
⊢ g (f j) = ⨆ i, g (f i)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : ConditionallyCompleteLattice β
inst✝¹ : Finite ι
inst✝ : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
j : ι
hj : f j = ⨆ i, f i
⊢ g (f j) = ⨆ i, g (f i)