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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x < y
⊢ (sumLexIicIoi x).symm y = toLex (Sum.inr ⟨y, h⟩)

Tactic:
symm_apply_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x < y
⊢ y = (sumLexIicIoi x) (toLex (Sum.inr ⟨y, h⟩))
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : Preorder β
inst✝ : Unique β
x : α
⊢ (fun x ↦ (ofLex x).1) ((fun x ↦ toLex (x, default)) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Unique α
inst✝ : LE β
x : β
⊢ (fun x ↦ (ofLex x).2) ((fun x ↦ toLex (default, x)) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
⊢ sSup (Iio x) = x

Tactic:
obtain rfl | hx := eq_bot_or_bot_lt x

Goal state after:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
h : IsSuccPrelimit ⊥
⊢ sSup (Iio ⊥) = ⊥

case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: α✝ β : Type u
α : Type v
⊢ #(Quotient.out #α) = #α

Tactic:
by simp

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

Goal state before:
pp: ι : Type u
a : Cardinal.{u}
⊢ (sum fun x ↦ a) = #ι * a

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≃r s
⊢ ∀ (a : α) (b : β), s b (f.toRelEmbedding a) → b ∈ Set.range ⇑f.toRelEmbedding

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ∀ (a b : α), a ≤ b → {a, b} ∈ univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := pd, get := p }.get h₂
t : od = pd
⊢ { Dom := od, get := o } = { Dom := pd, get := p }

Tactic:
cases t

Goal state after:
case refl
α : Type u_1
od : Prop
o p : od → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := od, get := p }.get h₂
⊢ { Dom := od, get := o } = { Dom := od, get := p }
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ o.toOption = Option.some a ↔ a ∈ o

Tactic:
by
  rw [← Option.mem_def, mem_toOption]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : β
⊢ ¬a ∈ map f none

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Part β
a : β
⊢ ¬a ∈ none.bind f

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → Part β
⊢ ∀ (a_1 : β), a_1 ∈ (some a).bind f ↔ a_1 ∈ f a

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
rcases h with ⟨z, hz, hzy⟩

Goal state after:
case neg
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
z : α
hz : z ∈ c
hzy : ¬z ≤ y
⊢ cSup c ≤ y ∨ f y ≤ cSup c
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
c : Chain α
hf : ωScottContinuous f
⊢ Set.range ⇑c ∈ Set.range fun c ↦ Set.range ⇑c

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : z ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
a✝ : y ≠ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y

Tactic:
obtain ⟨_, (hz | hz)⟩ := hz

Goal state after:
case inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
a✝ : y ≠ z
left✝ : z ∈ bot x f
hz : z ≤ y
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y

case inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
a✝ : y ≠ z
left✝ : z ∈ bot x f
hz : f y ≤ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (SupSet.sSup s)

Tactic:
rw [sSup_eq_iSup]; apply ωScottContinuous.iSup fun f ↦ ωScottContinuous.iSup <| hs f

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (SupSet.sSup s)

Tactic:
by
  rw [sSup_eq_iSup]; apply ωScottContinuous.iSup fun f ↦ ωScottContinuous.iSup <| hs f

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : IsEmpty β
this : IsEmpty α
⊢ ∀ (a : α), R a (((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm) a)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
a : β
⊢ ⊤ (ωSup c) ≤ a ↔ ωSup (c.map { toFun := ⊤, monotone' := ⋯ }) ≤ a

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ ∀ f ∈ ∅, ωScottContinuous f

Tactic:
by simp

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

Goal state before:
pp: α : Type u
h : Fintype α
⊢ Fintype.card α = Fintype.card (ULift.{u, 0} (Fin (Fintype.card α)))

Tactic:
by simp

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

Goal state before:
pp: ⊢ #Bool = 2

Tactic:
by simp

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

Goal state before:
pp: ⊢ #Prop = 2

Tactic:
by simp

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

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

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ f (ωSup (iterateChain (↑f) x h)) = ωSup (iterateChain (↑f) x h)

Tactic:
f.continuous

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) = ωSup (iterateChain (↑f) x h)
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

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

Tactic:
by 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:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: case inr
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ↑(toNat a) ≤ a

Tactic:
· simp [Cardinal.toNat_apply_of_aleph0_le h]

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by 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₀), 0 * a = 0

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

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
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
⊢ ∀ (x y : M), 0 (x + y) = 0 x + 0 y

Tactic:
by simp

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
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
⊢ ∀ (m : R₁) (x : M), 0 (m • x) = σ₁₂ m • 0 x

Tactic:
by simp

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
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] N₂
⊢ ∀ (m : R₁) (x : M), (-⇑f) (m • x) = σ₁₂ m • (-⇑f) x

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝² : SMul M X
inst✝¹ : Zero Y
inst✝ : SMulZeroClass N Y
⊢ ∀ (m : M) (x : X), 0 (m • x) = σ m • 0 x

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝² : SMul M X
inst✝¹ : AddGroup Y
inst✝ : DistribSMul N Y
f : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X), (-⇑f) (m • x) = σ m • (-⇑f) x

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝³ : SMul M X
inst✝² : Monoid N
inst✝¹ : Monoid Y
inst✝ : MulDistribMulAction N Y
f g : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X), (⇑f * ⇑g) (m • x) = σ m • (⇑f * ⇑g) x

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝³ : SMul M X
inst✝² : Monoid N
inst✝¹ : Monoid Y
inst✝ : MulDistribMulAction N Y
⊢ ∀ (m : M) (x : X), 1 (m • x) = σ m • 1 x

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝¹⁹ : Monoid M
N : Type u_2
inst✝¹⁸ : Monoid N
P : Type u_3
inst✝¹⁷ : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A✝ : Type u_4
inst✝¹⁶ : Monoid A✝
inst✝¹⁵ : MulDistribMulAction M A✝
B✝ : Type u_5
inst✝¹⁴ : Monoid B✝
inst✝¹³ : MulDistribMulAction N B✝
B₁ : Type u_6
inst✝¹² : Monoid B₁
inst✝¹¹ : MulDistribMulAction M B₁
C : Type u_7
inst✝¹⁰ : Monoid C
inst✝⁹ : MulDistribMulAction P C
A' : Type u_8
inst✝⁸ : Group A'
inst✝⁷ : MulDistribMulAction M A'
B' : Type u_9
inst✝⁶ : Group B'
inst✝⁵ : MulDistribMulAction N B'
F : Type u_10
inst✝⁴ : FunLike F A✝ B✝
A : Type u_11
inst✝³ : AddMonoid A
inst✝² : DistribMulAction M A
B : Type u_12
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction N B
m : M
x✝ : A
⊢ (↑0).toFun (m • x✝) = φ m • (↑0).toFun x✝

Tactic:
by simp

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

Goal state before:
pp: I : Type u
f : I → Type u_1
inst✝ : (i : I) → Semiring (f i)
i : I
x : f i
⊢ ((Pi.evalRingHom f i) fun x_1 ↦ if h : x_1 = i then ⋯ ▸ x else 0) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
⊢ r • m ≠ 0 ↔ r ≠ 0 ∧ m ≠ 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
h : IsUnit f
x : M
⊢ (h.unit.inv * f) x = x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : (f ^ k) m = 0
⊢ (f ^ l) m = 0

Tactic:
by
  rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]

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

Goal state before:
pp: case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))

Tactic:
| succ k ih =>

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Basic

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝ : Module.IsTorsionFree R M
⊢ ∀ (r : R) (m : ↥p), ↑(r • m) = r • ↑m

Tactic:
by simp

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

Goal state before:
pp: ⊢ ∀ {a : PUnit}, a ≠ 0 → IsLeftRegular a

Tactic:
by simp

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

Goal state before:
pp: ⊢ ∀ {a : PUnit}, a ≠ 0 → IsRightRegular a

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : SMul R S
⊢ ∀ (m : PUnit) (n : R) (a : S), m • n • a = n • m • a

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : SMul R S
⊢ ∀ (x : PUnit) (y : R) (z : S), (x • y) • z = x • y • z

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
⊢ ∀ (c : R) {x : M}, x ∈ {0} → c • x ∈ {0}

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
⊢ ∀ (c : R) {x : M}, x ∈ ∅ → c • x ∈ ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
⊢ ∀ (c : R) {x : M}, x ∈ Set.univ → c • x ∈ Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p : SubMulAction R M
r : R
x : M
⊢ ∀ (m : R) (x : ↥p), ↑(m • x) = id m • ↑x

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ s • x ∈ p

Tactic:
rw [← one_smul R x, ← smul_assoc]

Goal state after:
S : Type u'
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ (s • 1) • x ∈ p
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
s : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ (↑s)ᶜ → c • x ∈ (↑s)ᶜ

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
y : { v // v ≠ 0 }
a : Rˣ
⊢ (fun m ↦ m • ↑y) a = ↑((fun m ↦ m • y) a)

Tactic:
by simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
⊢ ∀ (x y : ↥p), ↑(x + y) = ↑x + ↑y

Tactic:
by simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Semiring R
inst✝ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
⊢ ∀ (m : R) (x : ↥p), ↑(m • x) = (RingHom.id R) m • ↑x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
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 →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
h : ∀ (c : M), f c ∈ p
x✝¹ x✝ : M
⊢ ⟨f (x✝¹ + x✝), ⋯⟩ = ⟨f x✝¹, ⋯⟩ + ⟨f x✝, ⋯⟩

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
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 →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
h : ∀ (c : M), f c ∈ p
x✝¹ : R
x✝ : M
⊢ ⟨f (x✝¹ • x✝), ⋯⟩ = σ₁₂ x✝¹ • ⟨f x✝, ⋯⟩

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
x : M
⊢ (fun f ↦ f 1) (smulRight 1 x) = x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ (neg R) x = -x

Tactic:
by simp

Goal state after: