mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S : Type u_6
M : 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✝¹⁰ : Semiring R₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : Semiring R₄
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid M₄
inst✝¹ : AddCommMonoid N₁
inst✝ : AddCommMonoid N₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e✝ e' e : M ≃ₛₗ[σ] M₂
r : S
x : M₂
⊢ ((↑e).inverse e.invFun ⋯ ⋯) (r • x) = σ' r • ((↑e).inverse e.invFun ⋯ ⋯) x

Tactic:
map_smulₛₗ

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S : Type u_6
M : 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✝¹⁰ : Semiring R₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : Semiring R₄
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid M₄
inst✝¹ : AddCommMonoid N₁
inst✝ : AddCommMonoid N₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e✝ e' e : M ≃ₛₗ[σ] M₂
r : S
x : M₂
⊢ σ' r • ((↑e).inverse e.invFun ⋯ ⋯) x = σ' r • ((↑e).inverse e.invFun ⋯ ⋯) x
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
⊢ f (0 • 0) = 0

Tactic:
map_smulₛₗ

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
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
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
c : R
x : M
⊢ f (c • x) = σ c • f x

Tactic:
map_smulₛₗ

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
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
c : R
x : M
⊢ σ c • f x = σ c • f x
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: case mk.mk
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
toAddHom✝¹ : M →ₙ+ M₃
map_smul'✝¹ : ∀ (m : R) (x : M), toAddHom✝¹.toFun (m • x) = σ m • toAddHom✝¹.toFun x
toAddHom✝ : M →ₙ+ M₃
map_smul'✝ : ∀ (m : R) (x : M), toAddHom✝.toFun (m • x) = σ m • toAddHom✝.toFun x
h :
  (fun f ↦ f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =
    (fun f ↦ f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
⊢ { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } = { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }

Tactic:
congr

Goal state after:
case mk.mk
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
toAddHom✝¹ : M →ₙ+ M₃
map_smul'✝¹ : ∀ (m : R) (x : M), toAddHom✝¹.toFun (m • x) = σ m • toAddHom✝¹.toFun x
toAddHom✝ : M →ₙ+ M₃
map_smul'✝ : ∀ (m : R) (x : M), toAddHom✝.toFun (m • x) = σ m • toAddHom✝.toFun x
h :
  (fun f ↦ f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =
    (fun f ↦ f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
⊢ toAddHom✝¹ = toAddHom✝
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: case mk.mk
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
toFun✝¹ : X → Y
map_smul'✝¹ : ∀ (m : M) (x : X), toFun✝¹ (m • x) = φ m • toFun✝¹ x
toFun✝ : X → Y
map_smul'✝ : ∀ (m : M) (x : X), toFun✝ (m • x) = φ m • toFun✝ x
h : { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }.toFun = { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } = { toFun := toFun✝, map_smul' := map_smul'✝ }

Tactic:
congr

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

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ g (f (m • x)) = g (φ m • f x)

Tactic:
map_smulₛₗ

Goal state after:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ g (φ m • f x) = g (φ m • f x)
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ g (φ m • f x) = ψ (φ m) • g (f x)

Tactic:
map_smulₛₗ

Goal state after:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ ψ (φ m) • g (f x) = ψ (φ m) • g (f x)
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (φ (φ' m) • f (g x)) = g (f (φ' m • g x))

Tactic:
map_smulₛₗ

Goal state after:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (φ (φ' m) • f (g x)) = g (φ (φ' m) • f (g x))
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: case mk.mk
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'
toFun✝¹ : A → B
map_smul'✝¹ : ∀ (m : M) (x : A), toFun✝¹ (m • x) = φ m • toFun✝¹ x
map_one'✝¹ : { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : A),
    { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }.toFun x * { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }.toFun y
toFun✝ : A → B
map_smul'✝ : ∀ (m : M) (x : A), toFun✝ (m • x) = φ m • toFun✝ x
map_one'✝ : { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun x * { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun y
h :
  (fun m ↦ m.toFun) { toFun := toFun✝¹, map_smul' := map_smul'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun m ↦ m.toFun) { toFun := toFun✝, map_smul' := map_smul'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toFun := toFun✝¹, map_smul' := map_smul'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toFun := toFun✝, map_smul' := map_smul'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }

Tactic:
congr

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

Goal state before:
pp: case e_4.e_2
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
i : DistribMulAction N α
⊢ SMulCommClass M N α = SMulCommClass M N α

Tactic:
congr

Goal state after:
case e_4.e_2.e_4.e_4.e_4.e_5
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
i : DistribMulAction N α
⊢ compHom α (MonoidHom.inl M N) = fst✝
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
n : ℕ
hn : n ≠ 0
h : Injective ⇑(f' ^ n.pred.succ)
⊢ Injective ⇑f'

Tactic:
iterate_succ,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Injective ⇑((f' ^ n.pred) ∘ₗ f')
⊢ Injective ⇑f'
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
n : ℕ
hn : n ≠ 0
h : Injective ⇑(f' ^ n)
⊢ Injective ⇑f'

Tactic:
by
  rw [← Nat.succ_pred_eq_of_pos (show 0 < n by lia), iterate_succ, coe_comp] at h
  exact h.of_comp

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

Goal state before:
pp: case mk.mk
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
toAddSubmonoid✝¹ : AddSubmonoid M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    (fun s ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
⊢ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }

Tactic:
congr

Goal state after:
case mk.mk
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
toAddSubmonoid✝¹ : AddSubmonoid M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    (fun s ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
⊢ toAddSubmonoid✝¹ = toAddSubmonoid✝
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: case mk.mk
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
carrier✝¹ : Set M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ carrier✝¹ → c • x ∈ carrier✝¹
carrier✝ : Set M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ carrier✝ → c • x ∈ carrier✝
h :
  { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ }.carrier = { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ } = { carrier := carrier✝, smul_mem' := smul_mem'✝ }

Tactic:
congr

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₃
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
r : R
c : M
⊢ f (r • c) = σ₁₂ r • f c

Tactic:
map_smulₛₗ

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

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
toFun✝¹ : α → β
map_sSup'✝¹ : ∀ (s : Set α), toFun✝¹ (sSup s) = sSup (toFun✝¹ '' s)
toFun✝ : α → β
map_sSup'✝ : ∀ (s : Set α), toFun✝ (sSup s) = sSup (toFun✝ '' s)
h : { toFun := toFun✝¹, map_sSup' := map_sSup'✝¹ }.toFun = { toFun := toFun✝, map_sSup' := map_sSup'✝ }.toFun
⊢ { toFun := toFun✝¹, map_sSup' := map_sSup'✝¹ } = { toFun := toFun✝, map_sSup' := map_sSup'✝ }

Tactic:
congr

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
toFun✝¹ : α → β
map_inf'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊓ b) = toFun✝¹ a ⊓ toFun✝¹ b
map_top'✝¹ : { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }.toFun ⊤ = ⊤
map_sSup'✝¹ :
  ∀ (s : Set α),
    { toFun := toFun✝¹, map_inf' := map_inf'✝¹, map_top' := map_top'✝¹ }.toFun (sSup s) =
      sSup ({ toFun := toFun✝¹, map_inf' := map_inf'✝¹, map_top' := map_top'✝¹ }.toFun '' s)
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
map_top'✝ : { toFun := toFun✝, map_inf' := map_inf'✝ }.toFun ⊤ = ⊤
map_sSup'✝ :
  ∀ (s : Set α),
    { toFun := toFun✝, map_inf' := map_inf'✝, map_top' := map_top'✝ }.toFun (sSup s) =
      sSup ({ toFun := toFun✝, map_inf' := map_inf'✝, map_top' := map_top'✝ }.toFun '' s)
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_inf' := map_inf'✝¹, map_top' := map_top'✝¹, map_sSup' := map_sSup'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_sSup' := map_sSup'✝ }
⊢ { toFun := toFun✝¹, map_inf' := map_inf'✝¹, map_top' := map_top'✝¹, map_sSup' := map_sSup'✝¹ } =
    { toFun := toFun✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_sSup' := map_sSup'✝ }

Tactic:
congr

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
toFun✝¹ : α → β
map_sInf'✝¹ : ∀ (s : Set α), toFun✝¹ (sInf s) = sInf (toFun✝¹ '' s)
map_sSup'✝¹ :
  ∀ (s : Set α),
    { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ }.toFun (sSup s) =
      sSup ({ toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ }.toFun '' s)
toFun✝ : α → β
map_sInf'✝ : ∀ (s : Set α), toFun✝ (sInf s) = sInf (toFun✝ '' s)
map_sSup'✝ :
  ∀ (s : Set α),
    { toFun := toFun✝, map_sInf' := map_sInf'✝ }.toFun (sSup s) =
      sSup ({ toFun := toFun✝, map_sInf' := map_sInf'✝ }.toFun '' s)
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹, map_sSup' := map_sSup'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_sInf' := map_sInf'✝, map_sSup' := map_sSup'✝ }
⊢ { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹, map_sSup' := map_sSup'✝¹ } =
    { toFun := toFun✝, map_sInf' := map_sInf'✝, map_sSup' := map_sSup'✝ }

Tactic:
congr

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
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
S : Submodule R₂ M₂
y : M
hx : f y ∈ S
⊢ f y ∈ map f (comap f S)

Tactic:
simp only [mem_map, mem_comap]

Goal state after:
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
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
S : Submodule R₂ M₂
y : M
hx : f y ∈ S
⊢ ∃ y_1, f y_1 ∈ S ∧ f y_1 = f y
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₂
p : Submodule R M
q : Submodule R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
h : comap f q < p
⊢ q < map f p

Tactic:
rw [lt_iff_le_not_ge] at h ⊢; rw [map_le_iff_le_comap]
  exact h.imp_left (le_map_of_comap_le_of_surjective hf)

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ 0 ∈ s

Tactic:
by subst ha; exact sa.zero_mem

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: case mk.mk
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
toSubmonoid✝¹ : Submonoid R
add_mem'✝¹ : ∀ {a b : R}, a ∈ toSubmonoid✝¹.carrier → b ∈ toSubmonoid✝¹.carrier → a + b ∈ toSubmonoid✝¹.carrier
zero_mem'✝¹ : 0 ∈ toSubmonoid✝¹.carrier
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
⊢ { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
toSubmonoid✝¹ : Submonoid R
add_mem'✝¹ : ∀ {a b : R}, a ∈ toSubmonoid✝¹.carrier → b ∈ toSubmonoid✝¹.carrier → a + b ∈ toSubmonoid✝¹.carrier
zero_mem'✝¹ : 0 ∈ toSubmonoid✝¹.carrier
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
⊢ toSubmonoid✝¹ = toSubmonoid✝
Module: Mathlib.RingTheory.NonUnitalSubring.Defs

Goal state before:
pp: case mk.mk
R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ toNonUnitalSubsemiring✝¹ = toNonUnitalSubsemiring✝
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ ↑↑n * (x✝¹ * x✝) = ↑↑n * x✝¹ * x✝

Tactic:
rw [Int.cast_natCast, (natCast_mem_center _ n).left_assoc _ _]

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

Goal state before:
pp: case add
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
hx : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ + y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
| add _ _ _ _ hx hy =>

Goal state after: