mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
X : Type u_5
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul M' Y
F : Type u_8
inst✝² : FunLike F X Y
inst✝¹ : FaithfulSMul M' X
inst✝ : MulActionHomClass F M' X Y
f : F
hf : Function.Injective ⇑f
x✝¹ x✝ : M'
h : ∀ (a : Y), x✝¹ • a = x✝ • a
m : X
⊢ f (x✝¹ • m) = f (x✝ • m)

Tactic:
[

Goal state after:
M' : Type u_1
X : Type u_5
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul M' Y
F : Type u_8
inst✝² : FunLike F X Y
inst✝¹ : FaithfulSMul M' X
inst✝ : MulActionHomClass F M' X Y
f : F
hf : Function.Injective ⇑f
x✝¹ x✝ : M'
h : ∀ (a : Y), x✝¹ • a = x✝ • a
m : X
⊢ f (x✝¹ • m) = f (x✝ • m)
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f • g) 1 = g 1 • f 1

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f • g) 1 = g 1 • f 1
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ Function.Injective fun a ↦ n • a

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ Function.Injective fun a ↦ n • a
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'
c : R
x : M
⊢ (a • ⇑f) (c • x) = σ₁₂ c • (a • ⇑f) x

Tactic:
[

Goal state after:
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'
c : R
x : M
⊢ (a • ⇑f) (c • x) = σ₁₂ c • (a • ⇑f) x
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
inst✝ : SMulCommClass S' T' M
s : S'ᵈᵐᵃ
t : T'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
m : M
⊢ (s • t • f) m = (t • s • f) m

Tactic:
[

Goal state after:
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
inst✝ : SMulCommClass S' T' M
s : S'ᵈᵐᵃ
t : T'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
m : M
⊢ (s • t • f) m = (t • s • f) 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'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝³ x✝² : Sᵈᵐᵃ
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ ((x✝³ + x✝²) • x✝¹) x✝ = (x✝³ • x✝¹ + x✝² • x✝¹) x✝

Tactic:
[

Goal state after:
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'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝³ x✝² : Sᵈᵐᵃ
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ ((x✝³ + x✝²) • x✝¹) x✝ = (x✝³ • x✝¹ + x✝² • x✝¹) x✝
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
⊢ x + -y ∈ p ↔ y ∈ p

Tactic:
p.add_mem_iff_right hx,

Goal state after:
R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
⊢ -y ∈ p ↔ y ∈ p
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
b c : M
⊢ p (Exists.choose ⋯) = p (Exists.choose ⋯ + Exists.choose ⋯)

Tactic:
[

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
ι : 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
b c : M
⊢ p (Exists.choose ⋯) = p (Exists.choose ⋯ + Exists.choose ⋯)
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 : Set (Submodule R M)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).carrier
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).carrier

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).carrier
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).carrier
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
⊢ p (Exists.choose ⋯) = p (σ₁₂ r • Exists.choose ⋯)

Tactic:
[

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
ι : 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
⊢ p (Exists.choose ⋯) = p (σ₁₂ r • Exists.choose ⋯)
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case add
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, ↑i
hy✝ : y✝ ∈ ⨆ i, ↑i
⊢ t • x✝ ∈ ⨆ a, ↑a → t • y✝ ∈ ⨆ a, ↑a → t • (x✝ + y✝) ∈ ⨆ a, ↑a

Tactic:
[

Goal state after:
case add
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, ↑i
hy✝ : y✝ ∈ ⨆ i, ↑i
⊢ t • x✝ ∈ ⨆ a, ↑a → t • y✝ ∈ ⨆ a, ↑a → t • (x✝ + y✝) ∈ ⨆ a, ↑a
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ f (⨆ i, ⨆ j, g i j) = ⨆ i, ⨆ j, f (g i j)

Tactic:
[

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ f (⨆ i, ⨆ j, g i j) = ⨆ i, ⨆ j, f (g i j)
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 α
x : α × α
s : Set (α × α)
⊢ (sSup s).1 ⊔ (sSup s).2 = sSup ((fun x ↦ x.1 ⊔ x.2) '' s)

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 α
x : α × α
s : Set (α × α)
⊢ (sSup s).1 ⊔ (sSup s).2 = sSup ((fun x ↦ x.1 ⊔ x.2) '' s)
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 α
x : α × α
s : Set (α × α)
⊢ (sInf s).1 ⊓ (sInf s).2 = sInf ((fun x ↦ x.1 ⊓ x.2) '' s)

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 α
x : α × α
s : Set (α × α)
⊢ (sInf s).1 ⊓ (sInf s).2 = sInf ((fun x ↦ x.1 ⊓ x.2) '' s)
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₂
s : Set (Submodule R M)
hs : sSup s = ⊤
h : ∀ m ∈ s, f ∘ₛₗ m.subtype = 0
⊢ f = 0

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₂
s : Set (Submodule R M)
hs : sSup s = ⊤
h : ∀ m ∈ s, f ∘ₛₗ m.subtype = 0
⊢ f = 0
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ u ≠ -u

Tactic:
[

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ u ≠ -u
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
σ : R →+* R
ι : Sort u_9
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
⊢ ∀ v ∈ iInf p, f v ∈ iInf p

Tactic:
simp only [mem_iInf]

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
σ : R →+* R
ι : Sort u_9
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
⊢ ∀ (v : M), (∀ (i : ι), v ∈ p i) → ∀ (i : ι), f v ∈ p i
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ center G₀ˣ ⊆ Units.val ⁻¹' center G₀

Tactic:
[

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ center G₀ˣ ⊆ Units.val ⁻¹' center G₀
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 ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a

Tactic:
[

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 ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝ : M
⊢ -a * x✝ = x✝ * -a

Tactic:
← neg_mul_comm,

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝ : M
⊢ -a * x✝ = -x✝ * a
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h ↦ ↑H1) H2

pp: case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h ↦ ↑H1) H2

Tactic:
· exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2

Goal state after:
case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h ↦ ↑H1) H2
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a

Tactic:
[

Goal state after:
R : Type u
inst✝¹ : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
H1 : Subsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h ↦ ↑H1) H2

pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h ↦ ↑H1) H2

Tactic:
· exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2

Goal state after:
case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h ↦ ↑H1) H2
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
x✝ : S
⊢ x✝ ∈ Submonoid.map h M₀⁰ ↔ x✝ ∈ S⁰

Tactic:
[

Goal state after:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
x✝ : S
⊢ x✝ ∈ Submonoid.map h M₀⁰ ↔ x✝ ∈ S⁰
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ IsUnit y ∨ x ~ᵤ y → y ∣ x

Tactic:
· rintro (hy | h)
    · exact hy.dvd
    · exact h.symm.dvd

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : a ∣ b
c : ↥M₀⁰
hc : b = a * c
⊢ ↑a ∣ ↑b

Tactic:
[

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : a ∣ b
c : ↥M₀⁰
hc : b = a * c
⊢ ↑a ∣ ↑b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
⊢ ∀ (a : (Associates M)ˣ), a = default

Tactic:
rintro ⟨a, b, hab, hba⟩

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
hab : a * b = 1
hba : b * a = 1
⊢ { val := a, inv := b, val_inv := hab, inv_val := hba } = default
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : ↑a ∣ ↑b
c : M₀
hc : ↑b = ↑a * c
⊢ b = a * ⟨c, ⋯⟩

Tactic:
[

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : ↑a ∣ ↑b
c : M₀
hc : ↑b = ↑a * c
⊢ b = a * ⟨c, ⋯⟩
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ IsPrimal (Associates.mk a) ↔ IsPrimal a

Tactic:
[

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ IsPrimal (Associates.mk a) ↔ IsPrimal a
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
⊢ DecompositionMonoid (Associates M) ↔ DecompositionMonoid M

Tactic:
[

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
⊢ DecompositionMonoid (Associates M) ↔ DecompositionMonoid M
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b

Tactic:
[

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
⊢ (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates M), Irreducible a ↔ Prime a

Tactic:
[

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
⊢ (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates M), Irreducible a ↔ Prime a
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
⊢ DvdNotUnit q r

Tactic:
have hq : q ≠ 0 := by simp_all

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
hq : q ≠ 0
⊢ DvdNotUnit q r
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
a✝ : A₁
⊢ (e.trans ((e.symm.trans (ψ.trans e')).trans e'.symm)) a✝ = ψ a✝

Tactic:
[

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₁ ≃ₐ[R] A₁'
a✝ : A₁
⊢ (e.trans ((e.symm.trans (ψ.trans e')).trans e'.symm)) a✝ = ψ a✝
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
a✝ : A₂
⊢ (e.symm.trans ((e.trans (ψ.trans e'.symm)).trans e')) a✝ = ψ a✝

Tactic:
[

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
a✝ : A₂
⊢ (e.symm.trans ((e.trans (ψ.trans e'.symm)).trans e')) a✝ = ψ a✝
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective ⇑i
hf : ∀ (x : M₁), f x ∈ i.range
x : M₁
⊢ i ((f.codRestrictOfInjective i hi hf) x) = f x

Tactic:
by
  simp [LinearMap.codRestrictOfInjective]

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y ∈ Submodule.comap O.subtype N, ϕ y = x) → ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x

Tactic:
[

Goal state after:
case refine_1
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y ∈ Submodule.comap O.subtype N, ϕ y = x) → ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y ∈ Submodule.comap O.subtype N, ϕ y = x

Tactic:
[

Goal state after:
case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y ∈ Submodule.comap O.subtype N, ϕ y = x
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p} = Set.Ici (⨆ a ∈ s, a • N)

Tactic:
[

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p} = Set.Ici (⨆ a ∈ s, a • N)
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x z y : α
⊢ z ≤ x → x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ z

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x z y : α
⊢ z ≤ x → x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ z