mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ ∃ y_1 ∈ x, ∃ z_1 ∈ y ⊓ z, y_1 * z_1 = b * c

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ ∃ y_1 ∈ x, ∃ z_1 ∈ y ⊓ z, y_1 * z_1 = b * c
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : comap φ M ≠ ⊤
⊢ comap φ M ≠ ⊤

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : comap φ M ≠ ⊤
⊢ comap φ M ≠ ⊤
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hM : comap φ M < comap φ (map φ K) → comap φ (map φ K) = comap φ ⊤
hK : comap φ M < K
⊢ K = ⊤

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hM : comap φ M < comap φ (map φ K) → comap φ (map φ K) = comap φ ⊤
hK : comap φ M < K
⊢ K = ⊤
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hM : comap φ M < K → K = ⊤
hK : comap φ M < K
⊢ K = ⊤

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hM : comap φ M < K → K = ⊤
hK : comap φ M < K
⊢ K = ⊤
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: case h
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ((v.prod fun x1 x2 ↦ f x1 ^ x2) * w.prod fun x1 x2 ↦ f x1 ^ x2) =
    (v.prod fun x1 x2 ↦ f x1 ^ x2) * w.prod fun x1 x2 ↦ f x1 ^ x2

pp: case h.h_zero
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, f a ^ 0 = 1

pp: case h.h_add
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℕ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂

Tactic:
]

Goal state after:
case h.h_zero
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, f a ^ 0 = 1

case h.h_add
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℕ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
refine ⟨exists_finsupp_of_mem_closure_range f x, ?_⟩

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) → x ∈ closure (Set.range f)
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ b (τ a f) = τ b (τ a f)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : ∀ ⦃x : G⦄, x ∈ M → x ∈ N
⊢ ∀ ⦃x : G⦄, x ∈ N → x ∈ M

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : ∀ ⦃x : G⦄, x ∈ M → x ∈ N
⊢ ∀ ⦃x : G⦄, x ∈ N → x ∈ M
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : ∀ i ∈ f, a✝ ∈ ↑i
hy : ∀ i ∈ f, b✝ ∈ ↑i
⊢ ∀ i ∈ f, a✝ * b✝ ∈ ↑i

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : ∀ i ∈ f, a✝ ∈ ↑i
hy : ∀ i ∈ f, b✝ ∈ ↑i
⊢ ∀ i ∈ f, a✝ * b✝ ∈ ↑i
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ y✝ : M
hx✝ : x✝ ∈ s.saturation
hy✝ : y✝ ∈ s.saturation
ih₁ : ∃ y, x✝ * y ∈ s
ih₂ : ∃ y, y✝ * y ∈ s
y₁ : M
h₁ : x✝ * y₁ ∈ s
y₂ : M
h₂ : y✝ * y₂ ∈ s
⊢ x✝ * y₁ * (y✝ * y₂) ∈ s

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ y✝ : M
hx✝ : x✝ ∈ s.saturation
hy✝ : y✝ ∈ s.saturation
ih₁ : ∃ y, x✝ * y ∈ s
ih₂ : ∃ y, y✝ * y ∈ s
y₁ : M
h₁ : x✝ * y₁ ∈ s
y₂ : M
h₂ : y✝ * y₂ ∈ s
⊢ x✝ * y₁ * (y✝ * y₂) ∈ s
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₁ * x₂ * y ∈ s

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₁ * x₂ * y ∈ s
Module: Mathlib.Algebra.GroupWithZero.Action.Center

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
u : ↥(center G₀ˣ)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this : ⇑invMonoidHom ∘ v '' baseOf v f ⊆ ⇑(MonoidHom.id G) '' v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)

Tactic:
]

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
this : ⇑invMonoidHom ∘ v '' baseOf v f ⊆ ⇑(MonoidHom.id G) '' v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)
Module: Mathlib.Algebra.GroupWithZero.Conj

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
⊢ (∃ x, x ≠ 0 ∧ SemiconjBy x a b) ↔ ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a b : α
⊢ (∃ x, x ≠ 0 ∧ SemiconjBy x a b) ↔ ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi✝ : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hk : k ∈ {i | 1 < f (v i)}
hi : v i = v j⁻¹ * v k⁻¹
⊢ v i = v j⁻¹ * v k⁻¹

Tactic:
]

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi✝ : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hk : k ∈ {i | 1 < f (v i)}
hi : v i = v j⁻¹ * v k⁻¹
⊢ v i = v j⁻¹ * v k⁻¹
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hi : 1 < f (v i)
hi' : v i ∉ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
⊢ False

Tactic:
have hne : s.Nonempty := ⟨i, hi, hi'⟩

Goal state after:
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hi : 1 < f (v i)
hi' : v i ∉ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : IsLeftCancelMulZero α
hs : s = ∅ ∨ s = {0}
⊢ #s ≤ #(s * s)

Tactic:
]

Goal state after:
case inl
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : IsLeftCancelMulZero α
hs : s = ∅ ∨ s = {0}
⊢ #s ≤ #(s * s)
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
⊢ closure (v '' IsMulIndecomposable.baseOf v f) = closure (v '' univ)

Tactic:
]

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
⊢ closure (v '' IsMulIndecomposable.baseOf v f) = closure (v '' univ)
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
⊢ v '' {i | 1 < f (v i)} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f)) ∧
    v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))

Tactic:
]

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
⊢ v '' {i | 1 < f (v i)} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f)) ∧
    v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom ∘ ⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f = v '' IsMulIndecomposable.baseOf v f

Tactic:
]

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom ∘ ⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f = v '' IsMulIndecomposable.baseOf v f
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
hx : x ≠ 0
⊢ 1 = 1

pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
hx : x ≠ 0
⊢ f x ≠ 0

Tactic:
]

Goal state after:
case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
hx : x ≠ 0
⊢ f x ≠ 0
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
hx : x ≠ 0
⊢ x ≠ 0

Tactic:
]

Goal state after:
case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
x : M₀
hx : x ≠ 0
⊢ x ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ ↑0
⊢ ↑(s • univ) = ↑univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ ↑0
⊢ ↑(s • univ) = ↑univ
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x : G₀
hx : x ≠ 0
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case refine_2
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)}
⊢ v '' {i | 1 < f' (v i)} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f'))

Tactic:
]

Goal state after:
case refine_2
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)}
⊢ v '' {i | 1 < f' (v i)} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f'))
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x : H₀
hx : x ≠ 0
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Submonoid.Instances

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : GroupWithZero G
inst✝ : GroupWithZero H
f : G →*₀ H
x : ↥(MonoidHom.mrange f)
⊢ (↑x)⁻¹ ∈ MonoidHom.mrange f

Tactic:
by
    obtain ⟨y, hy⟩ := x.prop
    use y⁻¹
    simp [← hy]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
⊢ v i ∈ Submonoid.closure (v '' {i | 1 < f (v i)}) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' {i | 1 < f (v i)})

Tactic:
]

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
⊢ v i ∈ Submonoid.closure (v '' {i | 1 < f (v i)}) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' {i | 1 < f (v i)})
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝³ : Monoid M
inst✝² : LinearOrder S
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hv_one : v i ≠ 1
⊢ v i ∈ closure (v '' {i | 1 < f (v i)}) ↔ 1 < f (v i)

Tactic:
refine ⟨fun hi ↦ ?_, fun hi ↦ subset_closure <| mem_image_of_mem v hi⟩
  suffices v i = 1 ∨ 1 < f (v i) from this.resolve_left hv_one
  refine closure_induction (by grind) (by simp) (fun x y _ _ hx hy ↦ ?_) hi
  rcases hx with rfl | hx; · simpa
  rcases hy with rfl | hy; · right; simpa
  right
  simpa only [map_mul] using Left.one_lt_mul hx hy

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

Goal state before:
pp: case h
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
y : A
hy : f y = ↑a✝
y' : A
hy' : f y' = ↑b✝
⊢ ↑a✝ * ↑b✝ = ↑a✝ * ↑b✝

Tactic:
]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ Submonoid.closure (↑f.valueMonoid ∪ (↑f.valueMonoid)⁻¹) = f.valueMonoid

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ Submonoid.closure (↑f.valueMonoid ∪ (↑f.valueMonoid)⁻¹) = f.valueMonoid
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ ↑f.valueGroup = ↑f.valueGroup

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : Associated x y
⊢ Associated x y

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : Associated x y
⊢ Associated x y
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ Function.Surjective ⇑(restrict₀ f)

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ Function.Surjective ⇑(restrict₀ f)
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
u : Bˣ
hu✝ : u ∈ ↑f.valueGroup
hu : u ∈ ↑f.valueMonoid
⊢ ∃ a, (restrict₀ f) a = some ⟨u, hu✝⟩

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
u : Bˣ
hu✝ : u ∈ ↑f.valueGroup
hu : u ∈ ↑f.valueMonoid
⊢ ∃ a, (restrict₀ f) a = some ⟨u, hu✝⟩
Module: Mathlib.Algebra.GroupWithZero.Torsion

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y
Module: Mathlib.Algebra.GroupWithZero.Torsion

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x = y
hx : IsLeftRegular (x ^ n)
⊢ x = y

Tactic:
]

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x = y
hx : IsLeftRegular (x ^ n)
⊢ x = y
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯.unit
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ u⁻¹ * v ∈ f.valueGroup

Tactic:
]

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯.unit
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ u⁻¹ * v ∈ f.valueGroup
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
⊢ (∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑y = f x) ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f x ≠ 0 ∧ f a * ↑y = f x

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
⊢ (∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑y = f x) ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f x ≠ 0 ∧ f a * ↑y = f x