mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mul.add_right
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ y✝ z✝ x✝ : R
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₁ : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₂ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * (y✝ + z✝) ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simpa using

Goal state after:
case mul.add_right
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ y✝ z✝ x✝ : R
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₁ : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₂ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * y✝ + x✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mul.neg_left
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ -x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simpa using

Goal state after:
case mul.neg_left
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mul.neg_right
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * -y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simpa using

Goal state after:
case mul.neg_right
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subring R
⊢ ⇑f '' ⋂ i, ↑(s i) = ⋂ i, ⇑f '' ↑(s i)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ p ∣ a ∨ p ∣ b

Tactic:
refine
        (hp.2.2 (f a) (f b) <| by
              convert! map_dvd f h
              simp).imp
          ?_ ?_

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f a → p ∣ a

case refine_2
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f b → p ∣ b
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
⊢ p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
⊢ x * (y * (p ^ k * p ^ l)) = p * (z * (p ^ k * p ^ l))
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
S : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : SetLike S M₀
inst✝ : SubmonoidClass S M₀
s : S
x : ↥s
hx : Irreducible x
h : ↑x = 0
⊢ IsUnit x

Tactic:
simpa using

Goal state after:
M₀ : Type u_1
S : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : SetLike S M₀
inst✝ : SubmonoidClass S M₀
s : S
x : ↥s
hx : Irreducible x
h : ↑x = 0
⊢ IsUnit x
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : MonoidWithZero M
a : M
h✝ : a ~ᵤ 0
u : Mˣ
h : 0 * ↑u = a
⊢ a = 0

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : MonoidWithZero M
a : M
h✝ : a ~ᵤ 0
u : Mˣ
h : 0 * ↑u = a
⊢ a = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
u : Mˣ
h : a * b * ↑u = 1
⊢ a * (b * ↑u) = 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a b : M
u : Mˣ
h : a * b * ↑u = 1
⊢ a * (b * ↑u) = 1
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c : M
hba : a * c ∣ a
⊢ a ~ᵤ a * c

Tactic:
rcases hba with ⟨d, a_eq⟩

Goal state after:
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
⊢ a ~ᵤ a * c
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero M₀'
r x y : M₀
inst✝¹ : Nontrivial M₀
inst✝ : IsLeftCancelMulZero M₀
z x✝¹ x✝ : ↥M₀⁰
h : (fun x ↦ z * x) x✝¹ = (fun x ↦ z * x) x✝
⊢ ↑z * ↑x✝¹ = ↑z * ↑x✝

Tactic:
simpa using

Goal state after:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero M₀'
r x y : M₀
inst✝¹ : Nontrivial M₀
inst✝ : IsLeftCancelMulZero M₀
z x✝¹ x✝ : ↥M₀⁰
h : (fun x ↦ z * x) x✝¹ = (fun x ↦ z * x) x✝
⊢ ↑z * ↑x✝¹ = ↑z * ↑x✝
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero M₀'
r x y : M₀
inst✝¹ : Nontrivial M₀
inst✝ : IsRightCancelMulZero M₀
z x✝¹ x✝ : ↥M₀⁰
h : (fun x ↦ x * z) x✝¹ = (fun x ↦ x * z) x✝
⊢ ↑x✝¹ * ↑z = ↑x✝ * ↑z

Tactic:
simpa using

Goal state after:
F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero M₀'
r x y : M₀
inst✝¹ : Nontrivial M₀
inst✝ : IsRightCancelMulZero M₀
z x✝¹ x✝ : ↥M₀⁰
h : (fun x ↦ x * z) x✝¹ = (fun x ↦ x * z) x✝
⊢ ↑x✝¹ * ↑z = ↑x✝ * ↑z
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y → Prime (x * y)

Tactic:
· rintro (⟨hx, hy⟩ | ⟨hx, hy⟩)
    · exact (associated_mul_unit_left x y hy).symm.prime hx
    · exact (associated_unit_mul_right y x hx).prime hy

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
t : Subring S
h : t ≤ f.range
⊢ map f (comap f t) = t

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
t : Subring S
h : t ≤ f.range
⊢ map f (comap f t) = t
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ x, a * x ~ᵤ b) → ∃ c, b = a * c

Tactic:
rintro ⟨x, u, rfl⟩
    exact ⟨_, mul_assoc ..⟩

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
x y : M
u : Mˣ
h : ∀ ⦃a b : M⦄, x * y * ↑u = a * b → IsUnit a ∨ IsUnit b
⊢ IsUnit x ∨ IsUnit y

Tactic:
simpa using

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
x y : M
u : Mˣ
h : ∀ ⦃a b : M⦄, x * y * ↑u = a * b → IsUnit a ∨ IsUnit b
⊢ IsUnit x ∨ IsUnit y
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime (Associates.mk p)
m : M
hle : Associates.mk m ≤ Associates.mk p
⊢ Associates.mk m = 1 ∨ Associates.mk m = Associates.mk p

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime (Associates.mk p)
m : M
hle : Associates.mk m ≤ Associates.mk p
⊢ IsUnit m ∨ p ~ᵤ m
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomSurjective τ₂₁
p : Submodule R M
f : M₂ →ₛₗ[τ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
⊢ (codRestrict p f hf).range = comap p.subtype f.range

Tactic:
simpa using

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomSurjective τ₂₁
p : Submodule R M
f : M₂ →ₛₗ[τ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
⊢ map (codRestrict p f hf) ⊤ = comap p.subtype (map f ⊤)
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
⊢ range 0 = ⊥

Tactic:
simpa using

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
⊢ map 0 ⊤ = ⊥
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : LeftInverse ⇑g ⇑f
x : P
hx : x ∈ (f ∘ₗ g - id).ker
⊢ f (g x) = x

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : LeftInverse ⇑g ⇑f
x : P
hx : x ∈ (f ∘ₗ g - id).ker
⊢ f (g x) = x
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
y : R
x : A₁
h : (algebraMap R A₂) y = e x
⊢ (algebraMap R A₁) y = x

Tactic:
simpa using

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
y : R
x : A₁
h : (algebraMap R A₂) y = e x
⊢ (algebraMap R A₁) y = x
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
⊢ f.ker ≤ p

Tactic:
rw [SetLike.le_def]

Goal state after:
case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
⊢ ∀ ⦃x : M⦄, x ∈ f.ker → x ∈ p
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : R
⊢ e.symm (e 1 * (algebraMap R A) x) = e.symm (x • e 1)

Tactic:
rw [Algebra.smul_def, mul_comm]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ (c • f).range ≤ f.range

Tactic:
simpa using

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ Submodule.map (c • f) ⊤ ≤ Submodule.map f ⊤
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: K : Type u_4
V : Type u_8
V₂ : Type u_9
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
a : K
h : a ≠ 0
⊢ (a • f).range = f.range

Tactic:
simpa using

Goal state after:
K : Type u_4
V : Type u_8
V₂ : Type u_9
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
a : K
h : a ≠ 0
⊢ Submodule.map (a • f) ⊤ = Submodule.map f ⊤
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: K : Type u_4
V : Type u_8
V₂ : Type u_9
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
a : K
⊢ (a • f).range = ⨆ (_ : a ≠ 0), f.range

Tactic:
simpa using

Goal state after:
K : Type u_4
V : Type u_8
V₂ : Type u_9
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
a : K
⊢ Submodule.map (a • f) ⊤ = ⨆ (_ : a ≠ 0), Submodule.map f ⊤
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.subtype.range = p

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.subtype.range = p
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
p' : Submodule R ↥p
⊢ map p.subtype p' ≤ p

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
p' : Submodule R ↥p
⊢ map p.subtype p' ≤ p
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q r : Submodule R M
h : comap p.subtype q ≤ comap p.subtype r
⊢ p ⊓ q ≤ p ⊓ r

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q r : Submodule R M
h : comap p.subtype q ≤ comap p.subtype r
⊢ p ⊓ q ≤ r
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q r : Submodule R M
h : p ⊓ q ≤ p ⊓ r
⊢ comap p.subtype q ≤ comap p.subtype r

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q r : Submodule R M
h : p ⊓ q ≤ p ⊓ r
⊢ comap p.subtype q ≤ comap p.subtype r
Module: Mathlib.Algebra.Module.Submodule.Equiv

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
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective ⇑f
h : p ≤ f.range
x y : ↥(comap f p)
hxy :
  (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) x = (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) y
⊢ x = y

Tactic:
simpa using

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
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective ⇑f
h : p ≤ f.range
x y : ↥(comap f p)
hxy :
  (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) x = (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) y
⊢ x = y
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
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
⊢ x ∈ {r} • N ↔ ∃ m ∈ N, x = r • m

Tactic:
fconstructor
  · intro hx
    induction x, hx using Submodule.set_smul_inductionOn with
    | smul₀ => aesop
    | @smul₁ t n mem h =>
      rcases h with ⟨n, hn, rfl⟩
      exact ⟨t • n, by aesop, smul_comm _ _ _⟩
    | add mem₁ mem₂ h₁ h₂ =>
      rcases h₁ with ⟨m₁, h₁, rfl⟩
      rcases h₂ with ⟨m₂, h₂, rfl⟩
      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
    | zero => exact ⟨0, Submodule.zero_mem _, by simp⟩
  · aesop

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
c₁ c₂ : ClosureOperator α
h : ∀ (x : α), c₁.IsClosed x ↔ c₂.IsClosed x
x : α
⊢ IsGLB {y | x ≤ y ∧ c₁.IsClosed y} (c₂ x)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
c₁ c₂ : ClosureOperator α
h : ∀ (x : α), c₁.IsClosed x ↔ c₂.IsClosed x
x : α
⊢ IsGLB {y | x ≤ y ∧ c₂.IsClosed y} (c₂ x)
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₀ : Codisjoint a b
h₁ : Disjoint b c
h₂ : a ≤ c
⊢ c ≤ a

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₀ : Codisjoint a b
h₁ : Disjoint b c
h₂ : a ≤ c
⊢ c ≤ a
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case smul.add
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y x✝ y✝ : M
hx✝ : x✝ ∈ closure (univ • s)
hy✝ : y✝ ∈ closure (univ • s)
h₁ : r₁ • x✝ ∈ closure (univ • s)
h₂ : r₁ • y✝ ∈ closure (univ • s)
⊢ r₁ • (x✝ + y✝) ∈ closure (univ • s)

Tactic:
simpa using

Goal state after:
case smul.add
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y x✝ y✝ : M
hx✝ : x✝ ∈ closure (univ • s)
hy✝ : y✝ ∈ closure (univ • s)
h₁ : r₁ • x✝ ∈ closure (univ • s)
h₂ : r₁ • y✝ ∈ closure (univ • s)
⊢ r₁ • x✝ + r₁ • y✝ ∈ closure (univ • s)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ ∀ (x y : M) (hx : x ∈ closure (univ • s)) (hy : y ∈ closure (univ • s)), p x ⋯ → p y ⋯ → p (x + y) ⋯

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ ∀ (x y : M) (hx : x ∈ closure (univ • s)) (hy : y ∈ closure (univ • s)), p x ⋯ → p y ⋯ → p (x + y) ⋯
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
d : α
hdisjoint : Disjoint b d
hcodisjoint : Codisjoint b d
⊢ b ⊓ ((d ⊔ a) ⊓ c) = a

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
d : α
hdisjoint : Disjoint b d
hcodisjoint : Codisjoint b d
⊢ a ≤ c
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
⊢ span R (⋃ S ∈ s, ↑S) = sSup s

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
⊢ span R (⋃ S ∈ s, ↑S) = sSup s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F β α
inst✝ : SupHomClass F β α
hs : SupClosed s
f : F
a : β
ha : a ∈ ⇑f ⁻¹' s
b : β
hb : b ∈ ⇑f ⁻¹' s
⊢ a ⊔ b ∈ ⇑f ⁻¹' s

Tactic:
simpa using

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F β α
inst✝ : SupHomClass F β α
hs : SupClosed s
f : F
a : β
ha : a ∈ ⇑f ⁻¹' s
b : β
hb : b ∈ ⇑f ⁻¹' s
⊢ f a ⊔ f b ∈ s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
⊢ SupClosed (range ⇑f)

Tactic:
simpa using

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
⊢ SupClosed (range ⇑f)
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑u ×ˢ ↑v ⊆ s ×ˢ t
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
a b : R
⊢ ∃ a_1, a_1 • y = a • y + b • y

Tactic:
exact ⟨a + b, by simp [add_smul]⟩

Goal state after: