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

Goal state before:
pp: case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : ↑e₁₂ ∘ₛₗ f = g
x✝ : M₃
⊢ f x✝ = (↑e₁₂.symm ∘ₛₗ g) x✝

Tactic:
·

Goal state after:
case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : ↑e₁₂ ∘ₛₗ f = g
x✝ : M₃
⊢ f x✝ = (↑e₁₂.symm ∘ₛₗ g) x✝
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : ↑e₁₂.symm ∘ₛₗ g = f
x✝ : M₃
⊢ g x✝ = (↑e₁₂ ∘ₛₗ f) x✝

pp: case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : g = ↑e₁₂ ∘ₛₗ f
x✝ : M₃
⊢ (↑e₁₂.symm ∘ₛₗ g) x✝ = f x✝

Tactic:
·

Goal state after:
case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : ↑e₁₂.symm ∘ₛₗ g = f
x✝ : M₃
⊢ g x✝ = (↑e₁₂ ∘ₛₗ f) x✝
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : g = ↑e₁₂ ∘ₛₗ f
x✝ : M₃
⊢ (↑e₁₂.symm ∘ₛₗ g) x✝ = f x✝

Tactic:
·

Goal state after:
case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : g = ↑e₁₂ ∘ₛₗ f
x✝ : M₃
⊢ (↑e₁₂.symm ∘ₛₗ g) x✝ = f x✝
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_14
M : Type u_15
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ IsLinearMap R fun z ↦ c • z

Tactic:
refine IsLinearMap.mk (smul_add c) ?_
  intro _ _
  simp only [smul_smul, mul_comm]

Goal state after:
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
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
α : Sˣ
e : V ≃ₗ[R] W
x✝ : W
⊢ (↑α • ↑e).toFun ((fun x ↦ ↑α⁻¹ • e.symm x) x✝) = x✝

Tactic:
simp [smul_smul]

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

Goal state before:
pp: case inl
M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
h✝ : Subsingleton α
⊢ m₁✝ = m₂✝

pp: case inr
M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
h✝ : Nontrivial α
⊢ m₁✝ = m₂✝

Tactic:
·

Goal state after:
case inl
M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
h✝ : Subsingleton α
⊢ m₁✝ = m₂✝
Module: Mathlib.Algebra.GroupWithZero.Action.Opposite

Goal state before:
pp: case inr
M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
h✝ : Nontrivial α
⊢ m₁✝ = m₂✝

Tactic:
·

Goal state after:
case inr
M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
h✝ : Nontrivial α
⊢ m₁✝ = m₂✝
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R'
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁵ : Monoid S'
inst✝⁴ : DistribMulAction S' M
inst✝³ : SMulCommClass R S' M
inst✝² : Monoid T'
inst✝¹ : DistribMulAction T' M
inst✝ : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
x y : M
⊢ (a • ⇑f) (x + y) = (a • ⇑f) x + (a • ⇑f) y

Tactic:
by simp only [DomMulAct.smul_apply, f.map_add, smul_add]

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

Goal state before:
pp: case e_3
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 α
⊢ compHom α (MonoidHom.inl M N) = fst✝

pp: case e_4
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 α
⊢ ⟨compHom α (MonoidHom.inr M N), ⋯⟩ ≍ ⟨x, snd✝⟩

Tactic:
·

Goal state after:
case e_3
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 α
⊢ compHom α (MonoidHom.inl M N) = fst✝
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 α
⊢ (fun x_1 ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α

pp: case e_4.e_3
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 α
⊢ compHom α (MonoidHom.inr M N) = x

pp: case e_4.e_4
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 α
⊢ ⋯ ≍ snd✝

Tactic:
·

Goal state after:
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 α
⊢ (fun x_1 ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4.e_3
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 α
⊢ compHom α (MonoidHom.inr M N) = x

pp: case e_4.e_4
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 α
⊢ ⋯ ≍ snd✝

Tactic:
·

Goal state after:
case e_4.e_3
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 α
⊢ compHom α (MonoidHom.inr M N) = x
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4.e_4
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 α
⊢ ⋯ ≍ snd✝

Tactic:
·

Goal state after:
case e_4.e_4
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 α
⊢ ⋯ ≍ snd✝
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(∅.inf p) = ⋂ i ∈ ∅, ↑(p i)

pp: case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑((insert i s).inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(∅.inf p) = ⋂ i ∈ ∅, ↑(p i)
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑((insert i s).inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑((insert i s).inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: case e'_2
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✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ e (c • a) = e.toAddMonoidHom (c • a)

pp: case e'_3
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✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ c • e a = c • e.toAddMonoidHom a

Tactic:
·

Goal state after:
case e'_2
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✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ e (c • a) = e.toAddMonoidHom (c • a)
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: case e'_3
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✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ c • e a = c • e.toAddMonoidHom a

Tactic:
·

Goal state after:
case e'_3
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✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ c • e a = c • e.toAddMonoidHom a
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right
  rw [LE.le] at this
  exact this

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup s ≤ p

pp: case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup s ≤ p
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: case inl
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 α
x✝ : CompleteLattice β
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' ∅)

pp: case inr
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 α
x✝ : CompleteLattice β
s : Set α
hs : s.Nonempty
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' s)

Tactic:
·

Goal state after:
case inl
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 α
x✝ : CompleteLattice β
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' ∅)
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: case inr
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 α
x✝ : CompleteLattice β
s : Set α
hs : s.Nonempty
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' s)

Tactic:
·

Goal state after:
case inr
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 α
x✝ : CompleteLattice β
s : Set α
hs : s.Nonempty
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' s)
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:
rw [← Nat.cast_two, Nat.cast_ne_zero]

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.Submodule.Map

Goal state before:
pp: case mp
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

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:
·

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

Goal state after:
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
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
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s

Tactic:
by subst ha; exact sa.add_mem

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

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 * ↑u = ↑u * 0

pp: case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * ↑u = ↑u * a

Tactic:
·

Goal state after:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 * ↑u = ↑u * 0
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * ↑u = ↑u * a

Tactic:
·

Goal state after:
case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * ↑u = ↑u * a
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0⁻¹ ∈ s.centralizer

pp: case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
⊢ a⁻¹ ∈ s.centralizer

Tactic:
·

Goal state after:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0⁻¹ ∈ s.centralizer
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
⊢ a⁻¹ ∈ s.centralizer

Tactic:
·

Goal state after:
case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
⊢ a⁻¹ ∈ s.centralizer
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
x✝ : M
⊢ x✝ ∈ ⋃ i, ↑(S i) → ∃ i, x✝ ∈ S i

pp: case refine_2
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
⊢ ∀ (x y : M),
    x ∈ closure (⋃ i, ↑(S i)) → y ∈ closure (⋃ i, ↑(S i)) → (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i

Tactic:
·

Goal state after:
case refine_1
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
x✝ : M
⊢ x✝ ∈ ⋃ i, ↑(S i) → ∃ i, x✝ ∈ S i
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ (∃ i, x ∈ S ↑i) ↔ ∃ i, p i ∧ x ∈ S i

pp: case hS
M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ S ↑x

Tactic:
·

Goal state after:
M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ (∃ i, x ∈ S ↑i) ↔ ∃ i, p i ∧ x ∈ S i
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case pos
M : Type u_2
inst✝ : Mul M
p : Prop
S : p → Subsemigroup M
x : M
h : p
⊢ x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h

pp: case neg
M : Type u_2
inst✝ : Mul M
p : Prop
S : p → Subsemigroup M
x : M
h : ¬p
⊢ x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h

Tactic:
·

Goal state after:
case pos
M : Type u_2
inst✝ : Mul M
p : Prop
S : p → Subsemigroup M
x : M
h : p
⊢ x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case neg
M : Type u_2
inst✝ : Mul M
p : Prop
S : p → Subsemigroup M
x : M
h : ¬p
⊢ x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h

Tactic:
·

Goal state after:
case neg
M : Type u_2
inst✝ : Mul M
p : Prop
S : p → Subsemigroup M
x : M
h : ¬p
⊢ x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : M) (x : ι), a ∈ S x → ∀ (b : M) (x : ι), b ∈ S x → a * b = b * a

Tactic:
intro a i ha b j hb

Goal state after:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
hb : b ∈ S j
⊢ a * b = b * a