awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a b : α
rw : b ∈ f.support ↔ b = x ∨ b = y
rw₁ : Membership.mem (γ := Finset α) {x, y} b ↔ b = x ∨ b = y
⊢ (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
have rw₂ : b = x ∨ Membership.mem (γ := Finset α) {y} b ↔ b = x ∨ b = y
Tactic: rw [← mem_support, ← hins, mem_insert, mem_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a b : α
rw : b ∈ f.support ↔ b = x ∨ b = y
rw₁ : Membership.mem (γ := Finset α) {x, y} b ↔ b = x ∨ b = y
rw₂ : b = x ∨ Membership.mem (γ := Finset α) {y} b ↔ b = x ∨ b = y
⊢ (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
have rw₃ : b = x ∨ b = y ↔ b = x ∨ b = y
Tactic: rw [← mem_support, ← hins, mem_insert, mem_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a : α
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
have key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
Tactic: have key : ∀ b, f b ≠ b ↔ _ := fun b => by rw [← mem_support, ← hins, mem_insert, mem_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
have pos : ∀ (ha : (f : (a : α) → α) a = a), Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
Tactic: by_cases ha : f a = a
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
pos : ∀ (ha : (f : (a : α) → α) a = a), Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
have neg : ∀ (ha : ¬(f : (a : α) → α) a = a), Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
Tactic: by_cases ha : f a = a
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
ha : (f : (a : α) → α) a = a
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
have ha' : ¬a = x ∧ ¬a = y
Tactic: have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
ha : (f : (a : α) → α) a = a
ha' : ¬a = x ∧ ¬a = y
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
have pos : a = (swap x y : (a : α) → α) a
Tactic: rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
ha : (f : (a : α) → α) a = a
ha' : ¬a = x ∧ ¬a = y
pos : a = (swap x y : (a : α) → α) a
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
have pos₁ : a = a
Tactic: rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
ha : ¬(f : (a : α) → α) a = a
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
have ha' : (f : (a : α) → α) a = x ∨ (f : (a : α) → α) a = y
Tactic: have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
ha : ¬(f : (a : α) → α) a = a
ha' : (f : (a : α) → α) a = x ∨ (f : (a : α) → α) a = y
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
have neg : ∀ (hmem : ¬a = y) (hins : {a, y} = f.support) (key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = a ∨ b = y)
  (ha' : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = y),
  Eq (α := α) ((f : (a : α) → α) a : α) ((swap a y : (a : α) → α) a : α)
Tactic: obtain rfl | rfl := (key a).mp ha
Cleared hypotheses: x, hmem, hins, key, ha'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : card (α := α) {y} = 1
a : α
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = y
ha : ¬(f : (a : α) → α) a = a
ha' : (f : (a : α) → α) a = x ∨ (f : (a : α) → α) a = y
neg :
  ∀ (hmem : ¬a = y) (hins : {a, y} = f.support) (key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = a ∨ b = y)
    (ha' : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = y),
    Eq (α := α) ((f : (a : α) → α) a : α) ((swap a y : (a : α) → α) a : α)
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x y : (a : α) → α) a : α)
have neg₁ : ∀ (hmem : ¬x = a) (hins : {x, a} = f.support) (ht : card (α := α) {a} = 1)
  (key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = a) (ha' : (f : (a : α) → α) a = x ∨ (f : (a : α) → α) a = a),
  Eq (α := α) ((f : (a : α) → α) a : α) ((swap x a : (a : α) → α) a : α)
Tactic: obtain rfl | rfl := (key a).mp ha
Cleared hypotheses: y, hmem, hins, ht, key, ha'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
y : α
ht : card (α := α) {y} = 1
a : α
ha : ¬(f : (a : α) → α) a = a
hmem : ¬a = y
hins : {a, y} = f.support
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = a ∨ b = y
ha' : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = y
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap a y : (a : α) → α) a : α)
have neg : y = (swap a y : (a : α) → α) a
Tactic: rw [Or.resolve_left ha' ha, swap_apply_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
y : α
ht : card (α := α) {y} = 1
a : α
ha : ¬(f : (a : α) → α) a = a
hmem : ¬a = y
hins : {a, y} = f.support
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = a ∨ b = y
ha' : (f : (a : α) → α) a = a ∨ (f : (a : α) → α) a = y
neg : y = (swap a y : (a : α) → α) a
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap a y : (a : α) → α) a : α)
have neg₁ : y = y
Tactic: rw [Or.resolve_left ha' ha, swap_apply_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x a : α
ha : ¬(f : (a : α) → α) a = a
hmem : ¬x = a
hins : {x, a} = f.support
ht : card (α := α) {a} = 1
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = a
ha' : (f : (a : α) → α) a = x ∨ (f : (a : α) → α) a = a
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x a : (a : α) → α) a : α)
have neg : x = (swap x a : (a : α) → α) a
Tactic: rw [Or.resolve_right ha' ha, swap_apply_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : #f.support = 2
x a : α
ha : ¬(f : (a : α) → α) a = a
hmem : ¬x = a
hins : {x, a} = f.support
ht : card (α := α) {a} = 1
key : ∀ (b : α), (f : (a : α) → α) b ≠ b ↔ b = x ∨ b = a
ha' : (f : (a : α) → α) a = x ∨ (f : (a : α) → α) a = a
neg : x = (swap x a : (a : α) → α) a
⊢ Eq (α := α) ((f : (a : α) → α) a : α) ((swap x a : (a : α) → α) a : α)
have neg₁ : x = x
Tactic: rw [Or.resolve_right ha' ha, swap_apply_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.IsSwap
⊢ #f.support = 2
have mpr : ∀ (x y : α) (hxy : x ≠ y), #(swap x y).support = 2
Tactic: obtain ⟨x, y, hxy, rfl⟩ := h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #f.support + #g.support
have rw : #(f * g).support = #(f.support ∪ g.support)
Tactic: rw [← Finset.card_union_of_disjoint]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
rw : #(f * g).support = #(f.support ∪ g.support)
⊢ #(f * g).support = #f.support + #g.support
have rw₁ : _root_.Disjoint f.support g.support
Tactic: rw [← Finset.card_union_of_disjoint]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #(f.support ∪ g.support)
have e_s : (f * g).support = f.support ∪ g.support
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).support = f.support ∪ g.support
have e_s : ∀ (a : α), a ∈ (f * g).support ↔ a ∈ f.support ∪ g.support
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
a : Perm α
t : List (Perm α)
ih : ∀ (h : List.Pairwise Disjoint t), #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
⊢ #(a :: t).prod.support = (List.map (card ∘ support) (a :: t)).sum
have ha : ∀ a' ∈ t, a.Disjoint a'
Tactic: obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
a : Perm α
t : List (Perm α)
ih : ∀ (h : List.Pairwise Disjoint t), #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
ha : ∀ a' ∈ t, a.Disjoint a'
⊢ #(a :: t).prod.support = (List.map (card ∘ support) (a :: t)).sum
have ht : List.Pairwise Disjoint t
Tactic: obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
a : Perm α
t : List (Perm α)
ih : ∀ (h : List.Pairwise Disjoint t), #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
ha : ∀ a' ∈ t, a.Disjoint a'
ht : List.Pairwise Disjoint t
⊢ #(a :: t).prod.support = (List.map (card ∘ support) (a :: t)).sum
have cons : #(a * t.prod).support = (card ∘ support) a + #t.prod.support
Tactic: rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ #l.prod.support = (List.map (card ∘ support) l).sum
have nil : ∀ (h : List.Pairwise.{u_1} (α := Perm α) Disjoint []),
  card.{u_1} (α := α) (support (List.prod [])) = (List.map.{u_1, 0} (α := Perm α) (card ∘ support) []).sum
Tactic: induction l with
  | nil => exact card_support_eq_zero.mpr rfl
  | cons a t ih =>
    obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
    rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]
    exact (disjoint_prod_right _ ha).card_support_mul
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
nil :
  ∀ (h : List.Pairwise.{u_1} (α := Perm α) Disjoint []),
    card.{u_1} (α := α) (support (List.prod [])) = (List.map.{u_1, 0} (α := Perm α) (card ∘ support) []).sum
⊢ #l.prod.support = (List.map (card ∘ support) l).sum
have cons : ∀ (a : Perm α) (t : List (Perm α))
  (ih : ∀ (h : List.Pairwise Disjoint t), #t.prod.support = (List.map (card ∘ support) t).sum)
  (h : List.Pairwise Disjoint (a :: t)), #(a :: t).prod.support = (List.map (card ∘ support) (a :: t)).sum
Tactic: induction l with
  | nil => exact card_support_eq_zero.mpr rfl
  | cons a t ih =>
    obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
    rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]
    exact (disjoint_prod_right _ ha).card_support_mul
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), Membership.mem (α := α) s ((f : (a : α) → α) x : α) ↔ x ∈ s
⊢ (f.subtypePerm (p := Membership.mem s) h).support = {x : ↥s | (f : (a : α) → α) (↑x : α) ≠ (↑x : α)}
have h₁ : ∀ (a : ↥s),
  a ∈ (f.subtypePerm (p := Membership.mem s) h).support ↔
    Membership.mem (γ := Finset ↥s) {x : ↥s | (f : (a : α) → α) (↑x : α) ≠ (↑x : α)} a
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ card.{u_1} (α := α) {x : α | (σ : (a : α) → α) x = x} < Fintype.card α - 1
have rw : 1 < card.{u_1} (α := α) {x : α | ¬(σ : (a : α) → α) x = x}
Tactic: rw [Nat.lt_sub_iff_add_lt, ← Nat.lt_sub_iff_add_lt', ← Finset.card_compl, Finset.compl_filter]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
⊢ (σ * τ * σ⁻¹).support = map (Equiv.toEmbedding σ) τ.support
have h : ∀ (a : α), a ∈ (σ * τ * σ⁻¹).support ↔ a ∈ map (Equiv.toEmbedding σ) τ.support
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (hypothesis)
Goal:
α : Type u_1
rels : Set (FreeGroup α)
⊢ Eq.{u_1 + 1} (α := Subgroup (PresentedGroup rels)) (Subgroup.closure (Set.range (of (rels := rels)))) ⊤
have this : Eq (α := (x : α) → PresentedGroup rels) (of (rels := rels))
  ((⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) :
      (a : FreeGroup α) → FreeGroup α ⧸ Subgroup.normalClosure rels) ∘
    FreeGroup.of)
Tactic: have : (PresentedGroup.of : α → PresentedGroup rels) = QuotientGroup.mk' _ ∘ FreeGroup.of := rfl
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
rels : Set (FreeGroup α)
this :
  Eq (α := (x : α) → PresentedGroup rels) (of (rels := rels))
    ((⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) :
        (a : FreeGroup α) → FreeGroup α ⧸ Subgroup.normalClosure rels) ∘
      FreeGroup.of)
⊢ Eq.{u_1 + 1} (α := Subgroup (PresentedGroup rels)) (Subgroup.closure (Set.range (of (rels := rels)))) ⊤
have rw : Eq (α := Subgroup (PresentedGroup rels)) (MonoidHom.range (QuotientGroup.mk' (Subgroup.normalClosure rels))) ⊤
Tactic: rw [this, Set.range_comp, ← MonoidHom.map_closure (QuotientGroup.mk' _),
    FreeGroup.closure_range_of, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
⊢ x ∈ H
have mk : ∀ (z : FreeGroup α),
  Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) z ∈ H
Tactic: obtain ⟨z⟩ := x
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
z : FreeGroup α
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) z ∈ H
have mk : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) 1 ∈ H
Tactic: induction z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
z : FreeGroup α
mk : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) 1 ∈ H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) z ∈ H
have mk₁ : ∀ (x : α),
  Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) (FreeGroup.of x) ∈
    H
Tactic: induction z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
z : FreeGroup α
mk : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) 1 ∈ H
mk₁ :
  ∀ (x : α),
    Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
        (FreeGroup.of x) ∈
      H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) z ∈ H
have mk₂ : ∀ (x : α),
  Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) (FreeGroup.of x) ∈
      H →
    Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
        (FreeGroup.of x)⁻¹ ∈
      H
Tactic: induction z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
z : FreeGroup α
mk : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) 1 ∈ H
mk₁ :
  ∀ (x : α),
    Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
        (FreeGroup.of x) ∈
      H
mk₂ :
  ∀ (x : α),
    Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
          (FreeGroup.of x) ∈
        H →
      Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
          (FreeGroup.of x)⁻¹ ∈
        H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) z ∈ H
have mk₃ : ∀ (x y : FreeGroup α),
  Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) x ∈ H →
    Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) y ∈ H →
      Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) (x * y) ∈ H
Tactic: induction z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
x_1 y : FreeGroup α
h1 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) x_1 ∈ H
h2 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) y ∈ H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) (x_1 * y) ∈ H
have mk : (↑(x_1 * y) : FreeGroup α ⧸ Subgroup.normalClosure rels) ∈ H.carrier
Tactic: change QuotientGroup.mk _ ∈ H.carrier
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
x_1 y : FreeGroup α
h1 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) x_1 ∈ H
h2 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) y ∈ H
⊢ (↑(x_1 * y) : FreeGroup α ⧸ Subgroup.normalClosure rels) ∈ H.carrier
have mk : HMul.hMul (α := HasQuotient.Quotient (FreeGroup α) (B := Subgroup (FreeGroup α)) (Subgroup.normalClosure rels))
    (↑x_1 : FreeGroup α ⧸ Subgroup.normalClosure rels) (↑y : FreeGroup α ⧸ Subgroup.normalClosure rels) ∈
  H.carrier
Tactic: rw [QuotientGroup.mk_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
G : Type u_3
inst : Group G
f : α → G
rels : Set (FreeGroup α)
h :
  ∀ r ∈ rels,
    Eq.{u_3 + 1} (α := G)
      ((((FreeGroup.lift : (a : α → G) → FreeGroup α →* G) f : MonoidHom.{u_1, u_3} (FreeGroup α) G) :
            (a : FreeGroup α) → G)
          r :
        G)
      (1 : G)
g : MonoidHom.{u_1, u_3} (PresentedGroup rels) G
hg : ∀ (x : α), (g : (a : PresentedGroup rels) → G) (PresentedGroup.of (rels := rels) x) = f x
x : PresentedGroup rels
⊢ Eq.{u_3 + 1} (α := G) ((g : (a : PresentedGroup rels) → G) x : G)
    ((toGroup (rels := rels) h : (a : PresentedGroup rels) → G) x : G)
have refine : ∀ (z : FreeGroup α),
  Eq.{u_3 + 1} (α := G) ((g : (a : PresentedGroup rels) → G) (↑z : FreeGroup α ⧸ Subgroup.normalClosure rels) : G)
    ((toGroup (rels := rels) h : (a : PresentedGroup rels) → G) (↑z : FreeGroup α ⧸ Subgroup.normalClosure rels) : G)
Tactic: refine QuotientGroup.induction_on x ?_
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
G : Type u_3
inst : Group G
rels : Set (FreeGroup α)
φ ψ : MonoidHom.{u_1, u_3} (PresentedGroup rels) G
hx :
  ∀ (x : α),
    Eq.{u_3 + 1} (α := G) ((φ : (a : PresentedGroup rels) → G) (of (rels := rels) x) : G)
      ((ψ : (a : PresentedGroup rels) → G) (of (rels := rels) x) : G)
⊢ φ = ψ
have h : ∀ (a : α),
  Eq.{u_3 + 1} (α := G)
    ((φ.comp (QuotientGroup.mk' (Subgroup.normalClosure rels)) : (a : FreeGroup α) → G) (FreeGroup.of a) : G)
    ((ψ.comp (QuotientGroup.mk' (Subgroup.normalClosure rels)) : (a : FreeGroup α) → G) (FreeGroup.of a) : G)
Tactic: ext