awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
⊢ (↑l.length : ℕ∞) ≤ ENat.card α
have inl : Finite α → (↑l.length : ℕ∞) ≤ ENat.card α
Tactic: cases finite_or_infinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
inl : Finite α → (↑l.length : ℕ∞) ≤ ENat.card α
⊢ (↑l.length : ℕ∞) ≤ ENat.card α
have inr : Infinite α → (↑l.length : ℕ∞) ≤ ENat.card α
Tactic: cases finite_or_infinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
h_1 : Finite α
⊢ (↑l.length : ℕ∞) ≤ ENat.card α
have inl : (↑(Nat.card α) : ℕ∞) ≤ ENat.card α
Tactic: grw [h.length_le_natCard, ENat.card_eq_coe_natCard]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
h_1 : Finite α
inl : (↑(Nat.card α) : ℕ∞) ≤ ENat.card α
⊢ (↑l.length : ℕ∞) ≤ ENat.card α
have inl₁ : LE.le (α := ℕ∞) (↑(Nat.card α) : ℕ∞) (↑(Nat.card α) : ℕ∞)
Tactic: grw [h.length_le_natCard, ENat.card_eq_coe_natCard]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
h_1 : Infinite α
⊢ (↑l.length : ℕ∞) ≤ ENat.card α
have inr : LE.le (α := ℕ∞) (↑l.length : ℕ∞) ⊤
Tactic: grw [ENat.card_eq_top_of_infinite]
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ Nat.card.{u_1} (Perm α) = (Nat.card α)!
have have : ∀ (this : Fintype α), Nat.card.{u_1} (Perm α) = (Nat.card α)!
Tactic: have := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
⊢ Nat.card.{u_1} (Perm α) = (Nat.card α)!
have rw : Fintype.card.{u_1} (Perm α) = (Nat.card α)!
Tactic: rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
rw : Fintype.card.{u_1} (Perm α) = (Nat.card α)!
⊢ Nat.card.{u_1} (Perm α) = (Nat.card α)!
have rw₁ : Fintype.card.{u_1} (Perm α) = (Fintype.card α)!
Tactic: rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
rw : Fintype.card.{u_1} (Perm α) = (Nat.card α)!
rw₁ : Fintype.card.{u_1} (Perm α) = (Fintype.card α)!
⊢ Nat.card.{u_1} (Perm α) = (Nat.card α)!
have rw₂ : (Fintype.card α)! = (Fintype.card α)!
Tactic: rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ Nat.card.{u_1} (Perm α) = (Nat.card α)!
have have : ∀ (this : Fintype α), Nat.card.{u_1} (Perm α) = (Nat.card α)!
Tactic: classical
  have := Fintype.ofFinite α
  rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
hα : Nat.card α ≤ 2
⊢ IsCyclic.{u_1} (Perm α)
have apply : Nat.card.{u_1} (Perm α) ∣ 2
Tactic: apply isCyclic_of_card_dvd_prime (p := 2)
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ IsMulCommutative.{u_1} (Perm α) ↔ Nat.card α ≤ 2
have refine : IsMulCommutative.{u_1} (Perm α) → Nat.card α ≤ 2
Tactic: refine ⟨?_, fun h ↦ (isCyclic_of_card_le_two h).isMulCommutative⟩
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
h : ∀ (a b : Perm α), a * b = b * a
⊢ Nat.card α ≤ 2
have rw : ¬∃ (a : α) (b : α) (c : α),
    Membership.mem (γ := Set α) _root_.Set.univ a ∧
      Membership.mem (γ := Set α) _root_.Set.univ b ∧
        Membership.mem (γ := Set α) _root_.Set.univ c ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: rw [← not_lt, ← Set.ncard_univ, Set.two_lt_ncard_iff]
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
h : ∀ (a b : Perm α), a * b = b * a
a b c : α
left : Membership.mem (γ := Set α) _root_.Set.univ a
left_1 : Membership.mem (γ := Set α) _root_.Set.univ b
left_2 : Membership.mem (γ := Set α) _root_.Set.univ c
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ False
have apply : b = c
Tactic: apply hbc
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (hypothesis)
Goal:
α : Type u_1
inst : Finite α
h : ∀ (a b : Perm α), a * b = b * a
a b c : α
left : Membership.mem (γ := Set α) _root_.Set.univ a
left_1 : Membership.mem (γ := Set α) _root_.Set.univ b
left_2 : Membership.mem (γ := Set α) _root_.Set.univ c
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = c
have h₁ : ∀ (a b : Perm α) (x : α), Eq (α := α) ((a * b : (a : α) → α) x : α) ((b * a : (a : α) → α) x : α)
Tactic: simp_rw [Perm.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ IsMulCommutative.{u_1} (Perm α) → Nat.card α ≤ 2
have rintro : ∀ (h : ∀ (a b : Perm α), a * b = b * a), Nat.card α ≤ 2
Tactic: classical
  rintro ⟨⟨h⟩⟩
  rw [← not_lt, ← Set.ncard_univ, Set.two_lt_ncard_iff]
  rintro ⟨a, b, c, _, _, _, hab, hac, hbc⟩
  apply hbc
  simp_rw [Perm.ext_iff] at h
  simpa [swap_apply_of_ne_of_ne hab hac] using h (swap a b) (swap b c) a
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
rintro : ∀ (h : ∀ (a b : Perm α), a * b = b * a), Nat.card α ≤ 2
⊢ IsMulCommutative.{u_1} (Perm α) → Nat.card α ≤ 2
have rintro₁ : ∀ (h : ∀ (a b : Perm α), a * b = b * a),
  ¬∃ (a : α) (b : α) (c : α),
      Membership.mem (γ := Set α) _root_.Set.univ a ∧
        Membership.mem (γ := Set α) _root_.Set.univ b ∧
          Membership.mem (γ := Set α) _root_.Set.univ c ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: classical
  rintro ⟨⟨h⟩⟩
  rw [← not_lt, ← Set.ncard_univ, Set.two_lt_ncard_iff]
  rintro ⟨a, b, c, _, _, _, hab, hac, hbc⟩
  apply hbc
  simp_rw [Perm.ext_iff] at h
  simpa [swap_apply_of_ne_of_ne hab hac] using h (swap a b) (swap b c) a
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
rintro : ∀ (h : ∀ (a b : Perm α), a * b = b * a), Nat.card α ≤ 2
rintro₁ :
  ∀ (h : ∀ (a b : Perm α), a * b = b * a),
    ¬∃ (a : α) (b : α) (c : α),
        Membership.mem (γ := Set α) _root_.Set.univ a ∧
          Membership.mem (γ := Set α) _root_.Set.univ b ∧
            Membership.mem (γ := Set α) _root_.Set.univ c ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ IsMulCommutative.{u_1} (Perm α) → Nat.card α ≤ 2
have rintro₂ : ∀ (h : ∀ (a b : Perm α), a * b = b * a) (a b c : α),
  Membership.mem (γ := Set α) _root_.Set.univ a →
    Membership.mem (γ := Set α) _root_.Set.univ b →
      Membership.mem (γ := Set α) _root_.Set.univ c → ∀ (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c), False
Tactic: classical
  rintro ⟨⟨h⟩⟩
  rw [← not_lt, ← Set.ncard_univ, Set.two_lt_ncard_iff]
  rintro ⟨a, b, c, _, _, _, hab, hac, hbc⟩
  apply hbc
  simp_rw [Perm.ext_iff] at h
  simpa [swap_apply_of_ne_of_ne hab hac] using h (swap a b) (swap b c) a
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
rintro : ∀ (h : ∀ (a b : Perm α), a * b = b * a), Nat.card α ≤ 2
rintro₁ :
  ∀ (h : ∀ (a b : Perm α), a * b = b * a),
    ¬∃ (a : α) (b : α) (c : α),
        Membership.mem (γ := Set α) _root_.Set.univ a ∧
          Membership.mem (γ := Set α) _root_.Set.univ b ∧
            Membership.mem (γ := Set α) _root_.Set.univ c ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
rintro₂ :
  ∀ (h : ∀ (a b : Perm α), a * b = b * a) (a b c : α),
    Membership.mem (γ := Set α) _root_.Set.univ a →
      Membership.mem (γ := Set α) _root_.Set.univ b →
        Membership.mem (γ := Set α) _root_.Set.univ c → ∀ (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c), False
⊢ IsMulCommutative.{u_1} (Perm α) → Nat.card α ≤ 2
have rintro₃ : ∀ (h : ∀ (a b : Perm α), a * b = b * a) (a b c : α),
  Membership.mem (γ := Set α) _root_.Set.univ a →
    Membership.mem (γ := Set α) _root_.Set.univ b →
      Membership.mem (γ := Set α) _root_.Set.univ c → ∀ (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c), b = c
Tactic: classical
  rintro ⟨⟨h⟩⟩
  rw [← not_lt, ← Set.ncard_univ, Set.two_lt_ncard_iff]
  rintro ⟨a, b, c, _, _, _, hab, hac, hbc⟩
  apply hbc
  simp_rw [Perm.ext_iff] at h
  simpa [swap_apply_of_ne_of_ne hab hac] using h (swap a b) (swap b c) a
-- Lean 4 proof step from Mathlib.Data.Finite.Perm (goal)
Goal:
α : Type u_1
inst : Finite α
rintro : ∀ (h : ∀ (a b : Perm α), a * b = b * a), Nat.card α ≤ 2
rintro₁ :
  ∀ (h : ∀ (a b : Perm α), a * b = b * a),
    ¬∃ (a : α) (b : α) (c : α),
        Membership.mem (γ := Set α) _root_.Set.univ a ∧
          Membership.mem (γ := Set α) _root_.Set.univ b ∧
            Membership.mem (γ := Set α) _root_.Set.univ c ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
rintro₂ :
  ∀ (h : ∀ (a b : Perm α), a * b = b * a) (a b c : α),
    Membership.mem (γ := Set α) _root_.Set.univ a →
      Membership.mem (γ := Set α) _root_.Set.univ b →
        Membership.mem (γ := Set α) _root_.Set.univ c → ∀ (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c), False
rintro₃ :
  ∀ (h : ∀ (a b : Perm α), a * b = b * a) (a b c : α),
    Membership.mem (γ := Set α) _root_.Set.univ a →
      Membership.mem (γ := Set α) _root_.Set.univ b →
        Membership.mem (γ := Set α) _root_.Set.univ c → ∀ (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c), b = c
⊢ IsMulCommutative.{u_1} (Perm α) → Nat.card α ≤ 2
have rintro₄ : ∀ (a b c : α),
  Membership.mem (γ := Set α) _root_.Set.univ a →
    Membership.mem (γ := Set α) _root_.Set.univ b →
      Membership.mem (γ := Set α) _root_.Set.univ c →
        ∀ (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
          (h : ∀ (a b : Perm α) (x : α), Eq (α := α) ((a * b : (a : α) → α) x : α) ((b * a : (a : α) → α) x : α)), b = c
Tactic: classical
  rintro ⟨⟨h⟩⟩
  rw [← not_lt, ← Set.ncard_univ, Set.two_lt_ncard_iff]
  rintro ⟨a, b, c, _, _, _, hab, hac, hbc⟩
  apply hbc
  simp_rw [Perm.ext_iff] at h
  simpa [swap_apply_of_ne_of_ne hab hac] using h (swap a b) (swap b c) a
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
⊢ Finite (α × β)
have haveI : ∀ (this : Fintype α), Finite (α × β)
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this : Fintype α
⊢ Finite (α × β)
have haveI : ∀ (this : Fintype β), Finite (α × β)
Tactic: haveI := Fintype.ofFinite β
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : α → Sort u_4
inst : Finite α
inst_1 : ∀ (a : α), Finite.{u_4} (β a)
⊢ Finite ((a : α) → β a)
have haveI : ∀ (this : Fintype (PLift α)), Finite ((a : α) → β a)
Tactic: haveI := Fintype.ofFinite (PLift α)
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : α → Sort u_4
inst : Finite α
inst_1 : ∀ (a : α), Finite.{u_4} (β a)
this : Fintype (PLift α)
⊢ Finite ((a : α) → β a)
have haveI : ∀ (this : (a : α) → Fintype (PLift (β a))), Finite ((a : α) → β a)
Tactic: haveI := fun a => Fintype.ofFinite (PLift (β a))
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : α → Sort u_4
inst : Finite α
inst_1 : ∀ (a : α), Finite.{u_4} (β a)
⊢ Finite ((a : α) → β a)
have haveI : ∀ (this : Fintype (PLift α)), Finite ((a : α) → β a)
Tactic: classical
  haveI := Fintype.ofFinite (PLift α)
  haveI := fun a => Fintype.ofFinite (PLift (β a))
  exact
    Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a)))
      (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : α → Sort u_4
inst : Finite α
inst_1 : ∀ (a : α), Finite.{u_4} (β a)
haveI haveI₁ haveI₂ : ∀ (this : Fintype (PLift α)), Finite ((a : α) → β a)
⊢ Finite ((a : α) → β a)
have haveI₃ : ∀ (this : Fintype (PLift α)) (this : (a : α) → Fintype (PLift (β a))), Finite ((a : α) → β a)
Tactic: classical
  haveI := Fintype.ofFinite (PLift α)
  haveI := fun a => Fintype.ofFinite (PLift (β a))
  exact
    Finite.of_equiv (∀ a : PLift α, PLift (β (Equiv.plift a)))
      (Equiv.piCongr Equiv.plift fun _ => Equiv.plift)
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
⊢ Finite (α ↪ β)
have inl : IsEmpty (α ↪ β) → Finite (α ↪ β)
Tactic: rcases isEmpty_or_nonempty (α ↪ β) with _ | h
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
inl : IsEmpty (α ↪ β) → Finite (α ↪ β)
⊢ Finite (α ↪ β)
have inr : ∀ (h : Nonempty (α ↪ β)), Finite (α ↪ β)
Tactic: rcases isEmpty_or_nonempty (α ↪ β) with _ | h
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
h : Nonempty (α ↪ β)
⊢ Finite (α ↪ β)
have inr : ∀ (f : α ↪ β), Finite (α ↪ β)
Tactic: refine h.elim fun f => ?_
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (hypothesis)
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Sort u_3
β : Sort u_4
inst : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
⊢ Finite (α ↪ β)
have this : Finite α
Tactic: haveI : Finite α := Finite.of_injective _ f.injective
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype (↑s : Type u_1)
ht : Fintype (↑t : Type u_2)
⊢ Fintype (↑(image2 f s t) : Type u_3)
have rw : Fintype (↑((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t) : Type u_3)
Tactic: rw [← image_prod]
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst : Finite.{u_1 + 1} (↑s : Type u_1)
inst_1 : Finite.{u_2 + 1} (↑t : Type u_2)
⊢ Finite.{u_3 + 1} (↑(image2 f s t) : Type u_3)
have rw : Finite.{u_3 + 1} (↑((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t) : Type u_3)
Tactic: rw [← image_prod]
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
⊢ (s ×ˢ t).Finite
have this : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ (s ×ˢ t).Finite
have this₁ : Finite.{u_2 + 1} (↑t : Type u_2)
Tactic: have := ht.to_subtype
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
have refine_1 : ∀ (h : (s ×ˢ t).Infinite), s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
refine_1 : ∀ (h : (s ×ˢ t).Infinite), s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
have refine_2 : s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
have refine_1 : ¬(t.Nonempty → s.Finite) ∨ ¬(s.Nonempty → t.Finite)
Tactic: simp_rw [Set.Infinite, @and_comm ¬_, ← Classical.not_imp]
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ ¬(t.Nonempty → s.Finite) ∨ ¬(s.Nonempty → t.Finite)
have refine_1 : ∀ (this : (t.Nonempty → s.Finite) ∧ (s.Nonempty → t.Finite)), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)
have contrapose! : (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
Tactic: contrapose! +distrib
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
⊢ (image2 f s t).Finite
have this : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ (image2 f s t).Finite
have this₁ : Finite.{u_2 + 1} (↑t : Type u_2)
Tactic: have := ht.to_subtype
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
have refine_1 : ∀ (h : (image2 f s t).Infinite), (s ×ˢ t).Infinite
Tactic: refine ⟨fun h => Set.infinite_prod.1 ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
refine_1 : ∀ (h : (image2 f s t).Infinite), (s ×ˢ t).Infinite
⊢ (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
have refine_2 : s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite
Tactic: refine ⟨fun h => Set.infinite_prod.1 ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (image2 f s t).Infinite
⊢ (s ×ˢ t).Infinite
have h₁ : (uncurry f '' s ×ˢ t).Infinite
Tactic: rw [← image_uncurry_prod] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (x : α) ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
have contrapose! : (image2 f s t).Infinite ↔ (s.Infinite ∨ t.Infinite) ∧ s.Nonempty ∧ t.Nonempty
Tactic: contrapose! +distrib
-- Lean 4 proof step from Mathlib.Data.Finite.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn.{u_1, u_3} (β := γ) (fun (x : α) ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Infinite ↔ (s.Infinite ∨ t.Infinite) ∧ s.Nonempty ∧ t.Nonempty
have rw : s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty ↔ (s.Infinite ∨ t.Infinite) ∧ s.Nonempty ∧ t.Nonempty
Tactic: rw [Set.infinite_image2 hfs hft]
-- Lean 4 proof step from Mathlib.Data.Finite.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
⊢ Finite (α ⊕ β)
have haveI : ∀ (this : Fintype α), Finite (α ⊕ β)
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this : Fintype α
⊢ Finite (α ⊕ β)
have haveI : ∀ (this : Fintype β), Finite (α ⊕ β)
Tactic: haveI := Fintype.ofFinite β
-- Lean 4 proof step from Mathlib.Data.Finite.Vector (goal)
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Finite.{u_1 + 1} (Vector α n)
have haveI : ∀ (this : Fintype α), Finite.{u_1 + 1} (Vector α n)
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Vector (goal)
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Finite.{u_1 + 1} (Sym α n)
have haveI : ∀ (this : Fintype α), Finite.{u_1 + 1} (Sym α n)
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Vector (goal)
Goal:
α : Type u_1
inst : Finite α
n : ℕ
⊢ Finite.{u_1 + 1} (Sym α n)
have haveI : ∀ (this : Fintype α), Finite.{u_1 + 1} (Sym α n)
Tactic: classical
  haveI := Fintype.ofFinite α
  infer_instance
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
⊢ m.keys (β := fun (a : α) ↦ β a).Nodup ↔ m.NodupKeys (β := fun (a : α) ↦ β a)
have mk : ∀ (l : List ((a : α) × β a)),
  (keys (β := fun (a : α) ↦ β a)
        (Quot.mk (⇑(isSetoid ((a : α) × β a)) : List ((a : α) × β a) → List ((a : α) × β a) → Prop) l)).Nodup ↔
    NodupKeys (β := fun (a : α) ↦ β a)
      (Quot.mk (⇑(isSetoid ((a : α) × β a)) : List ((a : α) × β a) → List ((a : α) × β a) → Prop) l)
Tactic: rcases m with ⟨l⟩
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
s₁ s₂ : AList β
⊢ s₁.toFinmap (β := β) = s₂.toFinmap (β := β) ↔ s₁.entries (β := β) ~ s₂.entries (β := β)
have mk : ∀ (entries : List (Sigma β)) (nodupKeys : entries.NodupKeys (β := β)),
  (mk (β := β) entries nodupKeys).toFinmap (β := β) = s₂.toFinmap (β := β) ↔
    (mk (β := β) entries nodupKeys).entries (β := β) ~ s₂.entries (β := β)
Tactic: cases s₁
Cleared hypotheses: s₁
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
s₂ : AList β
entries : List (Sigma β)
nodupKeys : entries.NodupKeys (β := β)
⊢ (mk (β := β) entries nodupKeys).toFinmap (β := β) = s₂.toFinmap (β := β) ↔
    (mk (β := β) entries nodupKeys).entries (β := β) ~ s₂.entries (β := β)
have mk : ∀ (entries_1 : List (Sigma β)) (nodupKeys_1 : entries_1.NodupKeys (β := β)),
  (mk (β := β) entries nodupKeys).toFinmap (β := β) = (mk (β := β) entries_1 nodupKeys_1).toFinmap (β := β) ↔
    (mk (β := β) entries nodupKeys).entries (β := β) ~ (mk (β := β) entries_1 nodupKeys_1).entries (β := β)
Tactic: cases s₂
Cleared hypotheses: s₂
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
⊢ γ
have refine_1 : ∀ (l₁ l₂ : List (Sigma β)) (p : l₁ ≈ l₂)
  (h₁ :
    Part.Dom.{u_1} (α := γ)
      ((fun (l : List (Sigma β)) ↦
          ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
            Part γ))
        l₁))
  (h₂ :
    Part.Dom.{u_1} (α := γ)
      ((fun (l : List (Sigma β)) ↦
          ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
            Part γ))
        l₂)),
  Part.get
      ((fun (l : List (Sigma β)) ↦
          ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
            Part γ))
        l₁)
      h₁ =
    Part.get
      ((fun (l : List (Sigma β)) ↦
          ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
            Part γ))
        l₂)
      h₂
Tactic: refine
    (Quotient.liftOn s.entries
      (fun (l : List (Sigma β)) => (⟨_, fun nd => f ⟨l, nd⟩⟩ : Part γ))
      (fun l₁ l₂ p => Part.ext' (perm_nodupKeys p) ?_) : Part γ).get ?_