mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ Ici (succ a) = Ioi a

Tactic:
by

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'
⊢ Function.Surjective ⇑(factor H)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (pred a) = Ici a

Tactic:
by

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₄
⊢ (f.prodMap g).range = f.range.prod g.range

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p'✝ 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₂
p' : Submodule R (M ⧸ p)
⊢ p' ≤ p.mkQ.range

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
A : Type u_4
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
B : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Module R B
a₁ a₂ : A
⊢ ((inl R A B) (a₁ * a₂)).2 = ((inl R A B) a₁ * (inl R A B) a₂).2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' 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₂
x✝ : ↑(Set.Ici p)
q : Submodule R M
hq : q ∈ Set.Ici p
⊢ ↑((fun p' ↦ ⟨comap p.mkQ p', ⋯⟩) ((fun q ↦ map p.mkQ ↑q) ⟨q, hq⟩)) = ↑⟨q, hq⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
A : Type u_4
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
B : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Module R B
b₁ b₂ : B
⊢ ((inr R A B) (b₁ * b₂)).1 = ((inr R A B) b₁ * (inr R A B) b₂).1

Tactic:
by

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
this : comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)
⊢ span R (⇑f ⁻¹' s) = comap f (span R₂ s)

Tactic:
by

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₃
x : M₃
⊢ x ∈ (f.coprod g).range ↔ x ∈ f.range ⊔ g.range

Tactic:
by

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
⊢ f.ker ≤ span R (⇑f ⁻¹' s)

Tactic:
by

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'
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
hb : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
⊢ ∀ i ∈ J, b i = 0

Tactic:
by

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₂
⊢ IsCompl (inl R M M₂).range (inr R M M₂).range

Tactic:
by

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₂
⊢ Disjoint (inl R M M₂).range (inr R M M₂).range

Tactic:
by

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₂
⊢ p.prod q = map (inl R M M₂) p ⊔ map (inr R M M₂) q

Tactic:
by

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 ∪ ⇑(inr R M M₂) '' t) = (span R s).prod (span R t)

Tactic:
by

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
⊢ span R (⇑f ⁻¹' s) = comap f (span R₂ s)

Tactic:
by

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'
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
⊢ ↥(⨅ i ∈ J, (proj i).ker) ≃ₗ[R] (i : ↑I) → φ ↑i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
r : R
x✝ y : M✝
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M✝
inst✝¹⁰ : Module R M✝
p p' 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₂
R₂ : Type u_5
inst✝⁶ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
f : M ≃ₛₗ[σ₁₂] N
hf : map (↑f) P = Q
x : M ⧸ P
⊢ ∀ (z : M), (Q.mapQ P ↑f.symm ⋯) ((P.mapQ Q ↑f ⋯).toFun (mk z)) = mk z

Tactic:
by

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₂
φ : ι → 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
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

Tactic:
by

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 : ι
⊢ single R φ i = pi (diag i)

Tactic:
by

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:
by

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

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
r : R
x✝ y : M✝
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup M✝
inst✝¹⁰ : Module R M✝
p p' 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₂
R₂ : Type u_5
inst✝⁶ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
f : M ≃ₛₗ[σ₁₂] N
hf : map (↑f) P = Q
x : N ⧸ Q
⊢ ∀ (z : N), (P.mapQ Q ↑f ⋯).toFun ((Q.mapQ P ↑f.symm ⋯) (mk z)) = mk z

Tactic:
by

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 : ι
⊢ proj i ∘ₗ single R φ j = diag j i

Tactic:
by

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).range ≤ f.range.prod g.range

Tactic:
by

Goal state after:
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✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
⊢ f.ker.prod g.ker ≤ (f.coprod g).ker

Tactic:
by

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
⊢ f x = ∑ i, x i • f fun j ↦ if i = j then 1 else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
⊢ ↑(Ico (succ a) b) = ↑(Ioo a b)

Tactic:
by

Goal state after:
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)
I : Set ι
p : (i : ι) → Submodule R (φ i)
⊢ ⨅ i ∈ I, comap (proj i) (p i) = pi I p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b : α
⊢ ↑(Icc (succ a) b) = ↑(Ioc a b)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_5
inst✝¹⁵ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹³ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
R₃ : Type u_8
O : Type u_9
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup O
inst✝⁶ : Module R₃ O
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomInvPair σ₁₃ σ₃₁
inst✝² : RingHomInvPair σ₃₁ σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
S : Submodule R₃ O
e : M ≃ₛₗ[σ₁₂] N
f : N ≃ₛₗ[σ₂₃] O
he : map (↑e) P = Q
hf : map (↑f) Q = S
hef : map (↑(e.trans f)) P = S
x✝ : M ⧸ P
⊢ (equiv P S (e.trans f) hef) x✝ = ((equiv P Q e he).trans (equiv Q S f hf)) x✝

Tactic:
simp only [Quotient.equiv_apply, LinearEquiv.trans_apply, LinearEquiv.coe_trans]

Goal state after:
R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_5
inst✝¹⁵ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹³ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
R₃ : Type u_8
O : Type u_9
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup O
inst✝⁶ : Module R₃ O
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomInvPair σ₁₃ σ₃₁
inst✝² : RingHomInvPair σ₃₁ σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
S : Submodule R₃ O
e : M ≃ₛₗ[σ₁₂] N
f : N ≃ₛₗ[σ₂₃] O
he : map (↑e) P = Q
hf : map (↑f) Q = S
hef : map (↑(e.trans f)) P = S
x✝ : M ⧸ P
⊢ (P.mapQ S (↑f ∘ₛₗ ↑e) ⋯) x✝ = (Q.mapQ S ↑f ⋯) ((P.mapQ Q ↑e ⋯) x✝)
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
⊢ f y ∈ f.range ⊓ g.range

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ ↑(Ico a (succ b)) = ↑(Icc a b)

Tactic:
by

Goal state after:
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)
p : (i : ι) → Submodule R (φ i)
⊢ ⨅ i, comap (proj i) (p i) = pi Set.univ p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ ↑(Ioo a (succ b)) = ↑(Ioc a b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ ↑(Ico (succ a) (succ b)) = ↑(Ioc a b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
⊢ ↑(insert a (Icc (succ a) b)) = ↑(Icc a b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ ↑(insert (succ b) (Icc a b)) = ↑(Icc a (succ b))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ ↑(insert b (Ico a b)) = ↑(Ico a (succ b))

Tactic:
by

Goal state after:
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 : ι
⊢ p i ≤ comap (single R φ i) (pi I p)

Tactic:
by

Goal state after:
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
⊢ (f.coprod g).ker = f.ker.prod g.ker

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
h : a < b
⊢ ↑(insert a (Ico (succ a) b)) = ↑(Ico a b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ ↑(insert (succ b) (Ioc a b)) = ↑(Ioc a (succ b))

Tactic:
by

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✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Module R✝ M₂✝
inst✝⁶ : Module R✝ M₃
inst✝⁵ : Module R✝ M₄
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
C : Submodule R M
h : IsCompl C f.ker
⊢ Function.Injective ⇑(codRestrict f.range f ⋯ ∘ₗ C.subtype)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
h : a < b
⊢ ↑(insert (succ a) (Ioc (succ a) b)) = ↑(Ioc a b)

Tactic:
by

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

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

Tactic:
by

Goal state after:
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)
p : (i : ι) → Submodule R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
⊢ ⨆ i, map (single R φ i) (p i) = pi Set.univ p

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ ↑(Ioo a (succ b)) = ↑(Ioc a b)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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₂
f : M →ₗ[R] M₂
I : Type u_1
x✝ : I → M₂
hx : x✝ ∈ Submodule.pi Set.univ fun x ↦ f.range
⊢ x✝ ∈ (f.compLeft I).range

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : a ≤ b
⊢ ↑(insert b (Ico a b)) = ↑(Ico a (succ b))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : a ≤ b
⊢ ↑(insert (succ b) (Ioc a b)) = ↑(Ioc a (succ b))

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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'
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
⊢ (fun i ↦ (e i) ((c • f) i)) = (RingHom.id R) c • fun i ↦ (e i) (f i)

Tactic:
by

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

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

Tactic:
by

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✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Module R✝ M₂✝
inst✝⁶ : Module R✝ M₃
inst✝⁵ : Module R✝ M₄
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
C : Submodule R M
h : IsCompl C f.ker
⊢ Function.Surjective ⇑(codRestrict f.range f ⋯ ∘ₗ C.subtype)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_5
inst✝¹⁵ : Ring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹³ : RingHomInvPair σ₂₁ σ₁₂
M : Type u_6
N : Type u_7
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R₂ N
P : Submodule R M
Q : Submodule R₂ N
R₃ : Type u_8
O : Type u_9
inst✝⁸ : Ring R₃
inst✝⁷ : AddCommGroup O
inst✝⁶ : Module R₃ O
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomInvPair σ₁₃ σ₃₁
inst✝² : RingHomInvPair σ₃₁ σ₁₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
S : Submodule R₃ O
e : M ≃ₛₗ[σ₁₂] N
f : N ≃ₛₗ[σ₂₃] O
he : map (↑e) P = Q
hf : map (↑f) Q = S
hef : map (↑(e.trans f)) P = S
⊢ equiv P S (e.trans f) hef = (equiv P Q e he).trans (equiv Q S f hf)

Tactic:
by

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'
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)
ι : Type u_4
M : Option ι → Type u_5
inst✝¹ : (i : Option ι) → AddCommMonoid (M i)
inst✝ : (i : Option ι) → Module R (M i)
⊢ ∀ (x y : (i : Option ι) → M i),
    Equiv.piOptionEquivProd.toFun (x + y) = Equiv.piOptionEquivProd.toFun x + Equiv.piOptionEquivProd.toFun y

Tactic:
by

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

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

Tactic:
by

Goal state after: