mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y ↦ y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝

Tactic:
exact (rightCoset_eq_iff s).symm

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
x : ↥A
i x✝ : ι
⊢ (mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ ↑(addSubgroupOfClosure A b h).repr) ((addSubgroupOfClosure A b h) x✝) =
    ((↑ℤ ↑b.repr).domRestrict (AddSubgroup.toIntSubmodule A)) ((addSubgroupOfClosure A b h) x✝)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
x✝ : ↑(g • ↑s)
x : α
property✝ : x ∈ g • ↑s
⊢ ↑((fun x ↦ ⟨g * ↑x, ⋯⟩) ((fun x ↦ ⟨g⁻¹ * ↑x, ⋯⟩) ⟨x, property✝⟩)) = ↑⟨x, property✝⟩

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α
x✝ : ↥s
g : α
property✝ : g ∈ s
⊢ ↑((fun x ↦ ⟨g✝⁻¹ * ↑x, ⋯⟩) ((fun x ↦ ⟨g✝ * ↑x, ⋯⟩) ⟨g, property✝⟩)) = ↑⟨g, property✝⟩

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
x✝ : ↑(op g • ↑s)
x : α
property✝ : x ∈ op g • ↑s
⊢ ↑((fun x ↦ ⟨↑x * g, ⋯⟩) ((fun x ↦ ⟨↑x * g⁻¹, ⋯⟩) ⟨x, property✝⟩)) = ↑⟨x, property✝⟩

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α
x✝ : ↥s
g : α
property✝ : g ∈ s
⊢ ↑((fun x ↦ ⟨↑x * g✝⁻¹, ⋯⟩) ((fun x ↦ ⟨↑x * g✝, ⋯⟩) ⟨g, property✝⟩)) = ↑⟨g, property✝⟩

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
⊢ (leftRel (s.subgroupOf t)) ⟨(f (Quotient.mk'' b))⁻¹ * b, ⋯⟩ ⟨(f (Quotient.mk'' c))⁻¹ * c, ⋯⟩

Tactic:
leftRel_apply

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
⊢ ⟨(f (Quotient.mk'' b))⁻¹ * b, ⋯⟩⁻¹ * ⟨(f (Quotient.mk'' c))⁻¹ * c, ⋯⟩ ∈ s.subgroupOf t
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : (leftRel (s.subgroupOf t)) b c
⊢ (leftRel s) (f a.1 * ↑b) (f a.1 * ↑c)

Tactic:
leftRel_apply

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
⊢ (f a.1 * ↑b)⁻¹ * (f a.1 * ↑c) ∈ s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_3
s : Set α
⊢ univ.ncard = s.ncard

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
x : α
⊢ Quotient.lift id ⋯ ↑x = x

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ.rangeRestrict a = φ.rangeRestrict b
⊢ a⁻¹ * b ∈ φ.ker

Tactic:
← ker_rangeRestrict,

Goal state after:
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ.rangeRestrict a = φ.rangeRestrict b
⊢ a⁻¹ * b ∈ φ.rangeRestrict.ker
Module: Mathlib.Data.Set.Card

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

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

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

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

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

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: H : Type u_2
I : Type u_3
inst✝¹ : Monoid H
inst✝ : Monoid I
G : Submonoid (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
⊢ ∃ f, G = f.mgraph

Tactic:
simpa using MonoidHom.exists_mrange_eq_mgraph hG₁.surjective
    fun a b h ↦ congr_arg (Prod.snd ∘ G.subtype) (hG₁.injective h)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
x : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ mk x = 0 ↔ x ∈ p

Tactic:
by simpa using (Quotient.eq' p : mk x = 0 ↔ _)

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

Goal state after:
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:
by 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:
by 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:
by 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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ ∀ (m : R) (x : M ⧸ p),
    (↑(lift p.toAddSubgroup f.toAddMonoidHom h)).toFun (m • x) =
      τ₁₂ m • (↑(lift p.toAddSubgroup f.toAddMonoidHom h)).toFun x

Tactic:
by rintro a ⟨x⟩; exact f.map_smulₛₗ a x

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 ≤ comap 0 q

Tactic:
by simp

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

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p.mapQ p (f ^ (k + 1)) h' = p.mapQ p f h ^ (k + 1)

Tactic:
| succ k ih =>

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

Goal state before:
pp: case mk
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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
x✝ : M ⧸ p
x : M
hx : Quot.mk (⇑p.quotientRel) x ∈ comap (p.liftQ f h) q
⊢ Quot.mk (⇑p.quotientRel) x ∈ map p.mkQ (comap f q)

Tactic:
exact ⟨_, hx, rfl⟩

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

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

Tactic:
cases nonempty_fintype ι
  refine iSup_map_single_le.antisymm fun x hx => ?_
  rw [← Finset.univ_sum_single x]
  exact sum_mem_iSup fun i => mem_map_of_mem (hx i trivial)

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 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
⊢ insert a (Icc (a + 1) b) = Icc a b

Tactic:
by
  simpa [succ_eq_add_one] using insert_Icc_succ_left_eq_Icc h

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

Goal state after: