awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
⊢ x ≠ 1

Tactic:
have hx1 : x ≠ 1 := by rintro rfl; simp_all only [ne_eq, one_mem, not_true_eq_false]
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
⊢ Ne (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g₁ : PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) 1 : PushoutI (G := G) φ)

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
⊢ g₁ ≠ 1

Tactic:
have hg₁1 : g₁ ≠ 1 :=
        ne_of_apply_ne (of (φ := φ) i) (by simp_all)
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
⊢ Ne (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) g₂ : PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) 1 : PushoutI (G := G) φ)

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
⊢ g₂ ≠ 1

Tactic:
have hg₂1 : g₂ ≠ 1 :=
        ne_of_apply_ne (of (φ := φ) j) (by simp_all)
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₂1 : g₂ ≠ 1
y : H
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) = x
hg₁1 : Ne.{u_2 + 1} (α := G i) ((φ i : (a : H) → G i) y : G i) (1 : G i)
⊢ Eq (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) g₂ : PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)

Tactic:
subst hg₁
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₂1 : g₂ ≠ 1
y : H
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) = x
hg₁1 : Ne.{u_2 + 1} (α := G i) ((φ i : (a : H) → G i) y : G i) (1 : G i)
hg₃ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) g₂ : PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
⊢ ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
      ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)

Tactic:
subst hg₁
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₂1 : g₂ ≠ 1
y : H
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) = x
hg₁1 : Ne.{u_2 + 1} (α := G i) ((φ i : (a : H) → G i) y : G i) (1 : G i)
hg₃ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) g₂ : PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
hx₁ :
  ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
      ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
⊢ Ne (α := PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ) (1 : PushoutI (G := G) φ)

Tactic:
subst hg₁
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
g₂ : G j
hg₂1 : g₂ ≠ 1
y : H
hg₁1 : Ne.{u_2 + 1} (α := G i) ((φ i : (a : H) → G i) y : G i) (1 : G i)
hg₂ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) g₂ : PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
hx :
  ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
      ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
hx1 :
  Ne (α := PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ) (1 : PushoutI (G := G) φ)
⊢ False

Tactic:
hx (of_apply_eq_base φ i y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)

Premises used: Iff.mpr, Monoid.PushoutI.of_apply_eq_base, Eq.rec, MonoidHom.mem_range, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
g₂ : G j
hg₂1 : g₂ ≠ 1
y : H
hg₁1 : Ne.{u_2 + 1} (α := G i) ((φ i : (a : H) → G i) y : G i) (1 : G i)
hg₂ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) g₂ : PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
hx :
  ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
      ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ)
hx1 :
  Ne (α := PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) y) : PushoutI (G := G) φ) (1 : PushoutI (G := G) φ)
⊢ False

Tactic:
exact hx (of_apply_eq_base φ i y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)

Premises used: Iff.mpr, Monoid.PushoutI.of_apply_eq_base, Eq.rec, MonoidHom.mem_range, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
⊢ g₁ ∉ (φ i).range

Tactic:
have hg₁r : g₁ ∉ (φ i).range := by
        rintro ⟨y, rfl⟩
        subst hg₁
        exact hx (of_apply_eq_base φ i y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₁r : g₁ ∉ (φ i).range
y : H
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) = x
hg₂1 : Ne.{u_2 + 1} (α := G j) ((φ j : (a : H) → G j) y : G j) (1 : G j)
⊢ Eq (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g₁ : PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)

Tactic:
subst hg₂
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₁r : g₁ ∉ (φ i).range
y : H
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) = x
hg₂1 : Ne.{u_2 + 1} (α := G j) ((φ j : (a : H) → G j) y : G j) (1 : G j)
hg₃ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g₁ : PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
⊢ ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
      ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)

Tactic:
subst hg₂
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₁r : g₁ ∉ (φ i).range
y : H
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) = x
hg₂1 : Ne.{u_2 + 1} (α := G j) ((φ j : (a : H) → G j) y : G j) (1 : G j)
hg₃ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g₁ : PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
hx₁ :
  ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
      ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
⊢ Ne (α := PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ) (1 : PushoutI (G := G) φ)

Tactic:
subst hg₂
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
g₁ : G i
hg₁1 : g₁ ≠ 1
hg₁r : g₁ ∉ (φ i).range
y : H
hg₂1 : Ne.{u_2 + 1} (α := G j) ((φ j : (a : H) → G j) y : G j) (1 : G j)
hg₁ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g₁ : PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
hx :
  ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
      ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
hx1 :
  Ne (α := PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ) (1 : PushoutI (G := G) φ)
⊢ False

Tactic:
hx (of_apply_eq_base φ j y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)

Premises used: Iff.mpr, Monoid.PushoutI.of_apply_eq_base, Eq.rec, MonoidHom.mem_range, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
g₁ : G i
hg₁1 : g₁ ≠ 1
hg₁r : g₁ ∉ (φ i).range
y : H
hg₂1 : Ne.{u_2 + 1} (α := G j) ((φ j : (a : H) → G j) y : G j) (1 : G j)
hg₁ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g₁ : PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
hx :
  ¬Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
      ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ)
hx1 :
  Ne (α := PushoutI (G := G) φ)
    ((of (G := G) j : (a : G j) → PushoutI φ) ((φ j : (a : H) → G j) y) : PushoutI (G := G) φ) (1 : PushoutI (G := G) φ)
⊢ False

Tactic:
exact hx (of_apply_eq_base φ j y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)

Premises used: Iff.mpr, Monoid.PushoutI.of_apply_eq_base, Eq.rec, MonoidHom.mem_range, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
⊢ g₂ ∉ (φ j).range

Tactic:
have hg₂r : g₂ ∉ (φ j).range := by
        rintro ⟨y, rfl⟩
        subst hg₂
        exact hx (of_apply_eq_base φ j y ▸ MonoidHom.mem_range.2 ⟨y, rfl⟩)
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
⊢ ∀ l ∈ [Sigma.mk (β := fun (i : ι) ↦ G i) i g₁, Sigma.mk (β := fun (i : ι) ↦ G i) j g₂⁻¹],
    l.snd (β := fun (i : ι) ↦ G i) ≠ 1

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
⊢ List.IsChain (fun (l l' : (i : ι) × G i) ↦ l.fst (β := fun (i : ι) ↦ G i) ≠ l'.fst (β := fun (i : ι) ↦ G i))
    [Sigma.mk (β := fun (i : ι) ↦ G i) i g₁, Sigma.mk (β := fun (i : ι) ↦ G i) j g₂⁻¹]

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
w : Word G := Word.mk (M := G) [Sigma.mk (β := fun (i : ι) ↦ G i) i g₁, Sigma.mk (β := fun (i : ι) ↦ G i) j g₂⁻¹] ⋯ ⋯
⊢ Reduced (G := G) φ w

Tactic:
simp only [w, Reduced, List.mem_cons,
          forall_eq_or_imp, not_false_eq_true,
          hg₁r, hg₂r, List.mem_nil_iff, false_imp_iff, imp_true_iff, and_true,
          inv_mem_iff]

Premises used: and_true, inv_mem_iff, forall_eq_or_imp, imp_true_iff, false_imp_iff, List.mem_cons, Monoid.PushoutI.Reduced, not_false_eq_true, List.mem_nil_iff
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
w : Word G := Word.mk (M := G) [Sigma.mk (β := fun (i : ι) ↦ G i) i g₁, Sigma.mk (β := fun (i : ι) ↦ G i) j g₂⁻¹] ⋯ ⋯
⊢ Reduced (G := G) φ w

Tactic:
have hw : Reduced φ w := by
        simp only [w, Reduced, List.mem_cons,
          forall_eq_or_imp, not_false_eq_true,
          hg₁r, hg₂r, List.mem_nil_iff, false_imp_iff, imp_true_iff, and_true,
          inv_mem_iff]
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
w : Word G := Word.mk (M := G) [Sigma.mk (β := fun (i : ι) ↦ G i) i g₁, Sigma.mk (β := fun (i : ι) ↦ G i) j g₂⁻¹] ⋯ ⋯
hw : Reduced (G := G) φ w
⊢ Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
    ((ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) : PushoutI (G := G) φ)

Tactic:
simp only [w, Word.prod, List.map_cons, List.prod_cons, List.prod_nil,
          List.map_nil, map_mul, ofCoprodI_of, hg₁, hg₂, map_inv, mul_one,
          mul_inv_cancel, one_mem]

Premises used: map_inv, List.map_cons, Monoid.CoprodI.Word.prod, Monoid.PushoutI.ofCoprodI_of, map_mul, List.prod_nil, mul_inv_cancel, OneMemClass.one_mem, mul_one, List.prod_cons, List.map_nil
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
w : Word G := Word.mk (M := G) [Sigma.mk (β := fun (i : ι) ↦ G i) i g₁, Sigma.mk (β := fun (i : ι) ↦ G i) j g₂⁻¹] ⋯ ⋯
hw : Reduced (G := G) φ w
⊢ w = Word.empty (M := G)

Tactic:
have := hw.eq_empty_of_mem_range hφ (by
        simp only [w, Word.prod, List.map_cons, List.prod_cons, List.prod_nil,
          List.map_nil, map_mul, ofCoprodI_of, hg₁, hg₂, map_inv, mul_one,
          mul_inv_cancel, one_mem])
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
hx : ¬x ∈ (base (G := G) φ).range
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
w : Word G := Word.mk (M := G) [Sigma.mk (β := fun (i : ι) ↦ G i) i g₁, Sigma.mk (β := fun (i : ι) ↦ G i) j g₂⁻¹] ⋯ ⋯
hw : Reduced (G := G) φ w
this : w = Word.empty (M := G)
⊢ False

Tactic:
simp [w, Word.empty] at this

Premises used: Monoid.CoprodI.Word.empty
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
rw :
  LE.le (α := Subgroup (PushoutI (G := G) φ)) (MonoidHom.range (G := H) (MonoidHom.comp (of (G := G) i) (φ i)))
    (MonoidHom.range (of (G := G) i))
⊢ (base (G := G) φ).range ≤ MonoidHom.range (of (G := G) i)

Tactic:
rw [← of_comp_eq_base i]

Premises used: Monoid.PushoutI.of_comp_eq_base
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
h : H
⊢ Membership.mem (α := PushoutI (G := G) φ) (γ := Subgroup (PushoutI (G := G) φ)) (MonoidHom.range (of (G := G) i))
    ((MonoidHom.comp (of (G := G) i) (φ i) : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)

Tactic:
MonoidHom.mem_range.2 ⟨φ i h, rfl⟩

Premises used: Iff.mpr, MonoidHom.mem_range, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
h : H
⊢ Membership.mem (α := PushoutI (G := G) φ) (γ := Subgroup (PushoutI (G := G) φ)) (MonoidHom.range (of (G := G) i))
    ((MonoidHom.comp (of (G := G) i) (φ i) : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)

Tactic:
exact MonoidHom.mem_range.2 ⟨φ i h, rfl⟩

Premises used: Iff.mpr, MonoidHom.mem_range, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
rw :
  LE.le (α := Subgroup (PushoutI (G := G) φ)) (MonoidHom.range (G := H) (MonoidHom.comp (of (G := G) j) (φ j)))
    (MonoidHom.range (of (G := G) j))
⊢ (base (G := G) φ).range ≤ MonoidHom.range (of (G := G) j)

Tactic:
rw [← of_comp_eq_base j]

Premises used: Monoid.PushoutI.of_comp_eq_base