mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x → ∀ (i : ℕ), c i ≤ x

pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ (∀ (i : ℕ), c i ≤ x) → ωSup c ≤ x

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x → ∀ (i : ℕ), c i ≤ x

case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ (∀ (i : ℕ), c i ≤ x) → ωSup c ≤ x
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f ≤ ⨆ n, (⇑f)^[n] ⊥

Tactic:
apply lfp_le_fixed

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ f (⨆ n, (⇑f)^[n] ⊥) = ⨆ n, (⇑f)^[n] ⊥
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma \ mb ∈ a \ b

Tactic:
simp [sdiff_def]; aesop

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a \ b).get hab = a.get ⋯ \ b.get ⋯

Tactic:
simp [sdiff_def]; aesop

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
h : y ≤ z
⊢ f y ≤ cSup c

Tactic:
obtain hyz | rfl := le_iff_lt_or_eq.1 h

Goal state after:
case cSup_mem.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
h : y ≤ z
hyz : y < z
⊢ f y ≤ cSup c

case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
⊢ f y ≤ cSup c
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
g : α → β
hg : ωScottContinuous g
f : α → β
hf : ωScottContinuous f
⊢ ωScottContinuous f

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous g

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
g : α → β
hg : ωScottContinuous g
f : α → β
hf : ωScottContinuous f
⊢ ωScottContinuous f

case inr
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous g
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x) → ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x

pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x) → ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x) → ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x

case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x) → ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ ((c.map g).map (Pi.evalOrderHom b)) i
j : ℕ
hb : (c.map f) j = Part.some b
⊢ y ∈ x

Tactic:
simp only [Part.eq_some_iff, Chain.coe_map, Function.comp_apply] at hy hb

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ (Pi.evalOrderHom b) (g (c i))
j : ℕ
hb : b ∈ f (c j)
⊢ y ∈ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z) → ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z

pp: case mpr
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z) → ∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z) → ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z

case mpr
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z) → ∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case refine_1
α β : Type u
⊢ ∀ (a b : Cardinal.{u}), lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

pp: case refine_2
α β : Type u
⊢ ∀ (a : Cardinal.{u}),
    ∀ b < (OrderEmbedding.ofMapLEIff lift.{v, u} ?refine_1).ltEmbedding a,
      b ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ?refine_1).ltEmbedding

Tactic:
<;>

Goal state after:
case refine_1
α β : Type u
⊢ ∀ (a b : Cardinal.{u}), lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

case refine_2
α β : Type u
⊢ ∀ (a : Cardinal.{u}),
    ∀ b < (OrderEmbedding.ofMapLEIff lift.{v, u} ?refine_1).ltEmbedding a,
      b ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ?refine_1).ltEmbedding
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ ((c.map { toFun := g, monotone' := ⋯ }).map ↑(f (c i))) j ≤
    (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ }) (max i j)

Tactic:
apply apply_mono

Goal state after:
case a.h₁
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ f (c i) ≤ f (c.toOrderHom (max i j))

case a.h₂
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ (c.map { toFun := g, monotone' := ⋯ }).toOrderHom j ≤ g (c.toOrderHom (max i j))
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α✝ β✝ : Type u
a b : Cardinal.{u}
α β : Type u
⊢ #α * #β = 0 → #α = 0 ∨ #β = 0

Tactic:
simpa only [mul_def, mk_eq_zero_iff, isEmpty_prod] using id

Goal state after:
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

pp: case inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
<;>

Goal state after:
case inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

case inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case zero
⊢ lift.{u, v} ↑0 = ↑0

pp: case succ
n✝ : ℕ
a✝ : lift.{u, v} ↑n✝ = ↑n✝
⊢ lift.{u, v} ↑(n✝ + 1) = ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
⊢ lift.{u, v} ↑0 = ↑0

case succ
n✝ : ℕ
a✝ : lift.{u, v} ↑n✝ = ↑n✝
⊢ lift.{u, v} ↑(n✝ + 1) = ↑(n✝ + 1)
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case a
m n : ℕ∞
⊢ ↑(m + n) ∈ Iic ℵ₀

pp: case a
m n : ℕ∞
⊢ ↑m + ↑n ∈ Iic ℵ₀

pp: case a
m n : ℕ∞
⊢ toENat ↑(m + n) = toENat (↑m + ↑n)

Tactic:
<;>

Goal state after:
case a
m n : ℕ∞
⊢ ↑(m + n) ∈ Iic ℵ₀

case a
m n : ℕ∞
⊢ ↑m + ↑n ∈ Iic ℵ₀

case a
m n : ℕ∞
⊢ toENat ↑(m + n) = toENat (↑m + ↑n)
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ → φ₁₂.CompTriple φ₃ φ₁₂₃

pp: case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃ → φ₁.CompTriple φ₂₃ φ₁₂₃

Tactic:
<;>

Goal state after:
case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ → φ₁₂.CompTriple φ₃ φ₁₂₃

case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃ → φ₁.CompTriple φ₂₃ φ₁₂₃
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ ¬¬Nontrivial α ↔ Nontrivial α

Tactic:
Classical.not_not

Goal state after:
α : Type u
⊢ Nontrivial α ↔ Nontrivial α
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case e'_2
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ x = g⁻¹ • (fun x ↦ g • x) x

pp: case e'_3
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ y = g⁻¹ • (fun x ↦ g • x) y

Tactic:
<;>

Goal state after:
case e'_2
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ x = g⁻¹ • (fun x ↦ g • x) x

case e'_3
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ y = g⁻¹ • (fun x ↦ g • x) y
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:
rcases h with rfl | ⟨a, ha, rfl⟩
    · exact Cardinal.sInf_empty
    · exact eq_bot_iff.2 (csInf_le' ha)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift.{u, v} (iInf f) = ⨅ i, lift.{u, v} (f i)

Tactic:
unfold iInf
  convert! lift_sInf (range f)
  simp_rw [← comp_apply (f := lift), range_comp]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2.inl
b : Cardinal.{u_1}
⊢ 0 * b < ℵ₀

pp: case refine_2.inr.inl
a : Cardinal.{u_1}
⊢ a * 0 < ℵ₀

pp: case refine_2.inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b < ℵ₀

Tactic:
<;>

Goal state after:
case refine_2.inl
b : Cardinal.{u_1}
⊢ 0 * b < ℵ₀

case refine_2.inr.inl
a : Cardinal.{u_1}
⊢ a * 0 < ℵ₀

case refine_2.inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n c : ℕ
h : ↑c ≤ ↑n
⊢ ∃ m ≤ n, ↑c = ↑m

Tactic:
exact ⟨c, mod_cast h, rfl⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case e'_2
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑(f ⁻¹' s) = lift.{u, u} #↑(f ⁻¹' s)

pp: case e'_3
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑s = lift.{u, u} #↑s

Tactic:
<;>

Goal state after:
case e'_2
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑(f ⁻¹' s) = lift.{u, u} #↑(f ⁻¹' s)

case e'_3
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑s = lift.{u, u} #↑s
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ ((x✝² • x✝¹) • x✝).1 = (x✝² • x✝¹ • x✝).1

pp: case snd
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ ((x✝² • x✝¹) • x✝).2 = (x✝² • x✝¹ • x✝).2

Tactic:
<;>

Goal state after:
case fst
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ ((x✝² • x✝¹) • x✝).1 = (x✝² • x✝¹ • x✝).1

case snd
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ ((x✝² • x✝¹) • x✝).2 = (x✝² • x✝¹ • x✝).2
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a : M
x : α × β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ (x✝² • x✝¹ • x✝).1 = (x✝¹ • x✝² • x✝).1

pp: case snd
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a : M
x : α × β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ (x✝² • x✝¹ • x✝).2 = (x✝¹ • x✝² • x✝).2

Tactic:
<;>

Goal state after:
case fst
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a : M
x : α × β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ (x✝² • x✝¹ • x✝).1 = (x✝¹ • x✝² • x✝).1

case snd
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a : M
x : α × β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ (x✝² • x✝¹ • x✝).2 = (x✝¹ • x✝² • x✝).2
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case fst
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✝¹ : MulAction M α
inst✝ : MulAction M β
x✝² x✝¹ : M
x✝ : α × β
⊢ ((x✝² * x✝¹) • x✝).1 = (x✝² • x✝¹ • x✝).1

pp: case snd
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✝¹ : MulAction M α
inst✝ : MulAction M β
x✝² x✝¹ : M
x✝ : α × β
⊢ ((x✝² * x✝¹) • x✝).2 = (x✝² • x✝¹ • x✝).2

Tactic:
<;>

Goal state after:
case fst
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✝¹ : MulAction M α
inst✝ : MulAction M β
x✝² x✝¹ : M
x✝ : α × β
⊢ ((x✝² * x✝¹) • x✝).1 = (x✝² • x✝¹ • x✝).1

case snd
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✝¹ : MulAction M α
inst✝ : MulAction M β
x✝² x✝¹ : M
x✝ : α × β
⊢ ((x✝² * x✝¹) • x✝).2 = (x✝² • x✝¹ • x✝).2
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case fst
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✝¹ : MulAction M α
inst✝ : MulAction M β
x✝ : α × β
⊢ (1 • x✝).1 = x✝.1

pp: case snd
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✝¹ : MulAction M α
inst✝ : MulAction M β
x✝ : α × β
⊢ (1 • x✝).2 = x✝.2

Tactic:
<;>

Goal state after:
case fst
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✝¹ : MulAction M α
inst✝ : MulAction M β
x✝ : α × β
⊢ (1 • x✝).1 = x✝.1

case snd
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✝¹ : MulAction M α
inst✝ : MulAction M β
x✝ : α × β
⊢ (1 • x✝).2 = x✝.2
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: case ofNat
G : Type u_1
G₀ : Type u_2
inst✝² : Group G
inst✝¹ : GroupWithZero G₀
inst✝ : MulDistribMulAction G G₀
g : G
x : G₀
a✝ : ℕ
⊢ g • x ^ Int.ofNat a✝ = (g • x) ^ Int.ofNat a✝

pp: case negSucc
G : Type u_1
G₀ : Type u_2
inst✝² : Group G
inst✝¹ : GroupWithZero G₀
inst✝ : MulDistribMulAction G G₀
g : G
x : G₀
a✝ : ℕ
⊢ g • x ^ Int.negSucc a✝ = (g • x) ^ Int.negSucc a✝

Tactic:
<;>

Goal state after:
case ofNat
G : Type u_1
G₀ : Type u_2
inst✝² : Group G
inst✝¹ : GroupWithZero G₀
inst✝ : MulDistribMulAction G G₀
g : G
x : G₀
a✝ : ℕ
⊢ g • x ^ Int.ofNat a✝ = (g • x) ^ Int.ofNat a✝

case negSucc
G : Type u_1
G₀ : Type u_2
inst✝² : Group G
inst✝¹ : GroupWithZero G₀
inst✝ : MulDistribMulAction G G₀
g : G
x : G₀
a✝ : ℕ
⊢ g • x ^ Int.negSucc a✝ = (g • x) ^ Int.negSucc a✝
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₃
⊢ f = g ∘ₛₗ ↑e₁₂.symm → f ∘ₛₗ ↑e₁₂ = g

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₃
⊢ f ∘ₛₗ ↑e₁₂ = g → f = g ∘ₛₗ ↑e₁₂.symm

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₃
⊢ f = g ∘ₛₗ ↑e₁₂.symm → f ∘ₛₗ ↑e₁₂ = g

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₃
⊢ f ∘ₛₗ ↑e₁₂ = g → f = g ∘ₛₗ ↑e₁₂.symm
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
⊢ f ∘ₛₗ ↑e₁₂ = g

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
⊢ f = g ∘ₛₗ ↑e₁₂.symm

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
⊢ f ∘ₛₗ ↑e₁₂ = g

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
⊢ f = g ∘ₛₗ ↑e₁₂.symm