awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Basic (goal)
Goal:
M : Type u_1
inst : Mul M
s : Set M
p :
  (x y : M) →
    Membership.mem (γ := Subsemigroup M) (closure s) x → Membership.mem (γ := Subsemigroup M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hy : Membership.mem (γ := Subsemigroup M) (closure s) y
z : M
hz : z ∈ s
⊢ p z y ⋯ hy
have mem₁ : ∀ (x : M) (h : x ∈ s), p z x sorry sorry
Tactic: induction hy using closure_induction with
    | mem _ h => exact mem _ _ hz h
    | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Basic (goal)
Goal:
M : Type u_1
inst : Mul M
s : Set M
p :
  (x y : M) →
    Membership.mem (γ := Subsemigroup M) (closure s) x → Membership.mem (γ := Subsemigroup M) (closure s) y → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
    (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (hz : Membership.mem (γ := Subsemigroup M) (closure s) z),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hy : Membership.mem (γ := Subsemigroup M) (closure s) y
z : M
hz : z ∈ s
mem₁ : ∀ (x : M) (h : x ∈ s), p z x ⋯ ⋯
⊢ p z y ⋯ hy
have mem₂ : ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (closure s) x)
  (hy : Membership.mem (γ := Subsemigroup M) (closure s) y) (h₁ : p z x sorry hx) (h₂ : p z y sorry hy), p z (x * y) sorry sorry
Tactic: induction hy using closure_induction with
    | mem _ h => exact mem _ _ hz h
    | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Basic (hypothesis)
Goal:
M : Type u_1
inst : Mul M
p : M → Prop
s : Set M
closure : Eq (α := Subsemigroup M) (Subsemigroup.closure s) ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x
have x₁ : Membership.mem (γ := Subsemigroup M) (Subsemigroup.closure s) x
Tactic: induction closure.symm ▸ mem_top x using closure_induction with
  | mem _ h => exact mem _ h
  | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Basic (goal)
Goal:
M : Type u_1
inst : Mul M
m : M
p : Subsemigroup M
⊢ closure {m} ≤ p ↔ m ∈ p
have rw : {m} ⊆ (↑p : Set M) ↔ m ∈ p
Tactic: rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Basic (goal)
Goal:
M : Type u_1
inst : Mul M
m : M
p : Subsemigroup M
rw : {m} ⊆ (↑p : Set M) ↔ m ∈ p
⊢ closure {m} ≤ p ↔ m ∈ p
have rw₁ : m ∈ (↑p : Set M) ↔ m ∈ p
Tactic: rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Basic (goal)
Goal:
M : Type u_1
inst : Mul M
m : M
p : Subsemigroup M
rw : {m} ⊆ (↑p : Set M) ↔ m ∈ p
rw₁ : m ∈ (↑p : Set M) ↔ m ∈ p
⊢ closure {m} ≤ p ↔ m ∈ p
have rw₂ : m ∈ p ↔ m ∈ p
Tactic: rw [closure_le, singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Basic (goal)
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), p i) m ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
have rw : (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
Tactic: rw [← closure_singleton_le_iff_mem, le_iSup_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Basic (goal)
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
⊢ Eq.{u_1 + 1} (α := Subsemigroup M) (⨆ (i : ι), p i) (closure (⋃ (i : ι), (↑(p i) : Set M)))
have simp_rw : Eq.{u_1 + 1} (α := Subsemigroup M) (⨆ (i : ι), p i) (⨆ (i : ι), closure (↑(p i) : Set M))
Tactic: simp_rw [Subsemigroup.closure_iUnion, Subsemigroup.closure_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s : Set M
p q : Subsemigroup M
h : p.carrier = q.carrier
⊢ p = q
have mk : ∀ (carrier : Set M) (mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier)
  (h : { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M }.carrier = q.carrier),
  { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M } = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s : Set M
q : Subsemigroup M
carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
h : { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M }.carrier = q.carrier
⊢ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M } = q
have mk : ∀ (carrier_1 : Set M) (mul_mem'_1 : ∀ {a b : M}, a ∈ carrier_1 → b ∈ carrier_1 → a * b ∈ carrier_1)
  (h :
    { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M }.carrier =
      { carrier := carrier_1, mul_mem' := @mul_mem'_1 : Subsemigroup M }.carrier),
  { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup M } = { carrier := carrier_1, mul_mem' := @mul_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Subsingleton.{u_1 + 1} (Subsemigroup M)
⊢ Subsingleton M
have allEq : ∀ (a b : M), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Defs (hypothesis)
Goal:
M : Type u_1
inst : Mul M
inst_1 : Subsingleton.{u_1 + 1} (Subsemigroup M)
x y : M
⊢ x = y
have this : ∀ (a : M), Membership.mem (γ := Subsemigroup M) ⊥ a
Tactic: have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
s : Set M
S : Subsemigroup M
hn : Nonempty M
h : Eq.{u_1 + 1} (α := Subsemigroup M) ⊥ ⊤
⊢ False
have obtain : ∀ (x : M), False
Tactic: obtain ⟨x⟩ := id hn
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i
have refine : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
Tactic: refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
have suffices : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i
Tactic: suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i
have refine_1 : ∀ (hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x) (x : M)
  (h : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x), ∃ (i : ι), x ∈ S i
Tactic: refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x : M
refine_1 :
  ∀ (hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x) (x : M)
    (h : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x), ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x → ∃ (i : ι), x ∈ S i
have refine_2 : ∀ (hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x) (x y : M)
  (hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x)
  (hy : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y),
  (∃ (i : ι), x ∈ S i) → (∃ (i : ι), y ∈ S i) → ∃ (i : ι), x * y ∈ S i
Tactic: refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
M : Type u_2
inst : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
x_1 : M
hx : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x_1
x y : M
hx_1 : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x
hy : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) y
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ (i : ι), x * y ∈ S i
have refine_2 : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k), ∃ (i : ι), x * y ∈ S i
Tactic: obtain ⟨k, hik, hjk⟩ := hS i j
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
M : Type u_2
inst : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔ ∃ (i : ι), p i ∧ x ∈ S i
have rw : (∃ (i : Subtype p), x ∈ S (↑i : ι)) ↔ ∃ (i : ι), p i ∧ x ∈ S i
Tactic: rw [iSup_subtype', mem_iSup_of_directed]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
M : Type u_2
inst : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
rw : (∃ (i : Subtype p), x ∈ S (↑i : ι)) ↔ ∃ (i : ι), p i ∧ x ∈ S i
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔ ∃ (i : ι), p i ∧ x ∈ S i
have hS₁ : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) fun (x : Subtype p) ↦ S (↑x : ι)
Tactic: rw [iSup_subtype', mem_iSup_of_directed]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
M : Type u_2
inst : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) on S) {i : ι | p i}
x : M
⊢ Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) fun (x : Subtype p) ↦ S (↑x : ι)
have hS₁ : Directed (ι := Subtype p) (S ⁻¹'o fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) (Subtype.val (p := p))
Tactic: rw [← Function.comp_def, directed_comp]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
M : Type u_2
inst : Mul M
p : Prop
S : p → Subsemigroup M
x : M
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (h : p), S h) x ↔ ∃ (h : p), x ∈ S h
have pos : ∀ (h : p), Membership.mem (γ := Subsemigroup M) (⨆ (h : p), S h) x ↔ ∃ (h : p), x ∈ S h
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
M : Type u_2
inst : Mul M
p : Prop
S : p → Subsemigroup M
x : M
pos : ∀ (h : p), Membership.mem (γ := Subsemigroup M) (⨆ (h : p), S h) x ↔ ∃ (h : p), x ∈ S h
⊢ Membership.mem (γ := Subsemigroup M) (⨆ (h : p), S h) x ↔ ∃ (h : p), x ∈ S h
have neg : ∀ (h : ¬p), Membership.mem (γ := Subsemigroup M) (⨆ (h : p), S h) x ↔ ∃ (h : p), x ∈ S h
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥(S i)
dir : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u_2} ↥(⨆ (i : ι), S i)
have refine : ∀ (a : M),
  Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) a →
    ∀ (b : M), Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) b → a * b = b * a
Tactic: refine .of_setLike_mul_comm ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥(S i)
dir : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
⊢ ∀ (a : M),
    Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) a →
      ∀ (b : M), Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) b → a * b = b * a
have simp_rw : ∀ (a : M) (x : ι) (h : a ∈ S x) (b : M) (x : ι) (h : b ∈ S x), a * b = b * a
Tactic: simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥(S i)
dir : Directed (fun (x1 x2 : Subsemigroup M) ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
hb : b ∈ S j
⊢ a * b = b * a
have obtain : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k), a * b = b * a
Tactic: obtain ⟨k, hik, hjk⟩ := dir i j
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (hypothesis)
Goal:
M : Type u_2
inst : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
have this : S ≤ S ⊔ T
Tactic: have : S ≤ S ⊔ T := le_sup_left
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (hypothesis)
Goal:
M : Type u_2
inst : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
have this : T ≤ S ⊔ T
Tactic: have : T ≤ S ⊔ T := le_sup_right
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (hypothesis)
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
have this : S i ≤ iSup S
Tactic: have : S i ≤ iSup S := le_iSup _ _
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (hypothesis)
Goal:
M : Type u_2
inst : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
have this : s ≤ sSup S
Tactic: have : s ≤ sSup S := le_sSup hs
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (hypothesis)
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁
have hx₂ : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁
Tactic: rw [iSup_eq_closure] at hx₁
Cleared hypotheses: hx₁, mem, mul
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁
have refine : ∀ (x₂ : M) (hx₂ : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x₂), C x₂
Tactic: refine closure_induction (fun x₂ hx₂ => ?_) (fun x y _ _ ↦ mul x y) hx₁
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (closure (⋃ (i : ι), (↑(S i) : Set M))) x₁
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : Membership.mem (γ := Set M) (⋃ (i : ι), (↑(S i) : Set M)) x₂
⊢ C x₂
have obtain : ∀ (i : ι) (hi : x₂ ∈ (↑(S i) : Set M)), C x₂
Tactic: obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
⊢ C x₁ hx₁
have refine : ∃ (x : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁), C x₁ x
Tactic: refine Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
⊢ ∃ (x : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁), C x₁ x
have refine_1 : ∀ (i : ι) (x₂ : M) (hx₂ : x₂ ∈ S i),
  (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') x₂
Tactic: refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁
      (fun i x₂ hx₂ => ?_) fun x₃ y => ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Membership (goal)
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
refine_1 :
  ∀ (i : ι) (x₂ : M) (hx₂ : x₂ ∈ S i),
    (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') x₂
⊢ ∃ (x : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁), C x₁ x
have refine_2 : ∀ (x₃ y : M),
  (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') x₃ →
    (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') y →
      (fun (x' : M) ↦ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x'), C x' hx'') (x₃ * y)
Tactic: refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁
      (fun i x₂ hx₂ => ?_) fun x₃ y => ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.MulOpposite (goal)
Goal:
M : Type u_2
inst : Mul M
s : Set M
⊢ Eq (α := Subsemigroup Mᵐᵒᵖ) (Subsemigroup.op (closure s)) (closure (MulOpposite.unop ⁻¹' s))
have simp_rw : Eq.{u_2 + 1} (α := Subsemigroup Mᵐᵒᵖ) (sInf {a : Subsemigroup Mᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ)})
  (sInf {S : Subsemigroup Mᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Mᵐᵒᵖ)})
Tactic: simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Subsemigroup.coe_unop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.MulOpposite (goal)
Goal:
M : Type u_2
inst : Mul M
s : Set M
⊢ Eq.{u_2 + 1} (α := Subsemigroup Mᵐᵒᵖ) (sInf {a : Subsemigroup Mᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ)})
    (sInf {S : Subsemigroup Mᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Mᵐᵒᵖ)})
have e_a : ∀ (a : Subsemigroup Mᵐᵒᵖ), s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Mᵐᵒᵖ)
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.MulOpposite (goal)
Goal:
M : Type u_2
inst : Mul M
s : Set Mᵐᵒᵖ
⊢ Eq (α := Subsemigroup M) (Subsemigroup.unop (closure s)) (closure (MulOpposite.op ⁻¹' s))
have rw : Eq (α := Subsemigroup Mᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
Tactic: rw [← op_inj, op_unop, op_closure]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.MulOpposite (goal)
Goal:
M : Type u_2
inst : Mul M
s : Set Mᵐᵒᵖ
⊢ Eq (α := Subsemigroup Mᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
have simp_rw : Eq (α := Subsemigroup Mᵐᵒᵖ) (closure s) (closure ((fun (x : Mᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
Tactic: simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.MulOpposite (goal)
Goal:
M : Type u_2
inst : Mul M
s : Set Mᵐᵒᵖ
simp_rw :
  Eq (α := Subsemigroup Mᵐᵒᵖ) (closure s) (closure ((fun (x : Mᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
⊢ Eq (α := Subsemigroup Mᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
have simp_rw₁ : Eq (α := Subsemigroup Mᵐᵒᵖ) (closure s) (closure ((fun (x : Mᵐᵒᵖ) ↦ x) ⁻¹' s))
Tactic: simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
S_1 : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a b : M
ha : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) a
hb : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) b
⊢ Membership.mem (α := N) S ((f : (a : M) → N) (a * b) : N)
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ∈ S
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
S_1 : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ (↑S : Set M)
y : M
hy : y ∈ (↑S : Set M)
⊢ (f : (a : M) → N) (x * y) = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
ι : Sort u_5
inst_2 : Nonempty ι
f : M →ₙ* N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
s : ι → Subsemigroup M
⊢ map f (iInf s) = ⨅ (i : ι), map f (s i)
have a : (↑(map f (iInf s)) : Set N) = (↑(⨅ (i : ι), map f (s i)) : Set N)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : 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
have mp : u ≤ s.prod t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
mp : u ≤ s.prod t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
⊢ u ≤ s.prod t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
have mpr : map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ s.prod t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ s.prod t
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
have mp : map (fst M N) u ≤ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subsemigroup.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ s.prod t
mp : map (fst M N) u ≤ s
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
have mp₁ : map (snd M N) u ≤ t
Tactic: constructor