mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: case e'_3.e'_3
M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
x✝ : M
⊢ x✝ ∈ ⋂ s ∈ f, ↑s ↔ x✝ ∈ (sInf (toSubmonoid '' f)).1.carrier

Tactic:
;

Goal state after:
case e'_3.e'_3
M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
x✝ : M
⊢ x✝ ∈ ⋂ s ∈ f, ↑s ↔ x✝ ∈ (sInf (toSubmonoid '' f)).1.carrier
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 : M
⊢ x ∈ s.saturation ↔ ∃ m ∈ s, x ∣ m

Tactic:
simp_rw [dvd_def, existsAndEq, and_true, mem_saturation_iff]

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

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

Tactic:
by
  rw [IsConj, Units.exists_iff_ne_zero (p := (SemiconjBy · a b))]
  congr! 2 with c
  exact and_congr_right (mul_inv_eq_iff_eq_mul₀ · |>.symm)

Goal state after:
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
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
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
k : ι
hk₀ : 1 < f (v k)
hk₁ : f (v k) < f (v i)
hk₂ : v k ∉ closure (v '' t)
⊢ False

Tactic:
;

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
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
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
k : ι
hk₀ : 1 < f (v k)
hk₁ : f (v k) < f (v i)
hk₂ : v k ∉ closure (v '' t)
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ 0⁻¹ ↔ a✝ ∈ 0

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ 0⁻¹ ↔ a✝ ∈ 0
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
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
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₁ : i ∈ t
⊢ v i ∈ closure (v '' t)

Tactic:
;

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
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
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₁ : i ∈ t
⊢ v i ∈ closure (v '' t)
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
i : ι
⊢ i ∈ univ ↔ i ∈ {i | 1 < f (v i)} ∪ {i | f (v i) < 1}

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
i : ι
⊢ i ∈ univ ↔ i ∈ {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
a : α
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • Set.univ = Set.univ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
a : α
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • Set.univ = Set.univ
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.Nontrivial
⊢ ↑s • Set.univ = Set.univ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nontrivial
⊢ ↑s • Set.univ = Set.univ
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a✝ : α
⊢ a✝ ∈ (a •> s)⁻¹ ↔ a✝ ∈ s⁻¹ <• a⁻¹

Tactic:
;

Goal state after:
case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a✝ : α
⊢ a✝ ∈ (a •> s)⁻¹ ↔ a✝ ∈ s⁻¹ <• a⁻¹
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a✝ : α
⊢ a✝ ∈ (s <• a)⁻¹ ↔ a✝ ∈ a⁻¹ •> s⁻¹

Tactic:
;

Goal state after:
case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a✝ : α
⊢ a✝ ∈ (s <• a)⁻¹ ↔ a✝ ∈ a⁻¹ •> s⁻¹
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Finset α
t : Finset β
⊢ s • image (fun x ↦ -x) t = image (fun x ↦ -x) (s • t)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Finset α
t : Finset β
⊢ s • image (fun x ↦ -x) t = image (fun x ↦ -x) (s • t)
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
s : Set ι
hst : s ⊆ {j | IsMulIndecomposable v {i | 1 < f (v i)} j}
i : ι
hf : v i = 1
⊢ ∃ i, f (v i) = 1

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
s : Set ι
hst : s ⊆ {j | IsMulIndecomposable v {i | 1 < f (v i)} j}
i : ι
hf : v i = 1
⊢ ∃ i, f (v i) = 1
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inl
ι : 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
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
y : M
x✝¹ : y ∈ closure (v '' {i | 1 < f (v i)})
hy : y = 1 ∨ 1 < f y
x✝ : 1 ∈ closure (v '' {i | 1 < f (v i)})
⊢ 1 * y = 1 ∨ 1 < f (1 * y)

pp: case inr
ι : 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
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x y : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
x✝ : y ∈ closure (v '' {i | 1 < f (v i)})
hy : y = 1 ∨ 1 < f y
hx : 1 < f x
⊢ x * y = 1 ∨ 1 < f (x * y)

Tactic:
;

Goal state after:
case inl
ι : 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
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
y : M
x✝¹ : y ∈ closure (v '' {i | 1 < f (v i)})
hy : y = 1 ∨ 1 < f y
x✝ : 1 ∈ closure (v '' {i | 1 < f (v i)})
⊢ 1 * y = 1 ∨ 1 < f (1 * y)

case inr
ι : 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
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x y : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
x✝ : y ∈ closure (v '' {i | 1 < f (v i)})
hy : y = 1 ∨ 1 < f y
hx : 1 < f x
⊢ x * y = 1 ∨ 1 < f (x * y)
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inr.inl
ι : 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
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
hx : 1 < f x
x✝ : 1 ∈ closure (v '' {i | 1 < f (v i)})
⊢ x * 1 = 1 ∨ 1 < f (x * 1)

pp: case inr.inr
ι : 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
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x y : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
x✝ : y ∈ closure (v '' {i | 1 < f (v i)})
hx : 1 < f x
hy : 1 < f y
⊢ x * y = 1 ∨ 1 < f (x * y)

Tactic:
;

Goal state after:
case inr.inl
ι : 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
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
hx : 1 < f x
x✝ : 1 ∈ closure (v '' {i | 1 < f (v i)})
⊢ x * 1 = 1 ∨ 1 < f (x * 1)

case inr.inr
ι : 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
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x y : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
x✝ : y ∈ closure (v '' {i | 1 < f (v i)})
hx : 1 < f x
hy : 1 < f y
⊢ x * y = 1 ∨ 1 < f (x * y)
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inr.inl
ι : 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
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
hx : 1 < f x
x✝ : 1 ∈ closure (v '' {i | 1 < f (v i)})
⊢ 1 < f (x * 1)

Tactic:
;

Goal state after:
case inr.inl
ι : 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
hi : v i ∈ closure (v '' {i | 1 < f (v i)})
x : M
x✝¹ : x ∈ closure (v '' {i | 1 < f (v i)})
hx : 1 < f x
x✝ : 1 ∈ closure (v '' {i | 1 < f (v i)})
⊢ 1 < f (x * 1)
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inr.inl
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : v i ∈ closure (v '' s)
⊢ f (v i) ≠ 1

pp: case inr.inr
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : (v i)⁻¹ ∈ closure (v '' s)
⊢ f (v i) ≠ 1

Tactic:
;

Goal state after:
case inr.inl
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : v i ∈ closure (v '' s)
⊢ f (v i) ≠ 1

case inr.inr
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : (v i)⁻¹ ∈ closure (v '' s)
⊢ f (v i) ≠ 1
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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : (v i)⁻¹ ∈ closure (v '' s)
⊢ v i⁻¹ ∈ closure (v '' s)

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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : (v i)⁻¹ ∈ closure (v '' s)
⊢ v i⁻¹ ∈ closure (v '' s)
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inl
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
y : G
x✝² : y ∈ closure (v '' s)
hy : y ≠ 1 → 1 < f y
x✝¹ : 1 ∈ closure (v '' s)
hx : 1 ≠ 1 → 1 < f 1
x✝ : 1 * y ≠ 1
⊢ 1 < f (1 * y)

pp: case inr
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
x y : G
x✝² : x ∈ closure (v '' s)
x✝¹ : y ∈ closure (v '' s)
hx : x ≠ 1 → 1 < f x
hy : y ≠ 1 → 1 < f y
x✝ : x * y ≠ 1
hx' : x ≠ 1
⊢ 1 < f (x * y)

Tactic:
;

Goal state after:
case inl
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
y : G
x✝² : y ∈ closure (v '' s)
hy : y ≠ 1 → 1 < f y
x✝¹ : 1 ∈ closure (v '' s)
hx : 1 ≠ 1 → 1 < f 1
x✝ : 1 * y ≠ 1
⊢ 1 < f (1 * y)

case inr
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
x y : G
x✝² : x ∈ closure (v '' s)
x✝¹ : y ∈ closure (v '' s)
hx : x ≠ 1 → 1 < f x
hy : y ≠ 1 → 1 < f y
x✝ : x * y ≠ 1
hx' : x ≠ 1
⊢ 1 < f (x * y)
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inr.inl
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
x : G
x✝² : x ∈ closure (v '' s)
hx : x ≠ 1 → 1 < f x
hx' : x ≠ 1
x✝¹ : 1 ∈ closure (v '' s)
hy : 1 ≠ 1 → 1 < f 1
x✝ : x * 1 ≠ 1
⊢ 1 < f (x * 1)

pp: case inr.inr
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
x y : G
x✝² : x ∈ closure (v '' s)
x✝¹ : y ∈ closure (v '' s)
hx : x ≠ 1 → 1 < f x
hy : y ≠ 1 → 1 < f y
x✝ : x * y ≠ 1
hx' : x ≠ 1
hy' : y ≠ 1
⊢ 1 < f (x * y)

Tactic:
;

Goal state after:
case inr.inl
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
x : G
x✝² : x ∈ closure (v '' s)
hx : x ≠ 1 → 1 < f x
hx' : x ≠ 1
x✝¹ : 1 ∈ closure (v '' s)
hy : 1 ≠ 1 → 1 < f 1
x✝ : x * 1 ≠ 1
⊢ 1 < f (x * 1)

case inr.inr
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : 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
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
x y : G
x✝² : x ∈ closure (v '' s)
x✝¹ : y ∈ closure (v '' s)
hx : x ≠ 1 → 1 < f x
hy : y ≠ 1 → 1 < f y
x✝ : x * y ≠ 1
hx' : x ≠ 1
hy' : y ≠ 1
⊢ 1 < f (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
⊢ ↑f.valueMonoid = ↑f.valueGroup

Tactic:
valueMonoid_eq_valueGroup,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ ↑f.valueGroup.toSubmonoid = ↑f.valueGroup
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case mpr
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
⊢ (∃ y, f y = x) ∧ ¬x = 0 → ∃ x_1, (∃ y, f y = ↑x_1) ∧ ↑x_1 = x

Tactic:
rintro ⟨⟨y, hy⟩, hx₀⟩
    refine ⟨Units.mk0 x hx₀, ?_, rfl⟩
    simpa [Units.val_mk0, mem_range] using ⟨y, hy⟩

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

Goal state before:
pp: case h
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
⊢ (restrict₀ f) 0 = 0

Tactic:
;

Goal state after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : f.ValueGroup₀
⊢ (restrict₀ f) 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
hy : y ∈ f.valueGroup
⊢ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑y = f x

Tactic:
simp only [valueGroup, valueMonoid] at hy

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
hy : y ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑y = f x
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case a
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ˣ := ⋯
hv₀ : f x = ↑v
u : Bˣ := ⋯
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ v ∈ f.valueGroup

Tactic:
· apply mem_valueGroup
      use x

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

Goal state before:
pp: case none
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
⊢ none = 0

Tactic:
;

Goal state after:
case none
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
⊢ none = 0
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
⊢ ⊤.Factors (⊤.arrow ≫ f.app (op ⦋0⦌))

Tactic:
apply top_factors

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
i : Fin (m.len + 1)
⊢ n.const m i = n.const m ((Hom.toOrderHom (⦋0⦌.const m i)) 0)

Tactic:
;

Goal state after:
n m : SimplexCategory
i : Fin (m.len + 1)
⊢ n.const m i = n.const m ((Hom.toOrderHom (⦋0⦌.const m i)) 0)