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

Goal state before:
pp: ⊢ ∀ (c : Cardinal.{u_1}), 0 < succ c

Tactic:
simp

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsStrongLimit
⊢ IsSuccLimit c

Tactic:
by
  rw [Cardinal.isSuccLimit_iff]
  exact ⟨hc.ne_zero, hc.isStrongPrelimit.isSuccPrelimit⟩

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ ∀ (a : α), True

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ ∀ (b : β), True

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ #(Fin n) = ↑n

Tactic:
simp

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

Goal state before:
pp: c : Cardinal.{u_1}
h : ↑(toNat c) = c
⊢ ↑(toNat c) < ℵ₀

Tactic:
simp

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

Goal state before:
pp: α : Type u
h : Infinite α
⊢ toNat #α = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Fintype α
⊢ toNat #α = Fintype.card α

Tactic:
simp

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

Goal state before:
pp: α : Type u
s : Finset α
⊢ #↥s = ↑s.card

Tactic:
simp

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

Goal state before:
pp: c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
⊢ toNat c = toNat d

Tactic:
rcases iff_iff_and_or_not_and_not.mp h' with ⟨hc, hd⟩ | ⟨hc, hd⟩

Goal state after:
case inl
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ℵ₀ ≤ c
hd : ℵ₀ ≤ d
⊢ toNat c = toNat d

case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ toNat c = toNat d
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
n : ℕ∞
x : ℕ
⊢ ↑n ≤ ↑x ↔ n ≤ (↑x).toENatAux

Tactic:
simp

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

Goal state before:
pp: case inl
n x : ℕ
⊢ (↑x).toENatAux ≤ ↑n ↔ ↑x ≤ ↑n

Tactic:
simp

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

Goal state before:
pp: case inr.inl
y : Cardinal.{u}
hy : ℵ₀ ≤ y
hle : 0 ≤ y
⊢ (0 * y).toENatAux = toENatAux 0 * y.toENatAux

Tactic:
simp

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

Goal state before:
pp: c : Cardinal.{u}
⊢ toENat c < 1 ↔ c < 1

Tactic:
simp

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

Goal state before:
pp: c : Cardinal.{u}
⊢ toENat c ≠ ⊤ ↔ c < ℵ₀

Tactic:
simp

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

Goal state before:
pp: case inl
c : ℕ∞
⊢ toENat (lift.{v, u} ↑c) = toENat ↑c

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: m n : ℕ∞
⊢ toENat ↑(m * n) = toENat (↑m * ↑n)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ (RingHom.id R₁) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ (RingHom.id R₂) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
inst✝ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ σ₁₂.comp (RingHom.id R₁) = σ₁₂

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
inst✝ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ (RingHom.id R₂).comp σ₁₂ = σ₁₂

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ lift.{u, w} (sSup (range f)) = sSup (range fun i ↦ lift.{u, w} (f i))

Tactic:
lift_sSup hf,

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ sSup (lift.{u, w} '' range f) = sSup (range fun i ↦ lift.{u, w} (f i))
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
inst✝ : Fintype α
⊢ #(Finset α) = 2 ^ Fintype.card α

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ ↑n.succ = succ ↑n

Tactic:
simp

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

Goal state before:
pp: S : Finset ℕ
h' : #↑↑S < #ℕ
h : lift.{u_1, 0} #↑↑S < ℵ₀
⊢ ∃ n, lift.{u_1, 0} #↑↑S = ↑n

Tactic:
simp

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 1 • a < ℵ₀ ↔ 1 = 0 ∨ a < ℵ₀

Tactic:
simp

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

Goal state before:
pp: a : Cardinal.{u_1}
n : ℕ
⊢ (n + 1 = 0 ∨ a < ℵ₀) ∧ a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ↑n * ℵ₀ = ℵ₀

Tactic:
nat_mul_aleph0 hn

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ ℵ₀ = ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ #(Fin n → α) = #α ^ n

Tactic:
simp

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

Goal state before:
pp: α : Type u
⊢ #((n : ℕ) × List.Vector α n) = sum fun n ↦ #α ^ n

Tactic:
simp

Goal state after:
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:
· intro h
    lift s to Finset α using lt_aleph0_iff_set_finite.1 (h.symm ▸ natCast_lt_aleph0)
    simpa using h

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: α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t} = lift.{v, u} #↑((fun x ↦ f ↑x) ⁻¹' t)

Tactic:
rw [mk_sep]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ lift.{v, u} #↑{x | f ↑x ∈ t} = lift.{v, u} #↑((fun x ↦ f ↑x) ⁻¹' t)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑{x | x ∈ s ∧ f x ∈ t} = #↑((fun x ↦ f ↑x) ⁻¹' t)

Tactic:
rw [mk_sep]

Goal state after:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑{x | f ↑x ∈ t} = #↑((fun x ↦ f ↑x) ⁻¹' t)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ {x, y} = univ

Tactic:
simpa using ht

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

Tactic:
rintro ⟨t, ht, x, y, hne, rfl⟩
    exact ⟨x, y, hne, by simpa using ht⟩

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

Tactic:
simp

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

Goal state before:
pp: a : Cardinal.{u_1}
h : a ≠ 0
⊢ ?m.23 ^ 0 ≤ 0 ^< a

pp: a : Cardinal.{u_1}
h : a ≠ 0
⊢ Cardinal.{u_1}

Tactic:
exact le_powerlt 0 (pos_iff_ne_zero.2 h)

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

Goal state before:
pp: case convert_3
a : Cardinal.{u_1}
⊢ IsEmpty ↑(Iio 0)

Tactic:
exact Subtype.isEmpty_of_false fun x => mem_Iio.not.mpr not_lt_zero

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : SemigroupWithZero M₀
inst✝ : SemigroupWithZero N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : SemigroupWithZero M₀
inst✝ : SemigroupWithZero N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : MulZeroOneClass N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : MulZeroOneClass N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : CommMonoidWithZero M₀
inst✝ : CommMonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : CommMonoidWithZero M₀
inst✝ : CommMonoidWithZero N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
simp

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

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

Goal state after:
Module: Mathlib.Algebra.Module.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r✝ s : R
x r : M
⊢ ((↑(DistribMulAction.toAddMonoidEnd R M)).toFun 0) r = 0 r

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ∀ (n : ℕ), op ↑(n + 1) = op ↑n + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Ring.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
n : ℕ
⊢ op ↑(Int.negSucc n) = op (-unop (op ↑(n + 1)))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: 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₂
f : M₃ →ₛₗ[σ₃₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
x✝ : M₃
⊢ (↑e₁₂ ∘ₛₗ ↑e₁₂.symm ∘ₛₗ f) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: 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₂
f : M₃ →ₛₗ[σ₃₁] M₁
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
x✝ : M₃
⊢ (↑e₁₂.symm ∘ₛₗ ↑e₁₂ ∘ₛₗ f) x✝ = f x✝

Tactic:
simp

Goal state after:
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:
simp [← H]

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

Tactic:
simp [← H]

Goal state after:
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 : ↑e₁₂ ∘ₛₗ f = g
x✝ : M₃
⊢ f x✝ = (↑e₁₂.symm ∘ₛₗ g) x✝

Tactic:
simp [← H]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
⊢ σ 0 • f 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
c : S
x : M
⊢ c • f x = f (σ' c • x)

Tactic:
simp

Goal state after:
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 : ↑e₁₂.symm ∘ₛₗ g = f
x✝ : M₃
⊢ g x✝ = (↑e₁₂ ∘ₛₗ f) x✝

Tactic:
simp [← H]

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: 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 σ₃₂ σ₂₁ σ₃₁
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
x✝ : M₃
⊢ (↑e ∘ₛₗ ↑e.symm ∘ₛₗ f) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: 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 σ₃₂ σ₂₁ σ₃₁
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₁] M₁
x✝ : M₃
⊢ (↑e.symm ∘ₛₗ ↑e ∘ₛₗ f) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: 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 σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ →ₛₗ[σ₂₃] M₃
x✝ : M₂
⊢ ((f ∘ₛₗ ↑e) ∘ₛₗ ↑e.symm) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: 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 σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ →ₛₗ[σ₁₃] M₃
x✝ : M₁
⊢ ((f ∘ₛₗ ↑e.symm) ∘ₛₗ ↑e) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: 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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₁ ≃ₛₗ[σ₁₃] M₃
x✝ : M₁
⊢ (e.trans (e.symm.trans f)) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: 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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₂ ≃ₛₗ[σ₂₃] M₃
x✝ : M₂
⊢ (e.symm.trans (e.trans f)) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: case zero
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S✝ : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_14
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
⊢ fₗ (0 • x) = 0 • fₗ x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: 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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₁] M₁
x✝ : M₃
⊢ ((f.trans e).trans e.symm) x✝ = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: 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₁
inst✝⁵ : RingHomInvPair σ₁₃ σ₃₁
inst✝⁴ : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₂] M₂
x✝ : M₃
⊢ ((f.trans e.symm).trans e) x✝ = f x✝

Tactic:
simp

Goal state after: