mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (∀ ⦃x : M⦄, x ∈ N → x ∈ f.ker) ↔ ∀ (a : M) (b : a ∈ N), (f ∘ₛₗ N.subtype) ⟨a, b⟩ = 0 ⟨a, b⟩

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
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₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (∀ ⦃x : M⦄, x ∈ N → x ∈ f.ker) ↔ ∀ (a : M) (b : a ∈ N), (f ∘ₛₗ N.subtype) ⟨a, b⟩ = 0 ⟨a, b⟩
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
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 τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ f.ker ≤ comap f g.ker

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
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 τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ f.ker ≤ comap f g.ker
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₂'
x✝ : M₂'
⊢ (e.conj (e.symm.conj f)) x✝ = f x✝

Tactic:
;

Goal state after:
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₂'
x✝ : M₂'
⊢ (e.conj (e.symm.conj f)) x✝ = f x✝
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 δ
g : CompleteLatticeHom α β
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) g
⊢ { toFun := toFun✝, map_sInf' := map_sInf'✝, map_sSup' := map_sSup'✝ } = g

Tactic:
;

Goal state after:
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 δ
g : CompleteLatticeHom α β
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) g
⊢ { toFun := toFun✝, map_sInf' := map_sInf'✝, map_sSup' := map_sSup'✝ } = g
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:
;

Goal state after:
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'✝ }
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₁'
x✝ : M₁'
⊢ (e.symm.conj (e.conj f)) x✝ = f x✝

Tactic:
;

Goal state after:
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₁'
x✝ : M₁'
⊢ (e.symm.conj (e.conj f)) x✝ = f x✝
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✝⁵ : 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₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), f c ∈ p
⊢ comap f ⊥ = f.ker

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
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₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), f c ∈ p
⊢ comap f ⊥ = f.ker
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₂'
x✝ : M₂'
⊢ (e.conj LinearMap.id) x✝ = LinearMap.id x✝

Tactic:
;

Goal state after:
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₂'
x✝ : M₂'
⊢ (e.conj LinearMap.id) x✝ = LinearMap.id x✝
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✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x✝ : ↥f.ker
⊢ (f.domRestrict f.ker) x✝ = 0 x✝

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
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₂
f : M →ₛₗ[τ₁₂] M₂
x✝ : ↥f.ker
⊢ (f.domRestrict f.ker) x✝ = 0 x✝
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
x✝ : 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 := ⋯ })
      x✝ =
    1 x✝

Tactic:
;

Goal state after:
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
x✝ : 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 := ⋯ })
      x✝ =
    1 x✝
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
x✝² x✝¹ : Aˣ
x✝ : A
⊢ (let __spread.0 := (x✝² * x✝¹).mulLeft;
      let __spread.1 := LinearMap.mulLeft R ↑(x✝² * x✝¹);
      { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
        right_inv := ⋯ })
      x✝ =
    ((let __spread.0 := x✝².mulLeft;
        let __spread.1 := LinearMap.mulLeft R ↑x✝²;
        { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
          right_inv := ⋯ }) *
        let __spread.0 := x✝¹.mulLeft;
        let __spread.1 := LinearMap.mulLeft R ↑x✝¹;
        { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
          right_inv := ⋯ })
      x✝

Tactic:
;

Goal state after:
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
x✝² x✝¹ : Aˣ
x✝ : A
⊢ (let __spread.0 := (x✝² * x✝¹).mulLeft;
      let __spread.1 := LinearMap.mulLeft R ↑(x✝² * x✝¹);
      { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
        right_inv := ⋯ })
      x✝ =
    ((let __spread.0 := x✝².mulLeft;
        let __spread.1 := LinearMap.mulLeft R ↑x✝²;
        { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
          right_inv := ⋯ }) *
        let __spread.0 := x✝¹.mulLeft;
        let __spread.1 := LinearMap.mulLeft R ↑x✝¹;
        { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
          right_inv := ⋯ })
      x✝
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✝⁶ : 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 τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
x✝ : ↥p
⊢ x✝ ∈ (f.submoduleMap p).ker ↔ x✝ ∈ comap p.subtype f.ker

Tactic:
;

Goal state after:
R : Type u_1
R₂ : Type u_2
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 τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
x✝ : ↥p
⊢ x✝ ∈ (f.submoduleMap p).ker ↔ x✝ ∈ comap p.subtype f.ker
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₂
x✝ : M
⊢ x✝ ∈ (-f).ker ↔ x✝ ∈ f.ker

Tactic:
;

Goal state after:
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₂
x✝ : M
⊢ x✝ ∈ (-f).ker ↔ x✝ ∈ f.ker
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_9
A : Type u_10
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b : Aˣ
x✝ : A
⊢ (mulRightLinearEquiv R a ≪≫ₗ mulRightLinearEquiv R b) x✝ = (mulRightLinearEquiv R (a * b)) x✝

Tactic:
;

Goal state after:
R : Type u_9
A : Type u_10
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b : Aˣ
x✝ : A
⊢ (mulRightLinearEquiv R a ≪≫ₗ mulRightLinearEquiv R b) x✝ = (mulRightLinearEquiv R (a * b)) x✝
Module: Mathlib.Algebra.Group.ULift

Goal state before:
pp: α : Type u
β : Type v
x y : ULift α
inst✝ : MulOneClass α
x✝ y✝ : ULift α
⊢ Equiv.ulift (x✝ * y✝) = Equiv.ulift x✝ * Equiv.ulift y✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
x y : ULift α
inst✝ : MulOneClass α
x✝ y✝ : ULift α
⊢ Equiv.ulift (x✝ * y✝) = Equiv.ulift x✝ * Equiv.ulift y✝
Module: Mathlib.Algebra.GroupWithZero.ULift

Goal state before:
pp: α : Type u
inst✝ : MulZeroOneClass α
a✝ b✝ : ULift α
⊢ Equiv.ulift (a✝ * b✝) = Equiv.ulift a✝ * Equiv.ulift b✝

Tactic:
;

Goal state after:
α : Type u
inst✝ : MulZeroOneClass α
a✝ b✝ : ULift α
⊢ Equiv.ulift (a✝ * b✝) = Equiv.ulift a✝ * Equiv.ulift b✝
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 ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬map f p ≤ q

Tactic:
;

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₂
p : Submodule R M
q : Submodule R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
h : comap f q ≤ p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬map f p ≤ q
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
n : ℕ
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 2 ≠ 0

Tactic:
;

Goal state after:
α : Type u_1
R : Type u_2
S : Type u_3
n : ℕ
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 2 ≠ 0
Module: Mathlib.Algebra.Module.ULift

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ (c • 0).down = down 0

Tactic:
;

Goal state after:
R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ (c • 0).down = down 0
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
a b : ℕ
h : ↑a = ↑b
⊢ a = b

Tactic:
;

Goal state after:
R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
a b : ℕ
h : ↑a = ↑b
⊢ a = b
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
val✝ : M
h₁ : val✝ ∈ p
h₂ : ⟨val✝, h₁⟩ ∈ ↑(comap p.subtype p')
⊢ p.subtype ⟨val✝, h₁⟩ ∈ p ⊓ p'

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
val✝ : M
h₁ : val✝ ∈ p
h₂ : ⟨val✝, h₁⟩ ∈ ↑(comap p.subtype p')
⊢ p.subtype ⟨val✝, h₁⟩ ∈ p ⊓ p'
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
f : M →ₗ[R] M₂
p : Submodule R M₂
x✝ : M
⊢ x✝ ∈ comap (-f) p ↔ x✝ ∈ comap f p

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
f : M →ₗ[R] M₂
p : Submodule R M₂
x✝ : M
⊢ x✝ ∈ comap (-f) p ↔ x✝ ∈ comap f p
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
b : V
⊢ b ∈ comap (a • f) p ↔ b ∈ comap f p

Tactic:
;

Goal state after:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
b : V
⊢ b ∈ comap (a • f) p ↔ b ∈ comap f p
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 τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y ∈ p, ↑e y = x) ↔ e.symm x ∈ p

Tactic:
;

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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y ∈ p, ↑e y = x) ↔ e.symm x ∈ p
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: case mpr
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 τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ e.symm x ∈ p → ∃ y ∈ p, ↑e y = x

Tactic:
· intro hx
    exact ⟨e.symm x, hx, by simp⟩

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
hg : ↑sg = ↑sa
⊢ ∀ {a b : R}, a ∈ ↑sa → b ∈ ↑sa → a + b ∈ ↑sa

Tactic:
;

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
hg : ↑sg = ↑sa
⊢ ∀ {a b : R}, a ∈ ↑sa → b ∈ ↑sa → a + b ∈ ↑sa
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

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

Tactic:
;

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
hg : ↑sg = ↑sa
⊢ 0 ∈ ↑sa
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
ha : ↑sa = ↑sg
⊢ ∀ {a b : R}, a ∈ ↑sg → b ∈ ↑sg → a * b ∈ ↑sg

Tactic:
;

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
ha : ↑sa = ↑sg
⊢ ∀ {a b : R}, a ∈ ↑sg → b ∈ ↑sg → a * b ∈ ↑sg
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
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
p' : Submodule R ↥p
x : M₂
property✝ : f.toAddHom.1 x ∈ p
h : ⟨f.toAddHom.1 x, property✝⟩ ∈ ↑p'
⊢ x ∈ comap (codRestrict p f hf) p'

Tactic:
;

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
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
p' : Submodule R ↥p
x : M₂
property✝ : f.toAddHom.1 x ∈ p
h : ⟨f.toAddHom.1 x, property✝⟩ ∈ ↑p'
⊢ x ∈ comap (codRestrict p f hf) p'
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) ∈ s

Tactic:
;

Goal state after:
S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) ∈ s
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: case mk
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
q : Subsemiring R
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) q
⊢ { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ } = q

Tactic:
;

Goal state after:
case mk
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
q : Subsemiring R
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) q
⊢ { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ } = q