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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v - vecCons y w = vecCons (x - y) (v - w)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Zero α
i : Fin n.succ
⊢ ∀ (i : Fin n), vecCons 0 0 i.succ = 0 i.succ

Tactic:
simp

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

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

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
A : Subgroup G
B : Subgroup H
q : (G × H) ⧸ A.prod B
⊢ ∀ (a : G × H),
    (fun q ↦ Quotient.liftOn₂' q.1 q.2 (fun g h ↦ ↑(g, h)) ⋯)
        ((fun q ↦
            Quotient.liftOn' q
              (fun x ↦
                match x with
                | (g, h) => (↑g, ↑h))
              ⋯)
          (Quotient.mk'' a)) =
      Quotient.mk'' a

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
A : Subgroup G
B : Subgroup H
x✝ : (G ⧸ A) × H ⧸ B
q₁ : G ⧸ A
q₂ : H ⧸ B
⊢ ∀ (a₁ : G) (a₂ : H),
    (fun q ↦
          Quotient.liftOn' q
            (fun x ↦
              match x with
              | (g, h) => (↑g, ↑h))
            ⋯)
        ((fun q ↦ Quotient.liftOn₂' q.1 q.2 (fun g h ↦ ↑(g, h)) ⋯) (Quotient.mk'' a₁, Quotient.mk'' a₂)) =
      (Quotient.mk'' a₁, Quotient.mk'' a₂)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
hns : n ≤ s.ncard
⊢ ∅.ncard ≤ n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ Subtype.val '' ↑t' ⊆ s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (↑t').Finite

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B✝ : Type u_3
C : Type u_4
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A✝
inst✝¹² : Algebra R A✝
inst✝¹¹ : Semiring B✝
inst✝¹⁰ : Algebra R B✝
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
S : Type u_5
T : Type u_6
A : Type u_7
B : Type u_8
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring S
inst✝⁴ : Semiring T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R A
inst✝ : Algebra R B
l : S ≃ₐ[R] A
r : T ≃ₐ[R] B
⊢ ∀ (x : R), (l.toRingEquiv.prodCongr r.toRingEquiv) ((algebraMap R (S × T)) x) = (algebraMap R (A × B)) x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (↑t').ncard = t'.card

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
hs : ∅.Finite
⊢ ∅.ncard ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
x✝ : G
⊢ ((((map M (Subgroup.map (mk' N) M) (mk' N) ⋯).comp (quotientQuotientEquivQuotientAux N M h)).comp
            (mk' (Subgroup.map (mk' N) M))).comp
        (mk' N))
      x✝ =
    (((MonoidHom.id ((G ⧸ N) ⧸ Subgroup.map (mk' N) M)).comp (mk' (Subgroup.map (mk' N) M))).comp (mk' N)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
x✝ : G
⊢ (((quotientQuotientEquivQuotientAux N M h).comp (map M (Subgroup.map (mk' N) M) (mk' N) ⋯)).comp (mk' M)) x✝ =
    ((MonoidHom.id (G ⧸ M)).comp (mk' M)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
φ : G →* H
N : Subgroup G
hn : N.Normal
H' : Subgroup (G ⧸ N)
⊢ H' ≤ (mk' N).range

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝ : Group G
⊢ Subsingleton (G ⧸ ⊤)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ (↑t).ncard = t.card

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H✝ : Type v
inst✝³ : Group H✝
M : Type x
inst✝² : Monoid M
φ : G →* H✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝ : ↥(domRestrictHom H A).ker
⊢ (fun f ↦ ⟨f.comp (mk' H), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨f, hf⟩ => lift H f ⋯)
        x✝) =
    x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H✝ : Type v
inst✝³ : Group H✝
M : Type x
inst✝² : Monoid M
φ : G →* H✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝¹ : G ⧸ H →* A
x✝ : G
⊢ (((fun x ↦
              match x with
              | ⟨f, hf⟩ => lift H f ⋯)
            ((fun f ↦ ⟨f.comp (mk' H), ⋯⟩) x✝¹)).comp
        (mk' H))
      x✝ =
    (x✝¹.comp (mk' H)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard.toNat = 2 ↔ s.encard = 2

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard.toNat = 3 ↔ s.encard = 3

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H✝ : Type v
inst✝³ : Group H✝
M : Type x
inst✝² : Monoid M
φ : G →* H✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝² x✝¹ : ↥(domRestrictHom H A).ker
x✝ : G
⊢ ((match x✝² * x✝¹ with
          | ⟨f, hf⟩ => lift H f ⋯).comp
        (mk' H))
      x✝ =
    (((match x✝² with
            | ⟨f, hf⟩ => lift H f ⋯) *
            match x✝¹ with
            | ⟨f, hf⟩ => lift H f ⋯).comp
        (mk' H))
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard.toNat = 4 ↔ s.encard = 4

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
h✝ : IsEmpty α
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
⊢ (Set.range g)ᶜ.ncard ≤ 1

Tactic:
· -- we must show that any two elements `a` and `b` missed by `g` are equal
    rw [Set.ncard_le_one]
    simp only [Set.mem_compl_iff, Set.mem_range, not_exists, ← ne_eq]
    intro a ha b hb
    -- there is a collision between `a` and `g (f a)`, and between `b` and `g (f b)`
    simpa [(ha (f b)).symm] using congrArg (a ∈ ·) (h a (g (f a)) b (g (f b))
      (hf (f a)).symm (hf (f b)).symm (ha (f a)).symm (hb (f b)).symm)

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

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' : Submodule R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
⊢ ∀ (x y : M), Quotient.mk (x + y) = Quotient.mk x + Quotient.mk y

Tactic:
simp

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

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' : Submodule R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
⊢ ∀ (m : R) (x : M), Quotient.mk (m • x) = (RingHom.id R) m • Quotient.mk x

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ f (f.symm w) = w

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ f (f.symm x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ f (f.symm y) = y

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ f (f.symm z) = z

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : RightInverse g ⇑f
x : (ker f).Quotient
⊢ f (g ((kerLift f) x)) = (kerLift f) x

Tactic:
hf

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : RightInverse g ⇑f
x : (ker f).Quotient
⊢ (kerLift f) x = (kerLift f) x
Module: Mathlib.RingTheory.Congruence.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ ⇑c = ⇑d ↔ c = d

Tactic:
simp

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
⊢ p.toAddSubgroup ≠ ⊤ ↔ p ≠ ⊤

Tactic:
simp

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
⊢ p.toAddSubgroup = ⊤ ↔ p = ⊤

Tactic:
simp

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
ι : Type u_5
N : ι → Type u_6
inst✝¹ : (i : ι) → AddCommGroup (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M →ₗ[R] N i
p : Submodule R M
h : ∀ (i : ι), p ≤ (f i).ker
x : M
i : ι
⊢ ((LinearMap.pi fun i ↦ p.liftQ (f i) ⋯) ∘ₗ p.mkQ) x i = (p.liftQ (LinearMap.pi f) ⋯ ∘ₗ p.mkQ) x i

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
⊢ sSup (DFunLike.coe '' S) x y ↔ ∃ c ∈ S, c x y

Tactic:
simp

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
x✝ : M
⊢ x✝ ∈ p.mkQ.ker ↔ x✝ ∈ p

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ (ringConGen (r on ⇑f)).comap (f.symm.toNonUnitalRingHom.comp f.toNonUnitalRingHom) ≤ ringConGen (r on ⇑f)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: ι : Type x
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : (i : ι) → φ i
x✝ : ι
⊢ (∑ i, Pi.single i (v i)) x✝ = v x✝

Tactic:
simp

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 : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
⊢ comap (single R φ i) (⨅ i ∈ J, (proj i).ker) = ⊤

Tactic:
simp only [← ker_comp, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
⊢ ∀ ⦃x : φ i⦄, x ∈ ⊤ → ∀ i_1 ∈ J, (proj i_1 ∘ₗ single R φ i) x = 0
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 ≤ comap 0 q

Tactic:
simp

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₂
h : p ≤ comap 0 q
x✝ : M
⊢ (p.mapQ q 0 h ∘ₛₗ p.mkQ) x✝ = (0 ∘ₛₗ p.mkQ) x✝

Tactic:
simp

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₂
R₃ : Type u_5
M₃ : Type u_6
inst✝³ : Ring R₃
inst✝² : AddCommGroup M₃
inst✝¹ : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : p ≤ comap f (comap g p₃)
x✝ : M
⊢ (p.mapQ p₃ (g ∘ₛₗ f) h ∘ₛₗ p.mkQ) x✝ = ((p₂.mapQ p₃ g hg ∘ₛₗ p.mapQ p₂ f hf) ∘ₛₗ p.mkQ) x✝

Tactic:
simp

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
h : p ≤ comap LinearMap.id p
x✝ : M
⊢ (p.mapQ p LinearMap.id h ∘ₗ p.mkQ) x✝ = (LinearMap.id ∘ₗ p.mkQ) x✝

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₂
x✝ : M
⊢ ∀ ⦃a₂ : M⦄, (inl R M M₂) x✝ = (inl R M M₂) a₂ → x✝ = a₂

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₂
x✝ : M₂
⊢ ∀ ⦃a₂ : M₂⦄, (inr R M M₂) x✝ = (inr R M M₂) a₂ → x✝ = a₂

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₂
x✝ : M × M₂
⊢ (fst R M M₂) x✝ = (id.coprod 0) x✝

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₂
x✝ : M × M₂
⊢ (snd R M M₂) x✝ = (coprod 0 id) x✝

Tactic:
simp

Goal state after:
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
⊢ ∀ i ∈ J, (if h : i ∈ I then proj ⟨i, h⟩ else 0) b = 0

Tactic:
intro j

Goal state after:
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 : ι
⊢ j ∈ J → (if h : j ∈ I then proj ⟨j, h⟩ else 0) b = 0
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
⊢ ((factor H2 ∘ₗ factor H1) ∘ₗ p.mkQ) x✝ = (factor ⋯ ∘ₗ p.mkQ) x✝

Tactic:
simp

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

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₄
fst✝ : M₃
snd✝ : M₄
⊢ (fst✝, snd✝) ∈ (f.prodMap g).range ↔ (fst✝, snd✝) ∈ f.range.prod g.range

Tactic:
simp

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

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

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

Goal state after:
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₂
x : M
y : M₂
⊢ (x, 0) + (0, y) = (x, y)

Tactic:
simp

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

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

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)
x : (i : ι) → φ i
⊢ x ∈ ⨅ i ∈ I, comap (proj i) (p i) ↔ x ∈ pi I p

Tactic:
simp

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)
x : (i : ι) → φ i
⊢ x ∈ ⨅ i, comap (proj i) (p i) ↔ x ∈ pi Set.univ p

Tactic:
simp

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

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

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

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

Goal state after: