mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ 1 + 1 + 1 + 1 = 4

Tactic:
grind

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ z ∉ {w}

Tactic:
grind

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ y ∉ {z, w}

Tactic:
grind

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ x ∉ {y, z, w}

Tactic:
grind

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

Goal state before:
pp: case e'_2
k : ℕ
⊢ {i | i < k}.encard = (↑(Finset.range k)).encard

Tactic:
rw [Finset.coe_range, Iio_def]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case pos
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
heq : j = i
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j

pp: case neg
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
heq : ¬j = i
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j

Tactic:
· subst heq
        simp

Goal state after:
case neg
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
heq : ¬j = i
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card α = 0 ↔ IsEmpty α

Tactic:
have := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card, Fintype.card_eq_zero_iff]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case pos
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
heq : j = i
⊢ Function.update x i 1 j = 1

pp: case neg
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
heq : ¬j = i
⊢ Function.update x i 1 j = 1

Tactic:
· subst heq
        simp

Goal state after:
case neg
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
heq : ¬j = i
⊢ Function.update x i 1 j = 1
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑(t \ s) ≤ 0
⊢ t ⊆ s

Tactic:
← sdiff_eq_empty,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑(t \ s) ≤ 0
⊢ t \ s = ∅
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ ↑(insert a s).ncard ≤ ↑s.ncard + 1

Tactic:
rw [hs.cast_ncard_eq, (hs.insert _).cast_ncard_eq]

Goal state after:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).encard ≤ s.encard + 1
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ a • ↑s ↔ x ∈ ↑s

Tactic:
by simp [mem_leftCoset_iff, mul_mem_cancel_left (s.inv_mem ha)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ x⁻¹ * y ∈ s.prod s' ↔ x.1⁻¹ * y.1 ∈ s ∧ x.2⁻¹ * y.2 ∈ s'

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ y * x⁻¹ ∈ s.prod s' ↔ y.1 * x.1⁻¹ ∈ s ∧ y.2 * x.2⁻¹ ∈ s'

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // Quotient.mk'' x = L } ≃ { x // Quotient.mk'' x = L }

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ ↑(t \ s).ncard + ↑s.ncard = t.encard

Tactic:
(ht.subset h).cast_ncard_eq,

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ ↑(t \ s).ncard + s.encard = t.encard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ ⋃ x, Quotient.out x • ↑H = ⋃ x, Quotient.out x • ↑H

Tactic:
rfl

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

Goal state before:
pp: case h
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ (rangeKerLift φ) ↑g = ⟨φ g, ⋯⟩

Tactic:
rfl

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' 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:
rfl

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' 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:
rfl

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

Tactic:
rfl

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

Goal state before:
pp: A : Type u
inst✝ : CommGroup A
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ (MulEquiv.refl (A ⧸ (zpowGroupHom n).range)) (Quotient.mk'' (Quotient.out x)) =
    (equivQuotientZPowOfEquiv (MulEquiv.refl A) n) (Quotient.mk'' (Quotient.out x))

Tactic:
rfl

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

Goal state before:
pp: A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ ((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n)) (Quotient.mk'' (Quotient.out x)) =
    (equivQuotientZPowOfEquiv (e.trans d) n) (Quotient.mk'' (Quotient.out x))

Tactic:
rfl

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

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ (s = ∅ ∨ ∃ a, s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
grind

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

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

Tactic:
Finset.one_lt_card,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (∃ a ∈ hs.toFinset, ∃ b ∈ hs.toFinset, a ≠ b) ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : 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}
this : ∀ (a b : α), f a = f b → a ≠ b → a = x ∨ a = g (f x)
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
grind

Goal state after:
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
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
grind

Goal state after:
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
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
grind

Goal state after:
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
hb : b ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
grind

Goal state after:
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
hb : b ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
grind

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

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 y : M
⊢ -x + y ∈ p.toAddSubgroup ↔ -x + y ∈ p

Tactic:
rfl

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
S : Type u_3
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
P : Submodule R M
⊢ mk 0 = 0

Tactic:
rfl

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
S : Type u_3
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
P : Submodule R M
x✝¹ x✝ : M
⊢ mk (x✝¹ + x✝) = mk x✝¹ + mk x✝

Tactic:
rfl

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 : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
a b : M
⊢ p.quotientRel a b ↔ p.quotientRel ((Equiv.refl M) a) ((Equiv.refl M) b)

Tactic:
rfl

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

Goal state before:
pp: case mk.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' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
h : p = p'
x✝ : M ⧸ p
x : M
y✝ : M ⧸ p
y : M
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑p.quotientRel) x + Quot.mk (⇑p.quotientRel) y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑p.quotientRel) x) +
      (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑p.quotientRel) y)

Tactic:
rfl

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

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' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
h : p = p'
x : R
x✝ : M ⧸ p
y : M
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (x • Quot.mk (⇑p.quotientRel) y) =
    (RingHom.id R) x • (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑p.quotientRel) y)

Tactic:
rfl

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

Tactic:
rfl

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 : P
⊢ (kerLift f) ((toQuotient ∘ g) x) = f (g x)

Tactic:
rfl

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

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

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

Tactic:
rfl

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✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
ι : Sort u_5
f : ι → RingCon R
⊢ iInf (DFunLike.coe ∘ f) = ⨅ i, ⇑(f i)

Tactic:
Function.comp_def

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
ι : Sort u_5
f : ι → RingCon R
⊢ ⨅ x, ⇑(f x) = ⨅ i, ⇑(f i)
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
⊢ Subsingleton c.Quotient ↔ c = ⊤

Tactic:
simp [RingCon.Quotient]

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

Tactic:
rfl

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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
x : M
⊢ (p.mapQ q f h ∘ₛₗ p.mkQ) x = (q.mkQ ∘ₛₗ f) x

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
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₂
y : M
⊢ (snd R M M₂) ((inl R M M₂) y) = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
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₂
y : M₂
⊢ (fst R M M₂) ((inr R M M₂) y) = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2
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 : ι
hj : j ∈ I
⊢ eval ⟨j, ⋯⟩ b = id b ⟨j, hj⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
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 : ι
hb : ∀ i ∈ J, b i = 0
h : j ∈ I
⊢ (proj ⟨j, h⟩) ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j

Tactic:
rfl

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₃
⊢ comap f ⊥ ⊓ comap g ⊥ = f.ker ⊓ g.ker

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case e'_2.e'_1
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ x = id x

Tactic:
rfl

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:
simpa [← ker_eq_bot, ker_codRestrict, ker_comp, ← disjoint_iff_comap_eq_bot] using h.disjoint

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x✝¹ y✝ : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x y : ↥(p.compatibleMaps q)
x✝ : M
⊢ (p.mapQ q ↑(x + y) ⋯ ∘ₗ p.mkQ) x✝ = ((p.mapQ q ↑x ⋯ + p.mapQ q ↑y ⋯) ∘ₗ p.mkQ) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x y : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
c : R
f : ↥(p.compatibleMaps q)
x✝ : M
⊢ (p.mapQ q ↑(c • f) ⋯ ∘ₗ p.mkQ) x✝ = (((RingHom.id R) c • p.mapQ q ↑f ⋯) ∘ₗ p.mkQ) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case fst
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)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : α ⊕ β → M
x✝ : α
⊢ ((Equiv.sumArrowEquivProdArrow α β M).toFun (f + g)).1 x✝ =
    ((Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g).1 x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case snd
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)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : α ⊕ β → M
x✝ : β
⊢ ((Equiv.sumArrowEquivProdArrow α β M).toFun (f + g)).2 x✝ =
    ((Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g).2 x✝

Tactic:
rfl

Goal state after: