mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case refine_1
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
i : ι
x₂ : M
hx₂ : x₂ ∈ S i
⊢ ∃ (hx'' : x₂ ∈ ⨆ i, S i), C x₂ hx''

pp: case refine_2
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
x₃ y : M
⊢ (∃ (hx'' : x₃ ∈ ⨆ i, S i), C x₃ hx'') →
    (∃ (hx'' : y ∈ ⨆ i, S i), C y hx'') → ∃ (hx'' : x₃ * y ∈ ⨆ i, S i), C (x₃ * y) hx''

Tactic:
·

Goal state after:
case refine_1
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
i : ι
x₂ : M
hx₂ : x₂ ∈ S i
⊢ ∃ (hx'' : x₂ ∈ ⨆ i, S i), C x₂ hx''
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case refine_2
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
x₃ y : M
⊢ (∃ (hx'' : x₃ ∈ ⨆ i, S i), C x₃ hx'') →
    (∃ (hx'' : y ∈ ⨆ i, S i), C y hx'') → ∃ (hx'' : x₃ * y ∈ ⨆ i, S i), C (x₃ * y) hx''

Tactic:
·

Goal state after:
case refine_2
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
x₃ y : M
⊢ (∃ (hx'' : x₃ ∈ ⨆ i, S i), C x₃ hx'') →
    (∃ (hx'' : y ∈ ⨆ i, S i), C y hx'') → ∃ (hx'' : x₃ * y ∈ ⨆ i, S i), C (x₃ * y) hx''
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: case inl
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False

pp: case inr
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False

Tactic:
·

Goal state after:
case inl
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: case inr
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False

Tactic:
·

Goal state after:
case inr
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ u ≤ s.prod t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

pp: case mpr
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ s.prod t

Tactic:
·

Goal state after:
case mp
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ u ≤ s.prod t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mp.left
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ s.prod t
⊢ map (fst M N) u ≤ s

pp: case mp.right
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ s.prod t
⊢ map (snd M N) u ≤ t

Tactic:
·

Goal state after:
case mp.left
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ s.prod t
⊢ map (fst M N) u ≤ s
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mp.right
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ s.prod t
⊢ map (snd M N) u ≤ t

Tactic:
·

Goal state after:
case mp.right
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ s.prod t
⊢ map (snd M N) u ≤ t
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mpr
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ s.prod t

Tactic:
·

Goal state after:
case mpr
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ s.prod t
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

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

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

Tactic:
·

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

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

Tactic:
·

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

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

Tactic:
intro a i ha b j hb

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ ↑M ⊆ ↑M.subsemiringClosure.toNonUnitalSubsemiring

pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ ↑M ⊆ ↑M.subsemiringClosure.toNonUnitalSubsemiring
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
·

Goal state after:
case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

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

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

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s

Tactic:
by
  ext x
  refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
  rintro - ⟨H, rfl⟩
  rintro - ⟨J, rfl⟩
  refine (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => ?_
  refine (Submonoid.mem_closure.mp hy) H.toSubmonoid fun z hz => ?_
  exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ x ∈ closure s → ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

pp: case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) → x ∈ closure s

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ x ∈ closure s → ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mp.mem.one
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = 1

Tactic:
exact ⟨[], List.forall_mem_nil _, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: case mp
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ Submonoid.map f (algebraMapSubmonoid A M) → x ∈ algebraMapSubmonoid B M

pp: case mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ algebraMapSubmonoid B M → x ∈ Submonoid.map f (algebraMapSubmonoid A M)

Tactic:
·

Goal state after:
case mp
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ Submonoid.map f (algebraMapSubmonoid A M) → x ∈ algebraMapSubmonoid B M
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: case mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ algebraMapSubmonoid B M → x ∈ Submonoid.map f (algebraMapSubmonoid A M)

Tactic:
·

Goal state after:
case mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ algebraMapSubmonoid B M → x ∈ Submonoid.map f (algebraMapSubmonoid A M)
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mp.zero
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = 0

Tactic:
exact ⟨[], List.forall_mem_nil _, rfl⟩

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) → x ∈ closure s

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) → x ∈ closure s
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
s : Set R
x : R
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = 0

Tactic:
exact ⟨[], List.forall_mem_nil _, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Prime.Defs

Goal state before:
pp: case succ.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a

pp: case succ.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a

Tactic:
·

Goal state after:
case succ.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a
Module: Mathlib.Algebra.Prime.Defs

Goal state before:
pp: case succ.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a

Tactic:
·

Goal state after:
case succ.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B

pp: case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : ↑u * y = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
·

Goal state after:
case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : ↑u * y = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
·

Goal state after:
case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : ↑u * y = A * B
⊢ IsUnit A ∨ IsUnit B
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B

pp: case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
·

Goal state after:
case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
·

Goal state after:
case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ IsUnit A ∨ IsUnit B
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mp
M : Type u_2
inst✝ : Monoid M
x y : M
⊢ Irreducible (x * y) → Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x

pp: case mpr
M : Type u_2
inst✝ : Monoid M
x y : M
⊢ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x → Irreducible (x * y)

Tactic:
·

Goal state after:
case mp
M : Type u_2
inst✝ : Monoid M
x y : M
⊢ Irreducible (x * y) → Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mp.refine_1
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit y
⊢ Irreducible x

pp: case mp.refine_2
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit x
⊢ Irreducible y

Tactic:
·

Goal state after:
case mp.refine_1
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit y
⊢ Irreducible x
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mp.refine_2
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit x
⊢ Irreducible y

Tactic:
·

Goal state after:
case mp.refine_2
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit x
⊢ Irreducible y
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inl
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = L.prod
⊢ C hd.prod

pp: case cons.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = -L.prod
⊢ C hd.prod

pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)

Tactic:
·

Goal state after:
case cons.inl
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = L.prod
⊢ C hd.prod
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inl
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = L.prod
⊢ C hd.prod

Tactic:
HP

Goal state after:
case cons.inl
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = L.prod
⊢ C L.prod
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: 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

Tactic:
·

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
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: 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

Tactic:
·

Goal state after:
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.Group.Irreducible.Lemmas

Goal state before:
pp: case mpr
M : Type u_2
inst✝ : Monoid M
x y : M
⊢ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x → Irreducible (x * y)

Tactic:
·

Goal state after:
case mpr
M : Type u_2
inst✝ : Monoid M
x y : M
⊢ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x → Irreducible (x * y)
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mpr.inl
M : Type u_2
inst✝ : Monoid M
x y : M
ha : Irreducible x
hb : IsUnit y
⊢ Irreducible (x * y)

pp: case mpr.inr
M : Type u_2
inst✝ : Monoid M
x y : M
hb : Irreducible y
ha : IsUnit x
⊢ Irreducible (x * y)

Tactic:
·

Goal state after:
case mpr.inl
M : Type u_2
inst✝ : Monoid M
x y : M
ha : Irreducible x
hb : IsUnit y
⊢ Irreducible (x * y)
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b c : M
hc : p * b = a * c
h : p ∣ a
⊢ p ∣ a ∨ a ∣ b

pp: case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b

Tactic:
·

Goal state after:
case inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b c : M
hc : p * b = a * c
h : p ∣ a
⊢ p ∣ a ∨ a ∣ b
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b

Tactic:
·

Goal state after:
case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b x : M
hc : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mpr.inr
M : Type u_2
inst✝ : Monoid M
x y : M
hb : Irreducible y
ha : IsUnit x
⊢ Irreducible (x * y)

Tactic:
·

Goal state after:
case mpr.inr
M : Type u_2
inst✝ : Monoid M
x y : M
hb : Irreducible y
ha : IsUnit x
⊢ Irreducible (x * y)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = -L.prod
⊢ C hd.prod

pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)

Tactic:
·

Goal state after:
case cons.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = -L.prod
⊢ C hd.prod