awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n ≤ p.length
⊢ some (p.getVert n) = getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n
have rw : some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n sorry) =
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n
Tactic: rw [getVert_eq_support_getElem p h, ← List.getElem?_eq_getElem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n ≤ p.length
rw :
  some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n ⋯) =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n
⊢ some (p.getVert n) = getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n
have rw₁ : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n =
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n
Tactic: rw [getVert_eq_support_getElem p h, ← List.getElem?_eq_getElem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ p.getVert n = p.support.getD n v
have pos : ∀ (h : n ≤ p.length), p.getVert n = p.support.getD n v
Tactic: by_cases h : n ≤ p.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
pos : ∀ (h : n ≤ p.length), p.getVert n = p.support.getD n v
⊢ p.getVert n = p.support.getD n v
have neg : ∀ (h : ¬n ≤ p.length), p.getVert n = p.support.getD n v
Tactic: by_cases h : n ≤ p.length
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : n < p.darts.length
⊢ getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h =
    { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }
have h₁ : n < p.length
Tactic: rw [p.length_darts] at h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h_1 : n < p.darts.length
h : n < p.length
⊢ getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h_1 =
    { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }
have h₁ : (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h_1).toProd.1 =
  { fst := p.getVert n, snd := p.getVert (n + 1), adj := sorry : G.Dart }.toProd.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h_1 : n < p.darts.length
h : n < p.length
h₁ :
  (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h_1).toProd.1 =
    { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ : G.Dart }.toProd.1
⊢ getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h_1 =
    { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }
have h₂ : (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts n h_1).toProd.2 =
  { fst := p.getVert n, snd := p.getVert (n + 1), adj := sorry : G.Dart }.toProd.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : [u', v'] <:+: p.support
⊢ G.Adj u' v'
have have : ∀ (k : ℕ) (hk : [u', v'].length + k ≤ p.support.length)
  (h :
    ∀ (i : ℕ) (h : i < [u', v'].length),
      getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
        some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)),
  G.Adj u' v'
Tactic: have ⟨k, hk, h⟩ := List.infix_iff_getElem?.mp h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
⊢ G.Adj u' v'
have h₀ : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
  some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two)
Tactic: have h₀ := Nat.zero_add _ ▸ h 0 Nat.zero_lt_two
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
h₀ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two)
⊢ G.Adj u' v'
have h₁ : getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (k + 1) =
  some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two)
Tactic: have h₁ := Nat.add_comm .. ▸ h 1 Nat.one_lt_two
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
h₀ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two)
h₁ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (k + 1) =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two)
⊢ G.Adj u' v'
have h₂ : p.getVert k = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two
Tactic: rw [← getVert_eq_support_getElem? _ <| by grind, Option.some.injEq] at h₀ h₁
Cleared hypotheses: h₀, h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h :
  ∀ (i : ℕ) (h : i < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
h₀ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support k =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two)
h₁ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (k + 1) =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two)
h₂ : p.getVert k = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 Nat.zero_lt_two
⊢ G.Adj u' v'
have h₃ : p.getVert (k + 1) = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 Nat.one_lt_two
Tactic: rw [← getVert_eq_support_getElem? _ <| by grind, Option.some.injEq] at h₀ h₁
Cleared hypotheses: h₀, h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ¬p.Nil
⊢ p.penultimate ∈ p.support.dropLast
have this : p.penultimate ≠ v
Tactic: have := adj_penultimate h |>.ne
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
ppt : PlacedTile ps → Prop
pt : PlacedTile ps
h :
  ∀ (i : ιₚ) (gx : G),
    ppt
      { index := i,
        groupElts :=
          (↑gx :
            G ⧸
              Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                ((↑ps : ιₚ → Prototile G X) i).symmetries) }
⊢ ppt pt
have rcases : ∀ (i : ιₚ)
  (gx :
    G ⧸
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)))
        ((↑ps : ιₚ → Prototile G X) i).symmetries),
  ppt { index := i, groupElts := gx }
Tactic: rcases pt with ⟨i, gx⟩
Cleared hypotheses: pt
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
ppt : PlacedTile ps → Prop
h :
  ∀ (i : ιₚ) (gx : G),
    ppt
      { index := i,
        groupElts :=
          (↑gx :
            G ⧸
              Subgroup.map (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)).subtype
                ((↑ps : ιₚ → Prototile G X) i).symmetries) }
i : ιₚ
gx :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i).symmetries
⊢ ppt { index := i, groupElts := gx }
have h₁ : ∀ (a : G), ppt { index := i, groupElts := ⟦a⟧ }
Tactic: induction gx using Quotient.inductionOn
Cleared hypotheses: gx
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
⊢ pt₁ = pt₂ ↔ pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
have refine_1 : ∀ (h : pt₁ = pt₂), pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
Tactic: refine ⟨fun h ↦ ?_, fun ⟨h, g, hg₁, hg₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
refine_1 : ∀ (h : pt₁ = pt₂), pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
⊢ pt₁ = pt₂ ↔ pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
have refine_2 : (pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts) →
  ∀ (h : pt₁.index = pt₂.index) (g : G) (hg₁ : ⟦g⟧ = pt₁.groupElts) (hg₂ : ⟦g⟧ = pt₂.groupElts), pt₁ = pt₂
Tactic: refine ⟨fun h ↦ ?_, fun ⟨h, g, hg₁, hg₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
h : pt₁ = pt₂
⊢ pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
have refine_1 : pt₁.index = pt₁.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₁.groupElts
Tactic: subst h
Cleared hypotheses: pt₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ : PlacedTile ps
⊢ pt₁.index = pt₁.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₁.groupElts
have refine_1 : ∃ (g : G), ⟦g⟧ = pt₁.groupElts
Tactic: simp only [and_self, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ : PlacedTile ps
⊢ ∃ (g : G), ⟦g⟧ = pt₁.groupElts
have refine_1 : ⟦Quotient.out pt₁.groupElts⟧ = pt₁.groupElts
Tactic: refine ⟨pt₁.groupElts.out, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ : PlacedTile ps
⊢ ⟦Quotient.out pt₁.groupElts⟧ = pt₁.groupElts
have refine_1 : pt₁.groupElts = pt₁.groupElts
Tactic: rw [Quotient.out_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
h_1 : pt₁.index = pt₂.index ∧ ∃ (g : G), ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
h : pt₁.index = pt₂.index
g : G
hg₁ : ⟦g⟧ = pt₁.groupElts
hg₂ : ⟦g⟧ = pt₂.groupElts
⊢ pt₁ = pt₂
have refine_2 : ∀ (i₁ : ιₚ)
  (g₁ :
    G ⧸
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
        ((↑ps : ιₚ → Prototile G X) i₁).symmetries),
  ({ index := i₁, groupElts := g₁ : PlacedTile ps }.index = pt₂.index ∧
      ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = pt₂.groupElts) →
    ∀ (h : { index := i₁, groupElts := g₁ : PlacedTile ps }.index = pt₂.index)
      (hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts), { index := i₁, groupElts := g₁ : PlacedTile ps } = pt₂
Tactic: rcases pt₁ with ⟨i₁, g₁⟩
Cleared hypotheses: pt₁, h_1, h, hg₁
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₂ : PlacedTile ps
g : G
hg₂ : ⟦g⟧ = pt₂.groupElts
i₁ : ιₚ
g₁ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
h_1 :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = pt₂.index ∧
    ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = pt₂.groupElts
h : { index := i₁, groupElts := g₁ : PlacedTile ps }.index = pt₂.index
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps } = pt₂
have refine_2 : ∀ (i₂ : ιₚ)
  (g₂ :
    G ⧸
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₂) : Set X)))
        ((↑ps : ιₚ → Prototile G X) i₂).symmetries)
  (hg₂ : ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts),
  ({ index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₂, groupElts := g₂ : PlacedTile ps }.index ∧
      ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts) →
    ∀
      (h :
        { index := i₁, groupElts := g₁ : PlacedTile ps }.index =
          { index := i₂, groupElts := g₂ : PlacedTile ps }.index),
      { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₂, groupElts := g₂ }
Tactic: rcases pt₂ with ⟨i₂, g₂⟩
Cleared hypotheses: pt₂, hg₂, h_1, h
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
i₂ : ιₚ
g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₂) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₂).symmetries
hg₂ : ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts
h_1 :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₂, groupElts := g₂ : PlacedTile ps }.index ∧
    ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₂, groupElts := g₂ }.groupElts
h : i₁ = i₂
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₂, groupElts := g₂ }
have refine_2 : ∀
  (g₂ :
    G ⧸
      Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
        ((↑ps : ιₚ → Prototile G X) i₁).symmetries)
  (hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts),
  ({ index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
      ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts) →
    { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₁, groupElts := g₂ }
Tactic: subst h
Cleared hypotheses: i₂, g₂, hg₂, h_1, h
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
h :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
    ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₁, groupElts := g₂ }
have refine_2 : { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ :
  G ⧸
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) i₁) : Set X)))
      ((↑ps : ιₚ → Prototile G X) i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
h :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index ∧
    ∃ (g : G), ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
refine_2 :
  { index := i₁, groupElts := g₁ : PlacedTile ps }.index = { index := i₁, groupElts := g₂ : PlacedTile ps }.index
⊢ { index := i₁, groupElts := g₁ : PlacedTile ps } = { index := i₁, groupElts := g₂ }
have refine_2₁ : { index := i₁, groupElts := g₁ : PlacedTile ps }.groupElts ≍ { index := i₁, groupElts := g₂ : PlacedTile ps }.groupElts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
⊢ pt₁ = pt₂ ↔
    pt₁.index = pt₂.index ∧
      Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
          {pt₁.groupElts} =
        Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
          {pt₂.groupElts}
have refine_1 : ∀ (h : pt₁ = pt₂),
  pt₁.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts}
Tactic: refine ⟨fun h ↦ ?_, fun ⟨hi, hq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
refine_1 :
  ∀ (h : pt₁ = pt₂),
    pt₁.index = pt₂.index ∧
      Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
          {pt₁.groupElts} =
        Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
          {pt₂.groupElts}
⊢ pt₁ = pt₂ ↔
    pt₁.index = pt₂.index ∧
      Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
          {pt₁.groupElts} =
        Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
          {pt₂.groupElts}
have refine_2 : pt₁.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts} →
  ∀ (hi : pt₁.index = pt₂.index)
    (hq :
      Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
          {pt₁.groupElts} =
        Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map
                (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
                ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
          {pt₂.groupElts}),
    pt₁ = pt₂
Tactic: refine ⟨fun h ↦ ?_, fun ⟨hi, hq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Tiling.Tile (goal)
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
h : pt₁ = pt₂
⊢ pt₁.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₂.index) : Set X)))
              ((↑ps : ιₚ → Prototile G X) pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts}
have refine_1 : pt₁.index = pt₁.index ∧
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
            ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
      {pt₁.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (Subgroup.subtype (MulAction.stabilizer G (↑((↑ps : ιₚ → Prototile G X) pt₁.index) : Set X)))
            ((↑ps : ιₚ → Prototile G X) pt₁.index).symmetries)) ⁻¹'
      {pt₁.groupElts}
Tactic: subst h
Cleared hypotheses: pt₂, h