mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b

pp: case refine_2
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_3
α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
·

Goal state after:
case refine_3
α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1
s : Set Cardinal.{u_1}
h : sInf s = 0
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

pp: case refine_2
s : Set Cardinal.{u_1}
h : s = ∅ ∨ ∃ a ∈ s, a = 0
⊢ sInf s = 0

Tactic:
·

Goal state after:
case refine_1
s : Set Cardinal.{u_1}
h : sInf s = 0
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1.inl
h : sInf ∅ = 0
⊢ ∅ = ∅ ∨ ∃ a ∈ ∅, a = 0

pp: case refine_1.inr
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
·

Goal state after:
case refine_1.inl
h : sInf ∅ = 0
⊢ ∅ = ∅ ∨ ∃ a ∈ ∅, a = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1.inr
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
·

Goal state after:
case refine_1.inr
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2
s : Set Cardinal.{u_1}
h : s = ∅ ∨ ∃ a ∈ s, a = 0
⊢ sInf s = 0

Tactic:
·

Goal state after:
case refine_2
s : Set Cardinal.{u_1}
h : s = ∅ ∨ ∃ a ∈ s, a = 0
⊢ sInf s = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2.inl
⊢ sInf ∅ = 0

pp: case refine_2.inr
s : Set Cardinal.{u_1}
ha : 0 ∈ s
⊢ sInf s = 0

Tactic:
·

Goal state after:
case refine_2.inl
⊢ sInf ∅ = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2.inr
s : Set Cardinal.{u_1}
ha : 0 ∈ s
⊢ sInf s = 0

Tactic:
·

Goal state after:
case refine_2.inr
s : Set Cardinal.{u_1}
ha : 0 ∈ s
⊢ sInf s = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case inl
⊢ lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)

pp: case inr
s : Set Cardinal.{v}
hs : s.Nonempty
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
·

Goal state after:
case inl
⊢ lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case inr
s : Set Cardinal.{v}
hs : s.Nonempty
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
·

Goal state after:
case inr
s : Set Cardinal.{v}
hs : s.Nonempty
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ ∀ c ∈ upperBounds (lift.{u, u_1} '' s), lift.{u, u_1} (sSup s) ≤ c

pp: s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) ∈ upperBounds (lift.{u, u_1} '' s)

Tactic:
·

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ ∀ c ∈ upperBounds (lift.{u, u_1} '' s), lift.{u, u_1} (sSup s) ≤ c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) ∈ upperBounds (lift.{u, u_1} '' s)

Tactic:
·

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) ∈ upperBounds (lift.{u, u_1} '' s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Finite α
⊢ ∃ s, n = s.card

pp: case inr
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
⊢ ∃ s, n = s.card

Tactic:
·

Goal state after:
case inl
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Finite α
⊢ ∃ s, n = s.card
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
⊢ ∃ s, n = s.card

Tactic:
·

Goal state after:
case inr
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
⊢ ∃ s, n = s.card
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ 0 < c

Tactic:
← succ_zero,

Goal state after:
c : Cardinal.{u_1}
⊢ succ 0 ≤ c ↔ 0 < c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1
a b : Cardinal.{u_1}
h : a * b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

pp: case refine_2
a b : Cardinal.{u_1}
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ → a * b < ℵ₀

Tactic:
·

Goal state after:
case refine_1
a b : Cardinal.{u_1}
h : a * b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case pos
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
·

Goal state after:
case pos
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case pos
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
·

Goal state after:
case pos
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg.left
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀

pp: case neg.right
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ b < ℵ₀

Tactic:
·

Goal state after:
case neg.left
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg.right
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ b < ℵ₀

Tactic:
·

Goal state after:
case neg.right
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mp
α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n → ∃ t, ↑t = s ∧ t.card = n

pp: case mpr
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ t.card = n) → #↑s = ↑n

Tactic:
·

Goal state after:
case mp
α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n → ∃ t, ↑t = s ∧ t.card = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mpr
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ t.card = n) → #↑s = ↑n

Tactic:
·

Goal state after:
case mpr
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ t.card = n) → #↑s = ↑n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mp
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) → ∃ h, Fintype.card α = n

pp: case mpr
α : Type u
n : ℕ
⊢ (∃ h, Fintype.card α = n) → ∃ t, ↑t = univ ∧ t.card = n

Tactic:
·

Goal state after:
case mp
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) → ∃ h, Fintype.card α = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mpr
α : Type u
n : ℕ
⊢ (∃ h, Fintype.card α = n) → ∃ t, ↑t = univ ∧ t.card = n

Tactic:
·

Goal state after:
case mpr
α : Type u
n : ℕ
⊢ (∃ h, Fintype.card α = n) → ∃ t, ↑t = univ ∧ t.card = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case pos
α : Type u
s : Set α
a : α
h : a ∈ s
⊢ #↑(insert a s) ≤ #↑s + 1

pp: case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
·

Goal state after:
case pos
α : Type u
s : Set α
a : α
h : a ∈ s
⊢ #↑(insert a s) ≤ #↑s + 1
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
·

Goal state after:
case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) ≤ #↑s + 1
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case inl
α : Type u
A B : Set α
hfin✝ : A.Finite
hlt : A ⊂ B
hfin : Finite ↑B
⊢ #↑A < #↑B

pp: case inr
α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
hinf : Infinite ↑B
⊢ #↑A < #↑B

Tactic:
·

Goal state after:
case inl
α : Type u
A B : Set α
hfin✝ : A.Finite
hlt : A ⊂ B
hfin : Finite ↑B
⊢ #↑A < #↑B
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case inr
α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
hinf : Infinite ↑B
⊢ #↑A < #↑B

Tactic:
·

Goal state after:
case inr
α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
hinf : Infinite ↑B
⊢ #↑A < #↑B
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mp
α : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y, x ≠ y ∧ {x, y} = univ

pp: case mpr
α : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}

Tactic:
·

Goal state after:
case mp
α : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y, x ≠ y ∧ {x, y} = univ
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mpr
α : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}

Tactic:
·

Goal state after:
case mpr
α : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mp
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃! y, y ≠ x

pp: case mpr
α : Type u
x : α
⊢ (∃! y, y ≠ x) → ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
·

Goal state after:
case mp
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃! y, y ≠ x
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mpr
α : Type u
x : α
⊢ (∃! y, y ≠ x) → ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
·

Goal state after:
case mpr
α : Type u
x : α
⊢ (∃! y, y ≠ x) → ∃ x y, x ≠ y ∧ {x, y} = univ
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b c : Cardinal.{u}
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ x < b, a ^ x ≤ c

pp: case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)

Tactic:
·

Goal state after:
a b c : Cardinal.{u}
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ x < b, a ^ x ≤ c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)

Tactic:
·

Goal state after:
case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inl M N) = hM

pp: case e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inr M N), ⋯⟩ ≍ ⟨hN, snd✝⟩

Tactic:
·

Goal state after:
case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inl M N) = hM
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: case pos
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), x • 0 = 0
hb : b = 0
⊢ (g / h) • (a / b) = g • a / h • b

pp: case neg
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
·

Goal state after:
case pos
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), x • 0 = 0
hb : b = 0
⊢ (g / h) • (a / b) = g • a / h • b
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_2
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ (fun x ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α

pp: case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inr M N) = hN

pp: case e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝

Tactic:
·

Goal state after:
case e_4.e_2
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ (fun x ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inr M N) = hN

pp: case e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝

Tactic:
·

Goal state after:
case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inr M N) = hN
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝

Tactic:
·

Goal state after:
case e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f = g ∘ₛₗ ↑e₁₂.symm
x✝ : M₁
⊢ (f ∘ₛₗ ↑e₁₂) x✝ = g x✝

pp: case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f ∘ₛₗ ↑e₁₂ = g
x✝ : M₂
⊢ f x✝ = (g ∘ₛₗ ↑e₁₂.symm) x✝

Tactic:
·

Goal state after:
case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f = g ∘ₛₗ ↑e₁₂.symm
x✝ : M₁
⊢ (f ∘ₛₗ ↑e₁₂) x✝ = g x✝
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f ∘ₛₗ ↑e₁₂ = g
x✝ : M₂
⊢ f x✝ = (g ∘ₛₗ ↑e₁₂.symm) x✝

Tactic:
·

Goal state after:
case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f ∘ₛₗ ↑e₁₂ = g
x✝ : M₂
⊢ f x✝ = (g ∘ₛₗ ↑e₁₂.symm) x✝
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g ∘ₛₗ ↑e₁₂.symm = f
x✝ : M₁
⊢ g x✝ = (f ∘ₛₗ ↑e₁₂) x✝

pp: case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g = f ∘ₛₗ ↑e₁₂
x✝ : M₂
⊢ (g ∘ₛₗ ↑e₁₂.symm) x✝ = f x✝

Tactic:
·

Goal state after:
case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g ∘ₛₗ ↑e₁₂.symm = f
x✝ : M₁
⊢ g x✝ = (f ∘ₛₗ ↑e₁₂) x✝
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g = f ∘ₛₗ ↑e₁₂
x✝ : M₂
⊢ (g ∘ₛₗ ↑e₁₂.symm) x✝ = f x✝

Tactic:
·

Goal state after:
case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g = f ∘ₛₗ ↑e₁₂
x✝ : M₂
⊢ (g ∘ₛₗ ↑e₁₂.symm) x✝ = f x✝
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : f = ↑e₁₂.symm ∘ₛₗ g
x✝ : M₃
⊢ (↑e₁₂ ∘ₛₗ f) x✝ = g x✝

pp: case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : ↑e₁₂ ∘ₛₗ f = g
x✝ : M₃
⊢ f x✝ = (↑e₁₂.symm ∘ₛₗ g) x✝

Tactic:
·

Goal state after:
case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : f = ↑e₁₂.symm ∘ₛₗ g
x✝ : M₃
⊢ (↑e₁₂ ∘ₛₗ f) x✝ = g x✝