mathlib-initiative/mathlib-tactics huggingface dataset:
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' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
x : G
hx : x ∈ A
⊢ (((quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯)).comp (mk' (A'.subgroupOf A))) ⟨x, hx⟩ =
    ((MonoidHom.id (↥A ⧸ A'.subgroupOf A)).comp (mk' (A'.subgroupOf A))) ⟨x, hx⟩

Tactic:
;

Goal state after:
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' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
x : G
hx : x ∈ A
⊢ (((quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯)).comp (mk' (A'.subgroupOf A))) ⟨x, hx⟩ =
    ((MonoidHom.id (↥A ⧸ A'.subgroupOf A)).comp (mk' (A'.subgroupOf A))) ⟨x, hx⟩
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' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
x : G
hx : x ∈ B
⊢ (((quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯)).comp (mk' (B'.subgroupOf B))) ⟨x, hx⟩ =
    ((MonoidHom.id (↥B ⧸ B'.subgroupOf B)).comp (mk' (B'.subgroupOf B))) ⟨x, hx⟩

Tactic:
;

Goal state after:
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' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
x : G
hx : x ∈ B
⊢ (((quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯)).comp (mk' (B'.subgroupOf B))) ⟨x, hx⟩ =
    ((MonoidHom.id (↥B ⧸ B'.subgroupOf B)).comp (mk' (B'.subgroupOf B))) ⟨x, hx⟩
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
f : A →ₐ[R] B
g : A →ₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Tactic:
;

Goal state after:
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
f : A →ₐ[R] B
g : A →ₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝
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
f : A →ₐ[R] B
g : A →ₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝

Tactic:
;

Goal state after:
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
f : A →ₐ[R] B
g : A →ₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.ncard = 1

Tactic:
;

Goal state after:
α : Type u_1
a : α
⊢ {a}.ncard = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case e'_2
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (fun a ↦ a ∉ hs.toFinset ∧ insert a hs.toFinset = ht.toFinset) = fun a ↦ a ∉ s ∧ insert a s = t

Tactic:
;

Goal state after:
case e'_2
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (fun a ↦ a ∉ hs.toFinset ∧ insert a hs.toFinset = ht.toFinset) = fun a ↦ a ∉ s ∧ insert a s = t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.one_lt_card, Finite.mem_toFinset]

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✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
φ_surjective : Surjective ⇑φ
⊢ N.subgroupOf H = φ.ker

Tactic:
by simp [φ, ← comap_ker]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < s.ncard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
by
  rw [one_lt_ncard hs]
  simp only [exists_and_left]

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

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

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

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

Goal state after:
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✝
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
by_cases hb : b ∈ Set.range g

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
by_cases hb : b ∈ Set.range g

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
Module: Mathlib.LinearAlgebra.Quotient.Defs

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
b✝ : M ⧸ p
x : M
⊢ ∃ a, p.mkQ a = Quot.mk (⇑p.quotientRel) x

Tactic:
;

Goal state after:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
b✝ : M ⧸ p
x : M
⊢ ∃ a, p.mkQ a = Quot.mk (⇑p.quotientRel) x
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
d : Con N
e : M ≃* N
h : c = comap ⇑e ⋯ d
x✝ : c.Quotient
x : M
y✝ : c.Quotient
y : M
⊢ (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x * Quot.mk (⇑c.toSetoid) y) =
    (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x) * (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) y)

Tactic:
;

Goal state after:
case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
d : Con N
e : M ≃* N
h : c = comap ⇑e ⋯ d
x✝ : c.Quotient
x : M
y✝ : c.Quotient
y : M
⊢ (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x * Quot.mk (⇑c.toSetoid) y) =
    (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x) * (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) y)
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
w✝ : c.Quotient
y : M
hy : (c.lift f H) (Quot.mk (⇑c.toSetoid) y) = x
⊢ x ∈ MonoidHom.mrange f

Tactic:
;

Goal state after:
case mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
w✝ : c.Quotient
y : M
hy : (c.lift f H) (Quot.mk (⇑c.toSetoid) y) = x
⊢ x ∈ MonoidHom.mrange f
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mk
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
x y : (ker f).Quotient
a✝ : M
h : (kerLift f).mrangeRestrict (Quot.mk (⇑(ker f).toSetoid) a✝) = (kerLift f).mrangeRestrict y
⊢ (kerLift f) (Quot.mk (⇑(ker f).toSetoid) a✝) = (kerLift f) y

Tactic:
;

Goal state after:
case mk
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
x y : (ker f).Quotient
a✝ : M
h : (kerLift f).mrangeRestrict (Quot.mk (⇑(ker f).toSetoid) a✝) = (kerLift f).mrangeRestrict y
⊢ (kerLift f) (Quot.mk (⇑(ker f).toSetoid) a✝) = (kerLift f) y
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mk.mk
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
x y : (ker f).Quotient
a✝¹ a✝ : M
h :
  (kerLift f).mrangeRestrict (Quot.mk (⇑(ker f).toSetoid) a✝¹) =
    (kerLift f).mrangeRestrict (Quot.mk (⇑(ker f).toSetoid) a✝)
⊢ (kerLift f) (Quot.mk (⇑(ker f).toSetoid) a✝¹) = (kerLift f) (Quot.mk (⇑(ker f).toSetoid) a✝)

Tactic:
;

Goal state after:
case mk.mk
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
x y : (ker f).Quotient
a✝¹ a✝ : M
h :
  (kerLift f).mrangeRestrict (Quot.mk (⇑(ker f).toSetoid) a✝¹) =
    (kerLift f).mrangeRestrict (Quot.mk (⇑(ker f).toSetoid) a✝)
⊢ (kerLift f) (Quot.mk (⇑(ker f).toSetoid) a✝¹) = (kerLift f) (Quot.mk (⇑(ker f).toSetoid) a✝)
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
x✝ : ↥(MonoidHom.mrange (kerLift f))
z : (ker f).Quotient
⊢ (kerLift f).mrangeRestrict z = ⟨(kerLift f) z, ⋯⟩

Tactic:
;

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
x✝ : ↥(MonoidHom.mrange (kerLift f))
z : (ker f).Quotient
⊢ (kerLift f).mrangeRestrict z = ⟨(kerLift f) z, ⋯⟩
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 : P
⊢ (kerLift f) ((toQuotient ∘ g) x) = f (g x)

Tactic:
;

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 : P
⊢ (kerLift f) ((toQuotient ∘ g) x) = f (g x)
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 : M →* P
c d : Con M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a * ↑↑b) = d.mk' (a * b)

Tactic:
;

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 : M →* P
c d : Con M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a * ↑↑b) = d.mk' (a * b)
Module: Mathlib.RingTheory.Congruence.Defs

Goal state before:
pp: case mk
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
d : RingCon R
toCon✝ : Con R
add'✝ : ∀ {w x y z : R}, toCon✝.toSetoid w x → toCon✝.toSetoid y z → toCon✝.toSetoid (w + y) (x + z)
⊢ (fun c ↦ c.toCon) { toCon := toCon✝, add' := add'✝ } = (fun c ↦ c.toCon) d → { toCon := toCon✝, add' := add'✝ } = d

Tactic:
;

Goal state after:
case mk
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
d : RingCon R
toCon✝ : Con R
add'✝ : ∀ {w x y z : R}, toCon✝.toSetoid w x → toCon✝.toSetoid y z → toCon✝.toSetoid (w + y) (x + z)
⊢ (fun c ↦ c.toCon) { toCon := toCon✝, add' := add'✝ } = (fun c ↦ c.toCon) d → { toCon := toCon✝, add' := add'✝ } = d
Module: Mathlib.RingTheory.Congruence.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
H : ∀ (x y : R), c x y ↔ d x y
x✝¹ x✝ : R
⊢ c x✝¹ x✝ ↔ d x✝¹ x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
H : ∀ (x y : R), c x y ↔ d x y
x✝¹ x✝ : R
⊢ c x✝¹ x✝ ↔ d x✝¹ x✝
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
⊢ Nonempty (Unique (M ⧸ ⊤))

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Nonempty (Unique (M ⧸ ⊤))
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case mk
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
a : R
x✝ : M ⧸ p
x : M
⊢ (↑(lift p.toAddSubgroup f.toAddMonoidHom h)).toFun (a • Quot.mk (⇑p.quotientRel) x) =
    τ₁₂ a • (↑(lift p.toAddSubgroup f.toAddMonoidHom h)).toFun (Quot.mk (⇑p.quotientRel) x)

Tactic:
;

Goal state after:
case mk
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
a : R
x✝ : M ⧸ p
x : M
⊢ (↑(lift p.toAddSubgroup f.toAddMonoidHom h)).toFun (a • Quot.mk (⇑p.quotientRel) x) =
    τ₁₂ a • (↑(lift p.toAddSubgroup f.toAddMonoidHom h)).toFun (Quot.mk (⇑p.quotientRel) x)
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
x✝ : M
⊢ (p.liftQ f h ∘ₛₗ p.mkQ) x✝ = f x✝

Tactic:
;

Goal state after:
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
x✝ : M
⊢ (p.liftQ f h ∘ₛₗ p.mkQ) x✝ = f x✝
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
h : (sInf S).toSetoid x y
r : Setoid R
x✝ : r ∈ (fun x ↦ x.toSetoid) '' S
c : RingCon R
hS : c ∈ S
hr : (fun x ↦ x.toSetoid) c = r
⊢ ((fun x ↦ x.toSetoid) c) x y

Tactic:
;

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
h : (sInf S).toSetoid x y
r : Setoid R
x✝ : r ∈ (fun x ↦ x.toSetoid) '' S
c : RingCon R
hS : c ∈ S
hr : (fun x ↦ x.toSetoid) c = r
⊢ ((fun x ↦ x.toSetoid) c) x y
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝

Tactic:
;

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝

Tactic:
;

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝
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)
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
⊢ c ∈ (pi f).ker ↔ c ∈ ⨅ i, (f i).ker

Tactic:
;

Goal state after:
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)
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
⊢ c ∈ (pi f).ker ↔ c ∈ ⨅ i, (f i).ker
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
x✝ : M ⧸ p
x : M
⊢ Quot.mk (⇑p.quotientRel) x ∈ p.mkQ.range

Tactic:
;

Goal state after:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x✝ : M ⧸ p
x : M
⊢ Quot.mk (⇑p.quotientRel) x ∈ p.mkQ.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
p : Submodule R M
x✝ : M
⊢ x✝ ∈ p.mkQ.ker ↔ x✝ ∈ p

Tactic:
;

Goal state after:
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
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)
x✝¹ : M₂
x✝ : ι
⊢ (pi fun x ↦ 0) x✝¹ x✝ = 0 x✝¹ x✝

Tactic:
;

Goal state after:
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)
x✝¹ : M₂
x✝ : ι
⊢ (pi fun x ↦ 0) x✝¹ x✝ = 0 x✝¹ x✝
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)
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : SMul R M
inst✝³ : SMul R N
inst✝² : Module S M
inst✝¹ : Module S N
inst✝ : CompatibleSMul M N R S
f : M →ₗ[S] ι → N
r : R
m : M
i : ι
⊢ f (r • m) i = (r • f m) i

Tactic:
;

Goal state after:
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)
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : SMul R M
inst✝³ : SMul R N
inst✝² : Module S M
inst✝¹ : Module S N
inst✝ : CompatibleSMul M N R S
f : M →ₗ[S] ι → N
r : R
m : M
i : ι
⊢ f (r • m) i = (r • f m) i
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:
;

Goal state after:
ι : 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✝
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : IsField R
a✝ : R
ha : a✝ ≠ 0
x✝¹ x✝ : R
hb : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
⊢ x✝¹ = x✝

Tactic:
by
    obtain ⟨x, hx⟩ := h.mul_inv_cancel ha
    simpa [mul_assoc, hx] using congr_arg (· * x) hb

Goal state after: