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

Goal state before:
pp: case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = lift.{u, v} (∏ i, f i)

Tactic:
← e.prod_comp f,

Goal state after:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = lift.{u, v} (∏ i, f (e i))
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
obtain ⟨d, rfl⟩ := Cardinal.mem_range_lift_of_le (not_le.1 h).le

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

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m + ↑n < ℵ₀

Tactic:
rw [← Nat.cast_add]

Goal state after:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m + n) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
⊢ ℵ₀ + ↑n = ℵ₀

Tactic:
aleph0_add_nat

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

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

Tactic:
← union_singleton,

Goal state after:
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(s ∪ {a}) = #↑s + 1
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 σ₃₁ σ₁₂ σ₃₂
⊢ ↑e₁₂ ∘ₛₗ ↑e₁₂.symm ∘ₛₗ f = f

Tactic:
by ext; 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 σ₃₁ σ₁₂ σ₃₂
⊢ ↑e₁₂.symm ∘ₛₗ ↑e₁₂ ∘ₛₗ f = f

Tactic:
by ext; 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 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
σ : R →+* R
inst✝ : RingHomId σ
r : R
x : M
⊢ r • x = σ r • x

Tactic:
have := (RingHomId.eq_id : σ = _)

Goal state after:
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✝⁷ : 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
σ : R →+* R
inst✝ : RingHomId σ
r : R
x : M
this : σ = RingHom.id R
⊢ r • x = σ r • x
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₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
⊢ f ∘ₛₗ ↑e₁₂ = g ∘ₛₗ ↑e₁₂ ↔ f = g

Tactic:
by
  refine ⟨fun h => ?_, fun a ↦ congrFun (congrArg LinearMap.comp a) e₁₂.toLinearMap⟩
  rw [(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm, eq_comp_toLinearMap_symm]

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

Tactic:
by ext; 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₁
⊢ ↑e.symm ∘ₛₗ ↑e ∘ₛₗ f = f

Tactic:
by ext; 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₃
⊢ (f ∘ₛₗ ↑e) ∘ₛₗ ↑e.symm = f

Tactic:
by ext; 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₃
⊢ (f ∘ₛₗ ↑e.symm) ∘ₛₗ ↑e = f

Tactic:
by ext; 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₃
⊢ e.trans (e.symm.trans f) = f

Tactic:
by ext; 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₃
⊢ e.symm.trans (e.trans f) = f

Tactic:
by ext; 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₁
⊢ (f.trans e).trans e.symm = f

Tactic:
by ext; 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₂
⊢ (f.trans e.symm).trans e = f

Tactic:
by ext; simp

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

Goal state before:
pp: S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst✝¹⁵ : Semiring R
inst✝¹⁴ : Semiring S
inst✝¹³ : AddCommMonoid V
inst✝¹² : Module R V
inst✝¹¹ : Module S V
inst✝¹⁰ : AddCommMonoid W
inst✝⁹ : Module R W
inst✝⁸ : Module S W
inst✝⁷ : AddCommMonoid G
inst✝⁶ : Module R G
inst✝⁵ : Module S G
inst✝⁴ : SMulCommClass R S W
inst✝³ : SMul S R
inst✝² : IsScalarTower S R V
inst✝¹ : IsScalarTower S R W
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
⊢ e ≪≫ₗ (α • f) = α • e ≪≫ₗ f

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
⊢ f.smulRight 0 = 0

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : M
⊢ smulRight 0 x = 0

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ Commute LinearMap.id f

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ Commute f LinearMap.id

Tactic:
by ext; simp

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

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✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a : S
⊢ a • 0 = 0

Tactic:
by ext; simp

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

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✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a : ↥p
⊢ 0 • a = 0

Tactic:
by ext; simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : ↥t
⊢ 1 • x✝ = x✝

Tactic:
by ext; simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : S
⊢ x✝ • 0 = 0

Tactic:
by ext; simp

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : ↥t
⊢ 0 • x✝ = 0

Tactic:
by ext; 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
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst✝²³ : Semiring R₁
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₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst✝¹¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁹ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝⁸ : RingHomInvPair σ₂'₁' σ₁'₂'
inst✝⁷ : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst✝⁶ : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst✝⁵ : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst✝³ : Semiring S
inst✝² : Module S M₁
inst✝¹ : SMulCommClass R₁ S M₁
inst✝ : RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
x✝¹ : S
x✝ : M₁ →ₛₗ[σ₁₁'] M₁'
⊢ ((refl R₁ M₁).arrowCongrAddEquiv e₂).toFun (DomMulAct.mk x✝¹ • x✝) =
    (RingHom.id Sᵈᵐᵃ) (DomMulAct.mk x✝¹) • ((refl R₁ M₁).arrowCongrAddEquiv e₂).toFun x✝

Tactic:
by ext; simp

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

Goal state before:
pp: R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst✝⁷ : CommSemiring R₁'
inst✝⁶ : CommSemiring R₂'
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : Module R₁' M₁'
inst✝² : Module R₂' M₂'
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
inst✝¹ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝ : RingHomInvPair σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : Module.End R₂' M₂'
⊢ e.conj (e.symm.conj f) = f

Tactic:
by ext; simp

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

Goal state before:
pp: R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst✝⁷ : CommSemiring R₁'
inst✝⁶ : CommSemiring R₂'
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : Module R₁' M₁'
inst✝² : Module R₂' M₂'
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
inst✝¹ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝ : RingHomInvPair σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : Module.End R₁' M₁'
⊢ e.symm.conj (e.conj f) = f

Tactic:
by ext; simp

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

Goal state before:
pp: R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst✝⁷ : CommSemiring R₁'
inst✝⁶ : CommSemiring R₂'
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : Module R₁' M₁'
inst✝² : Module R₂' M₂'
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
inst✝¹ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝ : RingHomInvPair σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
⊢ e.conj LinearMap.id = LinearMap.id

Tactic:
by ext; 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
R : Type u_9
A : Type u_10
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
⊢ (let __spread.0 := mulLeft 1;
    let __spread.1 := LinearMap.mulLeft R ↑1;
    { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
      right_inv := ⋯ }) =
    1

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
⊢ (-f).ker = f.ker

Tactic:
by ext; simp

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

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
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
⊢ ∀ (c : R₂) {x : M₂}, x ∈ ⇑f '' ↑p → c • x ∈ ⇑f '' ↑p

Tactic:
rintro c x ⟨y, hy, rfl⟩
      obtain ⟨a, rfl⟩ := σ₁₂.surjective c
      exact ⟨_, p.smul_mem a hy, map_smulₛₗ f _ _⟩

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
⊢ map f p ⋖ map f q

Tactic:
refine ⟨lt_of_le_of_ne (map_mono h.1.le) ((map_injective_of_injective hf).ne h.1.ne), ?_⟩

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
⊢ ∀ ⦃c : Submodule R₂ M₂⦄, map f p < c → ¬c < map f q
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ x✝ ∈ map (↑e) K ↔ x✝ ∈ comap (↑e.symm) K

Tactic:
rw [mem_map_equiv, mem_comap, LinearEquiv.coe_coe]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Mul R
inst✝² : HasDistribNeg R
inst✝¹ : SetLike S R
inst✝ : MulMemClass S R
s : S
x y : R
hx : -x ∈ s
hy : y ∈ s
⊢ -(x * y) ∈ s

Tactic:
simpa using mul_mem hx hy

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Mul R
inst✝² : HasDistribNeg R
inst✝¹ : SetLike S R
inst✝ : MulMemClass S R
s : S
x y : R
hx : x ∈ s
hy : -y ∈ s
⊢ -(x * y) ∈ s

Tactic:
simpa using mul_mem hx hy

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

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ False

Tactic:
by
  have :=
    NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)
  rw [Prod.mk_eq_zero, Prod.mk_eq_zero] at this
  rcases this with (⟨_, h⟩ | ⟨h, _⟩)
  · exact zero_ne_one h.symm
  · exact zero_ne_one h.symm

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ f.range = NonUnitalSubring.map f ⊤

Tactic:
by ext; simp

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

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
⊢ x * (x - (algebraMap R A) r) * (x - (algebraMap R A) r) ^ n =
    (x - (algebraMap R A) r) * (x - (algebraMap R A) r) ^ n * x

Tactic:
mul_sub_algebraMap_commutes,

Goal state after:
case succ
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
⊢ (x - (algebraMap R A) r) * x * (x - (algebraMap R A) r) ^ n =
    (x - (algebraMap R A) r) * (x - (algebraMap R A) r) ^ n * x
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P Q : Algebra ℕ R
⊢ P = Q

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : A →ₐ[R] A
n : ℕ
⊢ ⇑(φ ^ Nat.zero) = (⇑φ)^[Nat.zero]

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Group

Goal state before:
pp: G : Type u_1
inst✝² : Group G
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction G R
⊢ (let __src := DistribMulAction.toAddEquiv R 1;
    let __src_1 := toRingHom G R 1;
    { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ }) =
    1

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ f x ∈ closure (⇑f '' s)

Tactic:
by
  rw [← f.map_closure, Subring.mem_map]
  exact ⟨x, hx, rfl⟩

Goal state after: