awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G_1 : Type u
H : Type v
inst : Mul G_1
inst_1 : Mul H
ι : Type u_2
G : ι → Type u_1
inst_2 : (i : ι) → Mul (G i)
inst_3 : ∀ (i : ι), TwoUniqueProds.{u_1} (G i)
A_1 : Finset ((i : ι) → G i)
h : IsWellFounded (Finset ((i : ι) → G i)) fun (x1 x2 : Finset ((i : ι) → G i)) ↦ x1 ⊂ x2 := ⋯
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
hc_2 : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h1 : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
hc : 1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
pos :
  ∀ (hA : {a ∈ A | a i = p1.1} = A),
    1 < #({a ∈ A | a i = p1.1}) * #({a ∈ B | a i = p1.2}) →
      ∃ p1_1 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
        ∃ p2 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
          p1_1 ≠ p2 ∧
            UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧
              UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p2.1 p2.2
⊢ 1 < #({a ∈ A | a i = p1.1}) * #({a ∈ B | a i = p1.2}) →
    ∃ p1_1 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
      ∃ p2 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
        p1_1 ≠ p2 ∧
          UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧
            UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p2.1 p2.2
have neg : ∀ (hA : ¬{a ∈ A | a i = p1.1} = A),
  1 < #({a ∈ A | a i = p1.1}) * #({a ∈ B | a i = p1.2}) →
    ∃ p1_1 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
      ∃ p2 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
        p1_1 ≠ p2 ∧
          UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧
            UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p2.1 p2.2
Tactic: by_cases hA : {a ∈ A | a i = p1.1} = A
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G_1 : Type u
H : Type v
inst : Mul G_1
inst_1 : Mul H
ι : Type u_2
G : ι → Type u_1
inst_2 : (i : ι) → Mul (G i)
inst_3 : ∀ (i : ι), TwoUniqueProds.{u_1} (G i)
A_1 : Finset ((i : ι) → G i)
h : IsWellFounded (Finset ((i : ι) → G i)) fun (x1 x2 : Finset ((i : ι) → G i)) ↦ x1 ⊂ x2 := ⋯
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B_1 B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc_1 : 1 < #A * #B
hA_1 : A.Nonempty
hB : B.Nonempty
hc_2 : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun (x : (i : ι) → G i) ↦ x i) A) (image (fun (x : (i : ι) → G i) ↦ x i) B) p2.1 p2.2
h1 : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
hc : 1 < card.{u_1} (α := G i) (image (fun (x : (i : ι) → G i) ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA : {a ∈ A | a i = p1.1} = A
⊢ 1 < #({a ∈ A | a i = p1.1}) * #({a ∈ B | a i = p1.2}) →
    ∃ p1_1 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
      ∃ p2 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
        p1_1 ≠ p2 ∧
          UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧
            UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p2.1 p2.2
have pos : 1 < #A * #({a ∈ B | a i = p1.2}) →
  ∃ p1_1 ∈ A ×ˢ {a ∈ B | a i = p1.2},
    ∃ p2 ∈ A ×ˢ {a ∈ B | a i = p1.2},
      p1_1 ≠ p2 ∧ UniqueMul A ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧ UniqueMul A ({a ∈ B | a i = p1.2}) p2.1 p2.2
Tactic: rw [hA]
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G_1 : Type u
H : Type v
inst : Mul G_1
inst_1 : Mul H
ι : Type u_2
G : ι → Type u_1
inst_2 : (i : ι) → Mul (G i)
inst_3 : ∀ (i : ι), TwoUniqueProds.{u_1} (G i)
A : Finset ((i : ι) → G i)
let let₁ let₂ :
  ∀ {B : Finset ((i : ι) → G i)},
    1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
⊢ ∀ {B : Finset ((i : ι) → G i)},
    1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have let₃ : ∀ (x : Finset ((i : ι) → G i)),
  (∀ y ⊂ x,
      ∀ {B : Finset ((i : ι) → G i)},
        1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2) →
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #x * #B → ∃ p1 ∈ x ×ˢ B, ∃ p2 ∈ x ×ˢ B, p1 ≠ p2 ∧ UniqueMul x B p1.1 p1.2 ∧ UniqueMul x B p2.1 p2.2
Tactic: classical
    let _ := isWellFounded_ssubset (α := ∀ i, G i) -- why need this?
    apply IsWellFounded.induction (· ⊂ ·) A; intro A ihA B
    apply IsWellFounded.induction (· ⊂ ·) B; intro B ihB hc
    obtain ⟨hA, hB, hc⟩ := Nat.one_lt_mul_iff.mp hc
    rw [card_pos] at hA hB
    obtain ⟨i, hc⟩ := exists_or.mpr (hc.imp exists_of_one_lt_card_pi exists_of_one_lt_card_pi)
    obtain ⟨p1, h1, p2, h2, hne, hi1, hi2⟩ := uniqueMul_of_one_lt_card (Nat.one_lt_mul_iff.mpr
      ⟨card_pos.2 (hA.image _), card_pos.2 (hB.image _), hc.imp And.left And.left⟩)
    simp_rw [mem_product, mem_image, ← filter_nonempty_iff] at h1 h2
    replace h1 := uniqueMul_of_twoUniqueMul ?_ h1.1 h1.2
    on_goal 1 => replace h2 := uniqueMul_of_twoUniqueMul ?_ h2.1 h2.2
    · obtain ⟨a1, ha1, b1, hb1, hu1⟩ := h1
      obtain ⟨a2, ha2, b2, hb2, hu2⟩ := h2
      rw [mem_filter] at ha1 hb1 ha2 hb2
      simp_rw [mem_product]
      refine ⟨(a1, b1), ⟨ha1.1, hb1.1⟩, (a2, b2), ⟨ha2.1, hb2.1⟩, ?_,
        UniqueMul.of_image_filter (Pi.evalMulHom G i) ha1.2 hb1.2 hi1 hu1,
        UniqueMul.of_image_filter (Pi.evalMulHom G i) ha2.2 hb2.2 hi2 hu2⟩
      grind
    all_goals rcases hc with hc | hc; · exact ihA _ (hc.2 _)
    · by_cases hA : {a ∈ A | a i = p2.1} = A
      · rw [hA]
        exact ihB _ (hc.2 _)
      · exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)
    · by_cases hA : {a ∈ A | a i = p1.1} = A
      · rw [hA]
        exact ihB _ (hc.2 _)
      · exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
⊢ TwoUniqueProds (G × H)
have refine_3 : TwoUniqueProds (I G H true)
Tactic: have : ∀ b, TwoUniqueProds (I G H b) := Bool.rec ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
refine_3 : TwoUniqueProds (I G H true)
⊢ TwoUniqueProds (G × H)
have refine_1 : ∀ (this : ∀ (b : Bool), TwoUniqueProds (I G H b)), TwoUniqueProds (G × H)
Tactic: have : ∀ b, TwoUniqueProds (I G H b) := Bool.rec ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
refine_3 : TwoUniqueProds (I G H true)
refine_1 : ∀ (this : ∀ (b : Bool), TwoUniqueProds (I G H b)), TwoUniqueProds (G × H)
⊢ TwoUniqueProds (G × H)
have refine_2 : TwoUniqueProds (I G H false)
Tactic: have : ∀ b, TwoUniqueProds (I G H b) := Bool.rec ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
⊢ TwoUniqueProds (G × H)
have refine_1 : ∀ (x y : G × H)
  (he :
    Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
      ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)),
  x.1 = y.1
Tactic: refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he ↦ Prod.ext ?_ ?_)
      (TwoUniqueProds.instForall <| I G H)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
refine_1 :
  ∀ (x y : G × H)
    (he :
      Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
        ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)),
    x.1 = y.1
⊢ TwoUniqueProds (G × H)
have refine_1₁ : ∀ (x y : G × H)
  (he :
    Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
      ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)),
  x.2 = y.2
Tactic: refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he ↦ Prod.ext ?_ ?_)
      (TwoUniqueProds.instForall <| I G H)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he :
  Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
    ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)
⊢ x.1 = y.1
have refine_1 : { down := x.1 : ULift.{v, u} G } = { down := y.1 }
Tactic: apply up_injective
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : TwoUniqueProds G
inst_3 : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
x y : G × H
he :
  Eq (α := (b : Bool) → I G H b) ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) x : (b : Bool) → I G H b)
    ((Prod.upMulHom G H : (a : G × H) → (b : Bool) → I G H b) y : (b : Bool) → I G H b)
⊢ x.2 = y.2
have refine_1 : { down := x.2 : ULift.{u, v} H } = { down := y.2 }
Tactic: apply up_injective
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
hc : 1 < #A * #B
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hc₁ : 1 < #(map f B) * #(map f A)
Tactic: rw [← card_map f, ← card_map f, mul_comm] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have obtain : ∀ (p1 : Gᵐᵒᵖ × Gᵐᵒᵖ) (h1 : p1 ∈ map f B ×ˢ map f A) (p2 : Gᵐᵒᵖ × Gᵐᵒᵖ) (h2 : p2 ∈ map f B ×ˢ map f A) (hne : p1 ≠ p2)
  (hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2) (hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: obtain ⟨p1, h1, p2, h2, hne, hu1, hu2⟩ := h.uniqueMul_of_one_lt_card hc
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 : Gᵐᵒᵖ × Gᵐᵒᵖ
h1 : p1 ∈ map f B ×ˢ map f A
p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
h2 : p2 ∈ map f B ×ˢ map f A
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have simp_rw : ∀ (h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A) (h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A),
  ∃ (p1 : G × G),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧
      ∃ (p2 : G × G), (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: simp_rw [mem_product] at h1 h2 ⊢
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ ∃ (p1 : G × G),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧
      ∃ (p2 : G × G), (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have refine_1 : (p1.2.1, p1.1.1).1 ∈ A
Tactic: refine ⟨(_, _), ⟨?_, ?_⟩, (_, _), ⟨?_, ?_⟩, ?_, hu1.of_mulOpposite, hu2.of_mulOpposite⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
refine_1 : (p1.2.1, p1.1.1).1 ∈ A
⊢ ∃ (p1 : G × G),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧
      ∃ (p2 : G × G), (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have refine_2 : (p1.2.1, p1.1.1).2 ∈ B
Tactic: refine ⟨(_, _), ⟨?_, ?_⟩, (_, _), ⟨?_, ?_⟩, ?_, hu1.of_mulOpposite, hu2.of_mulOpposite⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
refine_1 : (p1.2.1, p1.1.1).1 ∈ A
refine_2 : (p1.2.1, p1.1.1).2 ∈ B
⊢ ∃ (p1 : G × G),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧
      ∃ (p2 : G × G), (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have refine_3 : (p2.2.1, p2.1.1).1 ∈ A
Tactic: refine ⟨(_, _), ⟨?_, ?_⟩, (_, _), ⟨?_, ?_⟩, ?_, hu1.of_mulOpposite, hu2.of_mulOpposite⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
refine_1 : (p1.2.1, p1.1.1).1 ∈ A
refine_2 : (p1.2.1, p1.1.1).2 ∈ B
refine_3 : (p2.2.1, p2.1.1).1 ∈ A
⊢ ∃ (p1 : G × G),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧
      ∃ (p2 : G × G), (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have refine_4 : (p2.2.1, p2.1.1).2 ∈ B
Tactic: refine ⟨(_, _), ⟨?_, ?_⟩, (_, _), ⟨?_, ?_⟩, ?_, hu1.of_mulOpposite, hu2.of_mulOpposite⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
refine_1 : (p1.2.1, p1.1.1).1 ∈ A
refine_2 : (p1.2.1, p1.1.1).2 ∈ B
refine_3 : (p2.2.1, p2.1.1).1 ∈ A
refine_4 : (p2.2.1, p2.1.1).2 ∈ B
⊢ ∃ (p1 : G × G),
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧
      ∃ (p2 : G × G), (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have refine_5 : Ne.{u + 1} (α := G × G) (p1.2.1, p1.1.1) (p2.2.1, p2.1.1)
Tactic: refine ⟨(_, _), ⟨?_, ?_⟩, (_, _), ⟨?_, ?_⟩, ?_, hu1.of_mulOpposite, hu2.of_mulOpposite⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ Ne.{u + 1} (α := G × G) (p1.2.1, p1.1.1) (p2.2.1, p2.1.1)
have refine_5 : ∀ (hne : Eq.{u + 1} (α := G × G) (p1.2.1, p1.1.1) (p2.2.1, p2.1.1)), p1 = p2
Tactic: contrapose hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
hne : Eq.{u + 1} (α := G × G) (p1.2.1, p1.1.1) (p2.2.1, p2.1.1)
⊢ p1 = p2
have refine_5 : ∀
  (hne :
    Eq.{u + 1} (α := G) (p1.2.1, p1.1.1).1 (p2.2.1, p2.1.1).1 ∧
      Eq.{u + 1} (α := G) (p1.2.1, p1.1.1).2 (p2.2.1, p2.1.1).2),
  p1.1 = p2.1 ∧ p1.2 = p2.2
Tactic: rw [Prod.ext_iff] at hne ⊢
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ (p1.2.1, p1.1.1).1 ∈ A
have refine_1 : Membership.mem (α := Gᵐᵒᵖ) (map f A) ((f : (a : G) → Gᵐᵒᵖ) (p1.2.1, p1.1.1).1 : Gᵐᵒᵖ)
Tactic: apply (mem_map' f).mp
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ (p1.2.1, p1.1.1).2 ∈ B
have refine_2 : Membership.mem (α := Gᵐᵒᵖ) (map f B) ((f : (a : G) → Gᵐᵒᵖ) (p1.2.1, p1.1.1).2 : Gᵐᵒᵖ)
Tactic: apply (mem_map' f).mp
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ (p2.2.1, p2.1.1).1 ∈ A
have refine_3 : Membership.mem (α := Gᵐᵒᵖ) (map f A) ((f : (a : G) → Gᵐᵒᵖ) (p2.2.1, p2.1.1).1 : Gᵐᵒᵖ)
Tactic: apply (mem_map' f).mp
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
inst : Mul G
h : TwoUniqueProds.{u} Gᵐᵒᵖ
A B : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B) * #(map f A)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B) (map f A) p1.1 p1.2
hu2 : UniqueMul (map f B) (map f A) p2.1 p2.2
h1 : p1.1 ∈ map f B ∧ p1.2 ∈ map f A
h2 : p2.1 ∈ map f B ∧ p2.2 ∈ map f A
⊢ (p2.2.1, p2.1.1).2 ∈ B
have refine_4 : Membership.mem (α := Gᵐᵒᵖ) (map f B) ((f : (a : G) → Gᵐᵒᵖ) (p2.2.1, p2.1.1).2 : Gᵐᵒᵖ)
Tactic: apply (mem_map' f).mp
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hA : 0 < #A
Tactic: obtain ⟨hA, hB, -⟩ := Nat.one_lt_mul_iff.mp hc
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
hA : 0 < #A
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hB : 0 < #B
Tactic: obtain ⟨hA, hB, -⟩ := Nat.one_lt_mul_iff.mp hc
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
hA : 0 < #A
hB : 0 < #B
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hA₁ : A.Nonempty
Tactic: rw [card_pos] at hA hB
Cleared hypotheses: hA, hB
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
hA : 0 < #A
hB : 0 < #B
hA₁ : A.Nonempty
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hB₁ : B.Nonempty
Tactic: rw [card_pos] at hA hB
Cleared hypotheses: hA, hB
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
hA : A.Nonempty
hB : B.Nonempty
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have hc₁ : 1 < #(A ×ˢ B)
Tactic: rw [← card_product] at hc
Cleared hypotheses: hc, hA, hB
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have obtain : ∀ (a0 : G) (ha0 : a0 ∈ A) (b0 : G) (hb0 : b0 ∈ B) (he0 : a0 * b0 = (A * B).max' sorry),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: obtain ⟨a0, ha0, b0, hb0, he0⟩ := mem_mul.mp (max'_mem _ <| hA.mul hB)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have obtain : ∀ (a1 : G) (ha1 : a1 ∈ A) (b1 : G) (hb1 : b1 ∈ B) (he1 : a1 * b1 = (A * B).min' sorry),
  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Tactic: obtain ⟨a1, ha1, b1, hb1, he1⟩ := mem_mul.mp (min'_mem _ <| hA.mul hB)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
have inl : ∀ (hl : b < b0), a = a0 ∧ b = b0
Tactic: obtain hl | rfl | hl := lt_trichotomy b b0