mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x y : M
⊢ x ~ᵤ y ↔ x = y

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
⊢ Associated = Eq

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
⊢ C x

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
p q : M
pp : Prime p
qp : Prime q
⊢ p ∣ q ↔ p = q

Tactic:
by

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S✝
inst✝¹ : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝ : SMul R α
S : Subring R
⊢ SMul (↥S) α

Tactic:
by

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝² : SMul R β
inst✝¹ : SMul α β
inst✝ : SMulCommClass R α β
S : Subring R
⊢ SMulCommClass (↥S) α β

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂

Tactic:
by

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝² : SMul α β
inst✝¹ : SMul R β
inst✝ : SMulCommClass α R β
S : Subring R
⊢ SMulCommClass α (↥S) β

Tactic:
by

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝⁶ : NonAssocRing R
inst✝⁵ : NonAssocRing S✝
inst✝⁴ : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝³ : SMul α β
inst✝² : SMul R α
inst✝¹ : SMul R β
inst✝ : IsScalarTower R α β
S : Subring R
⊢ IsScalarTower (↥S) α β

Tactic:
by

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝⁴ : NonAssocRing R
inst✝³ : NonAssocRing S✝
inst✝² : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝¹ : SMul R α
inst✝ : FaithfulSMul R α
S : Subring R
⊢ FaithfulSMul (↥S) α

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁴ : NonAssocRing R✝
inst✝³ : NonAssocRing S✝
inst✝² : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝¹ : Ring R
inst✝ : MulAction R α
S : Subring R
⊢ MulAction (↥S) α

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝² : Ring R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
S : Subring R
⊢ DistribMulAction (↥S) α

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Associates M
⊢ Associates.mk (Quot.out a) = a

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝² : Ring R
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction R α
S : Subring R
⊢ MulDistribMulAction (↥S) α

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
⊢ Quot.out (Associates.mk a) ~ᵤ a

Tactic:
by

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝⁴ : NonAssocRing R
inst✝³ : NonAssocRing S✝
inst✝² : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝¹ : Zero α
inst✝ : SMulWithZero R α
S : Subring R
⊢ SMulWithZero (↥S) α

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝² : Ring R
inst✝¹ : Zero α
inst✝ : MulActionWithZero R α
S : Subring R
⊢ MulActionWithZero (↥S) α

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
⊢ Associates.mk a = 1 ↔ IsUnit a

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝² : Ring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
S : Subring R
⊢ Module (↥S) α

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝² : Ring R
inst✝¹ : Semiring α
inst✝ : MulSemiringAction R α
S : Subring R
⊢ MulSemiringAction (↥S) α

Tactic:
by

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

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
hf : Function.Surjective ⇑f
t : Subring S
⊢ t ≤ f.range

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ M₀⁰ ∧ b ∈ M₀⁰

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
n : ℕ
⊢ Associates.mk (a ^ n) = Associates.mk a ^ n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
u : (Associates M)ˣ
⊢ ↑u = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : Associates M
⊢ IsUnit a ↔ a = ⊥

Tactic:
by

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

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ IsUnit (Associates.mk a) ↔ a ~ᵤ 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b c d : Associates M
h₁ : a ≤ b
h₂ : c ≤ d
x : Associates M
hx : b = a * x
y : Associates M
hy : d = c * y
⊢ b * d = a * c * (x * y)

Tactic:
by

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
⊢ b = a * ⟨c, ⋯⟩

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
x : G₀
u : G₀ˣ
⊢ (fun u ↦ Units.mk0 ↑u ⋯) ((fun u ↦ ⟨↑u, ⋯⟩) u) = u

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
x : G₀
u v : ↥G₀⁰
⊢ Units.mk0 ↑(u * v) ⋯ = Units.mk0 ↑u ⋯ * Units.mk0 ↑v ⋯

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ b * a

Tactic:
by

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

Goal state before:
pp: M₀ : Type ?u.3
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
u : M₀ˣ
⊢ ⟨↑u, ⋯⟩ * ⟨↑u⁻¹, ⋯⟩ = 1

Tactic:
by

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

Goal state before:
pp: M₀ : Type ?u.3
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
u : M₀ˣ
⊢ ⟨↑u⁻¹, ⋯⟩ * ⟨↑u, ⋯⟩ = 1

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ b_1, ↑a * ↑(unitsNonZeroDivisorsEquiv.symm.symm b_1) = ↑b) ↔ Associated a b

Tactic:
by

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

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

Tactic:
by

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
s : Subring R
x y : R
hy : y ∈ s
hxy : f y = f x
⊢ x - y ∈ ⇑f ⁻¹' {0}

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
x✝ : ∃ x, x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ Associates.mk b ≠ 0

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : MonoidWithZero M
⊢ Quot.out 0 = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ 0 * Associates.mk a = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk a * 0 = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
⊢ Prime (Associates.mk p) ↔ Prime p

Tactic:
by

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
s : Subring R
⊢ comap f (map f s) = s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰

Tactic:
by

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

Goal state before:
pp: M₀✝ : ?m.1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ ∀ (a : M₀), a ∈ M₀⁰ ↔ ⟦a⟧ ∈ (Quotient (Associated.setoid M₀))⁰

Tactic:
by

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

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

Tactic:
by

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
s : Subring R
h : ⇑f ⁻¹' {0} ⊆ ↑s
⊢ comap f (map f s) = s

Tactic:
by

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

Goal state before:
pp: M₀✝ : ?m.1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ ∀ (x y : ↥M₀⁰), (Associated.setoid ↥M₀⁰) x y ↔ (Associated.setoid M₀) ↑x ↑y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ ↑k * g ∈ G

Tactic:
by

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

Goal state before:
pp: M₀✝ : ?m.1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ ∀ (x y : ↥(Associates M₀)⁰),
    (Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x ∈ M₀⁰) (fun x ↦ x ∈ (Quotient (Associated.setoid M₀))⁰) ⋯
            ⋯).toFun
        (x * y) =
      (Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x ∈ M₀⁰) (fun x ↦ x ∈ (Quotient (Associated.setoid M₀))⁰) ⋯
              ⋯).toFun
          x *
        (Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x ∈ M₀⁰) (fun x ↦ x ∈ (Quotient (Associated.setoid M₀))⁰) ⋯
              ⋯).toFun
          y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a b : Associates M
hlt : a < b
⊢ DvdNotUnit a b

Tactic:
by

Goal state after:
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:
by

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✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.range = map f ⊤

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a✝ : Associates M
a : M
ha : Quot.mk (⇑(Associated.setoid M)) a ≠ 0
a₁✝ : Associates M
b : M
a₂✝ : Associates M
c : M
h :
  (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) b) =
    (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) c)
u : Mˣ
hu : (fun x1 x2 ↦ x1 * x2) a b * ↑u = (fun x1 x2 ↦ x1 * x2) a c
⊢ a * (b * ↑u) = a * c

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
⊢ ∀ {a : Associates M}, a ≠ 0 → IsLeftRegular a

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
⊢ NoZeroDivisors (Associates M)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c : Associates M
ha : a ≠ 0
d : Associates M
hd : a * c = a * b * d
⊢ a * c = a * (b * d)

Tactic:
by

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✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.range = ⊤ ↔ Surjective ⇑f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
⊢ p ≤ 1 ↔ p = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q r : M
h : DvdNotUnit p q
h' : q ~ᵤ r
⊢ DvdNotUnit p r

Tactic:
by

Goal state after:
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
⊢ q ≠ 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q r : M
h : DvdNotUnit p r
h' : p ~ᵤ q
⊢ DvdNotUnit q r

Tactic:
by

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✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f g : M →ₛₗ[τ₁₂] M₂
⊢ (f + g).range ≤ f.range ⊔ g.range

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p b : M
h : p * b ~ᵤ p
hp : p ≠ 0
⊢ IsUnit b

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q : M
h : DvdNotUnit p q
⊢ ¬p ~ᵤ q

Tactic:
by

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✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
⊢ f.range ≤ p ↔ comap f p = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ (-f).range = f.range

Tactic:
by

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✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
K : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (f.domRestrict K).range = map f K

Tactic:
by

Goal state after:
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 f g : A₁ ≃ₐ[R] A₂
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by

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✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
⊢ (f.domRestrict S).range ≤ f.range

Tactic:
by

Goal state after:
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
f : M →ₗ[R] M
n : ℕ
⊢ f.iterateRange (n + 1) = map f (f.iterateRange n)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q : M
hp : Prime p
n : ℕ
⊢ q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i

Tactic:
by

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✝⁵ : 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:
by

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✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
q : Submodule R₂ M₂
⊢ f.range ⊓ q ≤ map f (comap f q)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MulZeroClass α
s : Set α
⊢ s * 0 ⊆ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MulZeroClass α
s : Set α
⊢ 0 * s ⊆ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MulZeroClass α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s * 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MulZeroClass α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ 0 * s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
s : Set α
⊢ s / 0 ⊆ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
s : Set α
⊢ 0 / s ⊆ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s / 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ 0 / s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
⊢ 0⁻¹ = 0

Tactic:
by

Goal state after:
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₂
r : R
⊢ e.toRingEquiv.symm.toFun ((algebraMap R A₂) r) = (algebraMap R A₁) r

Tactic:
by

Goal state after:
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₂
⊢ (↑e).comp ↑e.symm = AlgHom.id R A₂

Tactic:
by

Goal state after: