awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
x_1 : G
h : x_1 ∈ k
⊢ p x_1 z ⋯ ⋯

Tactic:
exact mem _ _ h hz
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
⊢ p 1 z ⋯ ⋯

Tactic:
one_left _ (subset_closure hz)

Premises used: Subgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
⊢ p 1 z ⋯ ⋯

Tactic:
exact one_left _ (subset_closure hz)

Premises used: Subgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
x_1 y_1 : G
hx : Membership.mem (γ := Subgroup G) (closure k) x_1
hy : Membership.mem (γ := Subgroup G) (closure k) y_1
h₁ : p x_1 z hx ⋯
h₂ : p y_1 z hy ⋯
⊢ p (x_1 * y_1) z ⋯ ⋯

Tactic:
mul_left _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
x_1 y_1 : G
hx : Membership.mem (γ := Subgroup G) (closure k) x_1
hy : Membership.mem (γ := Subgroup G) (closure k) y_1
h₁ : p x_1 z hx ⋯
h₂ : p y_1 z hy ⋯
⊢ p (x_1 * y_1) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
x_1 : G
hx : Membership.mem (γ := Subgroup G) (closure k) x_1
h : p x_1 z hx ⋯
⊢ p x_1⁻¹ z ⋯ ⋯

Tactic:
inv_left _ _ _ _ h
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
x_1 : G
hx : Membership.mem (γ := Subgroup G) (closure k) x_1
h : p x_1 z hx ⋯
⊢ p x_1⁻¹ z ⋯ ⋯

Tactic:
exact inv_left _ _ _ _ h
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : Membership.mem (γ := Subgroup G) (closure k) x
z : G
hz : z ∈ k
mem₁ : ∀ (x : G) (h : x ∈ k), p x z ⋯ ⋯
mem₂ : p 1 z ⋯ ⋯
mem₃ :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (h₁ : p x z hx ⋯) (h₂ : p y z hy ⋯), p (x * y) z ⋯ ⋯
mem₄ : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x) (h : p x z hx ⋯), p x⁻¹ z ⋯ ⋯
⊢ p x z hx ⋯

Tactic:
induction hx using closure_induction with
    | mem _ h => exact mem _ _ h hz
    | one => exact one_left _ (subset_closure hz)
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | inv _ _ h => exact inv_left _ _ _ _ h

Premises used: Subgroup.mul, Subgroup.one, Subgroup.subset_closure, Subgroup.inv
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : Membership.mem (γ := Subgroup G) (closure k) x
⊢ p x 1 hx ⋯

Tactic:
one_right x hx
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : Membership.mem (γ := Subgroup G) (closure k) x
⊢ p x 1 hx ⋯

Tactic:
exact one_right x hx
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : Membership.mem (γ := Subgroup G) (closure k) x
x_1 y_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (closure k) x_1
hy : Membership.mem (γ := Subgroup G) (closure k) y_1
h₁ : p x x_1 hx hx_1
h₂ : p x y_1 hx hy
⊢ p x (x_1 * y_1) hx ⋯

Tactic:
mul_right _ _ _ _ _ hx h₁ h₂
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : Membership.mem (γ := Subgroup G) (closure k) x
x_1 y_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (closure k) x_1
hy : Membership.mem (γ := Subgroup G) (closure k) y_1
h₁ : p x x_1 hx hx_1
h₂ : p x y_1 hx hy
⊢ p x (x_1 * y_1) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ hx h₁ h₂
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : Membership.mem (γ := Subgroup G) (closure k) x
x_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (closure k) x_1
h : p x x_1 hx hx_1
⊢ p x x_1⁻¹ hx ⋯

Tactic:
inv_right _ _ _ _ h
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : Membership.mem (γ := Subgroup G) (closure k) x
x_1 : G
hx_1 : Membership.mem (γ := Subgroup G) (closure k) x_1
h : p x x_1 hx hx_1
⊢ p x x_1⁻¹ hx ⋯

Tactic:
exact inv_right _ _ _ _ h
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
p : (x y : G) → Membership.mem (γ := Subgroup G) (closure k) x → Membership.mem (γ := Subgroup G) (closure k) y → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (hz : Membership.mem (γ := Subgroup G) (closure k) z),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : Membership.mem (γ := Subgroup G) (closure k) y)
    (hz : Membership.mem (γ := Subgroup G) (closure k) z) (hx : Membership.mem (γ := Subgroup G) (closure k) x),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure k) x)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : Membership.mem (γ := Subgroup G) (closure k) x
hy : Membership.mem (γ := Subgroup G) (closure k) y
mem₁ : ∀ (z : G) (hz : z ∈ k), p x z hx ⋯
one : p x 1 hx ⋯
mul :
  ∀ (x_1 y : G) (hx_1 : Membership.mem (γ := Subgroup G) (closure k) x_1)
    (hy : Membership.mem (γ := Subgroup G) (closure k) y) (h₁ : p x x_1 hx hx_1) (h₂ : p x y hx hy), p x (x_1 * y) hx ⋯
inv : ∀ (x_1 : G) (hx_1 : Membership.mem (γ := Subgroup G) (closure k) x_1) (h : p x x_1 hx hx_1), p x x_1⁻¹ hx ⋯
⊢ p x y hx hy

Tactic:
induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem _ _ h hz
    | one => exact one_left _ (subset_closure hz)
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | inv _ _ h => exact inv_left _ _ _ _ h
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂
  | inv _ _ h => exact inv_right _ _ _ _ h

Premises used: Subgroup.mul, Subgroup.one, Subgroup.inv
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
k : Set G
⊢ Eq (α := Subgroup ↥(closure k))
    (closure (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (closure k) x) ⁻¹' k)) ⊤

Tactic:
eq_top_iff.2 fun x _ ↦ Subtype.recOn x fun _ hx' ↦
    closure_induction (fun _ h ↦ subset_closure h) (one_mem _) (fun _ _ _ _ ↦ mul_mem)
      (fun _ _ ↦ inv_mem) hx'

Premises used: Iff.mpr, eq_top_iff, Subtype.recOn
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
h k : Set G
h' : h ⊆ k
⊢ LE.le (α := Subgroup G) (closure h) (closure k)

Tactic:
(Subgroup.gi G).gc.monotone_l h'

Premises used: Subgroup.gi, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
⊢ closure (↑K : Set G) = K

Tactic:
(Subgroup.gi G).l_u_eq K

Premises used: Subgroup.gi, GaloisInsertion.l_u_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
⊢ Eq.{u_1 + 1} (α := Subgroup G) (closure ∅) ⊥

Tactic:
(Subgroup.gi G).gc.l_bot

Premises used: Subgroup.gi, GaloisConnection.l_bot, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
⊢ Eq.{u_1 + 1} (α := Subgroup G) (closure univ) ⊤

Tactic:
@coe_top G _ ▸ closure_eq ⊤

Premises used: Subgroup.closure_eq, Eq.rec, Subgroup.coe_top, Top.top