awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.SetLike.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : PartialOrder A
inst_2 : IsConcreteLE A B
S T : A
rw : (↑S : Set B) ⊆ (↑T : Set B) ∧ (↑S : Set B) ≠ (↑T : Set B) ↔ S < T
rw₁ : (↑S : Set B) ⊆ (↑T : Set B) ∧ (↑S : Set B) ≠ (↑T : Set B) ↔ S ≤ T ∧ S ≠ T
rw₂ : S ≤ T ∧ (↑S : Set B) ≠ (↑T : Set B) ↔ S ≤ T ∧ S ≠ T
⊢ (↑S : Set B) ⊂ (↑T : Set B) ↔ S < T
have rw₃ : S ≤ T ∧ S ≠ T ↔ S ≤ T ∧ S ≠ T
Tactic: rw [ssubset_iff_subset_ne, lt_iff_le_and_ne, coe_subset_coe, SetLike.coe_ne_coe]
-- Lean 4 proof step from Mathlib.Data.SetLike.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : PartialOrder A
inst_2 : IsConcreteLE A B
p q : A
⊢ p < q ↔ p ≤ q ∧ ∃ (x : B), x ∈ q ∧ ¬x ∈ p
have rw : p ≤ q ∧ ¬q ≤ p ↔ p ≤ q ∧ ∃ (x : B), x ∈ q ∧ ¬x ∈ p
Tactic: rw [lt_iff_le_not_ge, not_le_iff_exists]
-- Lean 4 proof step from Mathlib.Data.SetLike.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : PartialOrder A
inst_2 : IsConcreteLE A B
p q : A
rw : p ≤ q ∧ ¬q ≤ p ↔ p ≤ q ∧ ∃ (x : B), x ∈ q ∧ ¬x ∈ p
⊢ p < q ↔ p ≤ q ∧ ∃ (x : B), x ∈ q ∧ ¬x ∈ p
have rw₁ : (p ≤ q ∧ ∃ (x : B), x ∈ q ∧ ¬x ∈ p) ↔ p ≤ q ∧ ∃ (x : B), x ∈ q ∧ ¬x ∈ p
Tactic: rw [lt_iff_le_not_ge, not_le_iff_exists]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
q : Prod.{u_1, u_2} (Quotient r) (Quotient s)
⊢ (fun (q : Quotient (r.prod s)) ↦
        (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
          Prod.{u_1, u_2} (Quotient r) (Quotient s)))
      ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
          (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
            | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
            Quotient (r.prod s)))
        q) =
    q
have rcases : ∀ (qa : Quotient r) (qb : Quotient s),
  (fun (q : Quotient (r.prod s)) ↦
        (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) sorry :
          Prod.{u_1, u_2} (Quotient r) (Quotient s)))
      ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
          (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
            | (x, y) => Quotient.map₂ Prod.mk sorry x y :
            Quotient (r.prod s)))
        (qa, qb)) =
    (qa, qb)
Tactic: rcases q with ⟨qa, qb⟩
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
qa : Quotient r
qb : Quotient s
⊢ (fun (q : Quotient (r.prod s)) ↦
        (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
          Prod.{u_1, u_2} (Quotient r) (Quotient s)))
      ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
          (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
            | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
            Quotient (r.prod s)))
        (qa, qb)) =
    (qa, qb)
have h : ∀ (a₁ : α) (a₂ : β),
  Eq (α := Prod.{u_1, u_2} (Quotient r) (Quotient s))
    ((fun (q : Quotient (r.prod s)) ↦
        (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) sorry :
          Prod.{u_1, u_2} (Quotient r) (Quotient s)))
      ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
          (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
            | (x, y) => Quotient.map₂ Prod.mk sorry x y :
            Quotient (r.prod s)))
        (Quotient.mk'' a₁, Quotient.mk'' a₂)))
    (Quotient.mk'' a₁, Quotient.mk'' a₂)
Tactic: induction qa, qb using Quotient.inductionOn₂'
Cleared hypotheses: qa, qb
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
⊢ (fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
        (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
          | (x, y) => Quotient.map₂ Prod.mk ⋯ x y :
          Quotient (r.prod s)))
      ((fun (q : Quotient (r.prod s)) ↦
          (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯ :
            Prod.{u_1, u_2} (Quotient r) (Quotient s)))
        q) =
    q
have h : ∀ (a : α × β),
  Eq (α := Quotient (r.prod s))
    ((fun (x : Prod.{u_1, u_2} (Quotient r) (Quotient s)) ↦
        (match (motive := Prod.{u_1, u_2} (Quotient r) (Quotient s) → Quotient (r.prod s)) x with
          | (x, y) => Quotient.map₂ Prod.mk sorry x y :
          Quotient (r.prod s)))
      ((fun (q : Quotient (r.prod s)) ↦
          (q.liftOn' (fun (xy : α × β) ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) sorry :
            Prod.{u_1, u_2} (Quotient r) (Quotient s)))
        (Quotient.mk'' a)))
    (Quotient.mk'' a)
Tactic: induction q using Quotient.inductionOn'
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))
x y : (i : ι) → α i
hxy : (piSetoid : ((i : ι) → α i) → ((i : ι) → α i) → Prop) x y
⊢ Eq (α := (i : ι) → Quotient (r i)) ((fun (x : (i : ι) → α i) (i : ι) ↦ (Quotient.mk'' (x i) : Quotient (r i))) x)
    ((fun (x : (i : ι) → α i) (i : ι) ↦ (Quotient.mk'' (x i) : Quotient (r i))) y)
have h : ∀ (i : ι),
  Eq.{u_4} (α := Quotient (r i)) ((fun (x : (i : ι) → α i) (i : ι) ↦ (Quotient.mk'' (x i) : Quotient (r i))) x i)
    ((fun (x : (i : ι) → α i) (i : ι) ↦ (Quotient.mk'' (x i) : Quotient (r i))) y i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
q : (i : ι) → Quotient (r i)
⊢ (fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
        (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) ⋯ : (i : ι) → Quotient (r i)))
      ((fun (x : (i : ι) → Quotient (r i)) ↦
          (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        q) =
    q
have h : ∀ (i : ι),
  (fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
        (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) sorry : (i : ι) → Quotient (r i)))
      ((fun (x : (i : ι) → Quotient (r i)) ↦
          (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
        q)
      i =
    q i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))
⊢ (fun (x : (i : ι) → Quotient (r i)) ↦
        (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      ((fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
          (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) ⋯ : (i : ι) → Quotient (r i)))
        q) =
    q
have h : ∀ (a : (i : ι) → α i),
  Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    ((fun (x : (i : ι) → Quotient (r i)) ↦
        (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      ((fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
          (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) sorry : (i : ι) → Quotient (r i)))
        (Quotient.mk'' a)))
    (Quotient.mk'' a)
Tactic: induction q using Quotient.inductionOn'
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
a : (i : ι) → α i
⊢ Eq (α := Quotient (α := (i : ι) → α i) (piSetoid (α := α)))
    ((fun (x : (i : ι) → Quotient (r i)) ↦
        (Quotient.mk'' fun (i : ι) ↦ (x i).out : Quotient (α := (i : ι) → α i) (piSetoid (α := α))))
      ((fun (q : Quotient (α := (i : ι) → α i) (piSetoid (α := α))) ↦
          (q.liftOn' (fun (x : (i : ι) → α i) (i : ι) ↦ Quotient.mk'' (x i)) ⋯ : (i : ι) → Quotient (r i)))
        (Quotient.mk'' a)))
    (Quotient.mk'' a)
have h : (piSetoid : ((i : ι) → α i) → ((i : ι) → α i) → Prop) (fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) a
Tactic: simp only [Quotient.liftOn'_mk'', Quotient.eq'']
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
a : (i : ι) → α i
i : ι
⊢ (fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) i ≈ a i
have h : (r i : α i → α i → Prop) ((fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) i) (a i)
Tactic: change Setoid.r _ _
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
ι : Sort u_3
α : ι → Sort u_4
r : (i : ι) → Setoid.{u_4} (α i)
a : (i : ι) → α i
i : ι
⊢ (r i : α i → α i → Prop) ((fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) i) (a i)
have h : Eq (α := Quotient (r i)) (Quotient.mk'' ((fun (i : ι) ↦ Quotient.out (s := r i) (Quotient.mk'' (a i))) i))
  (Quotient.mk'' (a i))
Tactic: rw [← Quotient.eq'']
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
s : Set (Setoid α)
⊢ (⇑(sInf s) : α → α → Prop) = sInf (@r α '' s)
have h : ∀ (x x_1 : α), (sInf s : α → α → Prop) x x_1 ↔ sInf (@r α '' s) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
s : Set (Setoid α)
x x_1 : α
⊢ (sInf s : α → α → Prop) x x_1 ↔ sInf (@r α '' s) x x_1
have h : (sInf s : α → α → Prop) x x_1 ↔ ∀ (i : Setoid α) (i_1 : i ∈ s), (i : α → α → Prop) x x_1
Tactic: simp only [sInf_image, iInf_apply, iInf_Prop_eq]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
s : Setoid α
⊢ s = ⊤ ↔ ∀ (x y : α), (s : α → α → Prop) x y
have rw : (∀ {x y : α}, ⊤ x y → (s : α → α → Prop) x y) ↔ ∀ (x y : α), (s : α → α → Prop) x y
Tactic: rw [_root_.eq_top_iff, Setoid.le_def, Setoid.top_def]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
r s : Setoid α
⊢ r ⊔ s = EqvGen.setoid fun (x y : α) ↦ (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y
have rw : r ⊔ s = sInf {s_1 : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y → (s_1 : α → α → Prop) x y}
Tactic: rw [eqvGen_eq]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
r s : Setoid α
⊢ r ⊔ s =
    sInf {s_1 : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y → (s_1 : α → α → Prop) x y}
have apply : Eq.{u_1 + 1} (α := Set (Setoid α)) {x : Setoid α | r ≤ x ∧ s ≤ x}
  {s_1 : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y → (s_1 : α → α → Prop) x y}
Tactic: apply congr_arg sInf
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
r s : Setoid α
⊢ r ⊔ s = EqvGen.setoid ((⇑r : α → α → Prop) ⊔ (⇑s : α → α → Prop))
have rw : Eq.{u_1 + 1} (α := Setoid α) (EqvGen.setoid fun (x y : α) ↦ (r : α → α → Prop) x y ∨ (s : α → α → Prop) x y)
  (EqvGen.setoid ((⇑r : α → α → Prop) ⊔ (⇑s : α → α → Prop)))
Tactic: rw [sup_eq_eqvGen]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
S : Set (Setoid α)
⊢ sSup S = EqvGen.setoid fun (x y : α) ↦ ∃ r ∈ S, (r : α → α → Prop) x y
have rw : sSup S = sInf {s : Setoid α | ∀ ⦃x y : α⦄, (∃ r ∈ S, (r : α → α → Prop) x y) → (s : α → α → Prop) x y}
Tactic: rw [eqvGen_eq]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
S : Set (Setoid α)
⊢ sSup S = sInf {s : Setoid α | ∀ ⦃x y : α⦄, (∃ r ∈ S, (r : α → α → Prop) x y) → (s : α → α → Prop) x y}
have apply : upperBounds S = {s : Setoid α | ∀ ⦃x y : α⦄, (∃ r ∈ S, (r : α → α → Prop) x y) → (s : α → α → Prop) x y}
Tactic: apply congr_arg sInf
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
S : Set (Setoid α)
⊢ upperBounds S = {s : Setoid α | ∀ ⦃x y : α⦄, (∃ r ∈ S, (r : α → α → Prop) x y) → (s : α → α → Prop) x y}
have simp : Eq.{u_1 + 1} (α := Set (Setoid α))
  {x : Setoid α | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, (a : α → α → Prop) x_1 y → (x : α → α → Prop) x_1 y}
  {s : Setoid α | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, (x_1 : α → α → Prop) x y → (s : α → α → Prop) x y}
Tactic: simp only [upperBounds, le_def, and_imp, exists_imp]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
S : Set (Setoid α)
⊢ Eq.{u_1 + 1} (α := Set (Setoid α))
    {x : Setoid α | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, (a : α → α → Prop) x_1 y → (x : α → α → Prop) x_1 y}
    {s : Setoid α | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, (x_1 : α → α → Prop) x y → (s : α → α → Prop) x y}
have h : ∀ (x : Setoid α),
  Membership.mem (γ := Set (Setoid α))
      {x : Setoid α | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, (a : α → α → Prop) x_1 y → (x : α → α → Prop) x_1 y} x ↔
    Membership.mem (γ := Set (Setoid α))
      {s : Setoid α | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, (x_1 : α → α → Prop) x y → (s : α → α → Prop) x y} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
s : Set (Setoid α)
⊢ sSup s = EqvGen.setoid (sSup (@r α '' s))
have rw : Eq.{u_1 + 1} (α := Setoid α) (EqvGen.setoid fun (x y : α) ↦ ∃ r ∈ s, (r : α → α → Prop) x y)
  (EqvGen.setoid (⨆ a ∈ s, (⇑a : α → α → Prop)))
Tactic: rw [sSup_eq_eqvGen, sSup_image]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
s : Set (Setoid α)
⊢ Eq.{u_1 + 1} (α := Setoid α) (EqvGen.setoid fun (x y : α) ↦ ∃ r ∈ s, (r : α → α → Prop) x y)
    (EqvGen.setoid (⨆ a ∈ s, (⇑a : α → α → Prop)))
have e_r : ∀ (x y : α), (∃ r ∈ s, (r : α → α → Prop) x y) ↔ (⨆ a ∈ s, (⇑a : α → α → Prop)) x y
Tactic: congr with (x y)
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
r : Setoid α
⊢ EqvGen.setoid (⇑r : α → α → Prop) ≤ r
have rw : sInf {s : Setoid α | ∀ ⦃x y : α⦄, (r : α → α → Prop) x y → (s : α → α → Prop) x y} ≤ r
Tactic: rw [eqvGen_eq]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → (s : α → α → Prop) x y
⊢ EqvGen.setoid r ≤ s
have rw : sInf {s : Setoid α | ∀ ⦃x y : α⦄, r x y → (s : α → α → Prop) x y} ≤ s
Tactic: rw [eqvGen_eq]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
⊢ Quotient.lift f H = g
have h : ∀ (x : Quotient r) (x : α), Quotient.lift f H (Quot.mk (⇑r : α → α → Prop) x) = g (Quot.mk (⇑r : α → α → Prop) x)
Tactic: ext ⟨x⟩
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x_1 : Quotient r
x : α
⊢ Quotient.lift f H (Quot.mk (⇑r : α → α → Prop) x) = g (Quot.mk (⇑r : α → α → Prop) x)
have h : Quotient.lift f H ⟦x⟧ = g ⟦x⟧
Tactic: rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x_1 : Quotient r
x : α
h : Quotient.lift f H ⟦x⟧ = g ⟦x⟧
⊢ Quotient.lift f H (Quot.mk (⇑r : α → α → Prop) x) = g (Quot.mk (⇑r : α → α → Prop) x)
have h₁ : f x = g ⟦x⟧
Tactic: rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x_1 : Quotient r
x : α
h : Quotient.lift f H ⟦x⟧ = g ⟦x⟧
h₁ : f x = g ⟦x⟧
⊢ Quotient.lift f H (Quot.mk (⇑r : α → α → Prop) x) = g (Quot.mk (⇑r : α → α → Prop) x)
have h₂ : (g ∘ Quotient.mk'') x = g ⟦x⟧
Tactic: rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x_1 : Quotient r
x : α
h : Quotient.lift f H ⟦x⟧ = g ⟦x⟧
h₁ : f x = g ⟦x⟧
h₂ : (g ∘ Quotient.mk'') x = g ⟦x⟧
⊢ Quotient.lift f H (Quot.mk (⇑r : α → α → Prop) x) = g (Quot.mk (⇑r : α → α → Prop) x)
have h₃ : g (Quotient.mk'' x) = g ⟦x⟧
Tactic: rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x_1 : Quotient r
x : α
h : Quotient.lift f H ⟦x⟧ = g ⟦x⟧
h₁ : f x = g ⟦x⟧
h₂ : (g ∘ Quotient.mk'') x = g ⟦x⟧
h₃ : g (Quotient.mk'' x) = g ⟦x⟧
⊢ Quotient.lift f H (Quot.mk (⇑r : α → α → Prop) x) = g (Quot.mk (⇑r : α → α → Prop) x)
have h₄ : g ⟦x⟧ = g ⟦x⟧
Tactic: rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ r.map f = r.mapOfSurjective f h hf
have rw : r.map f = Relation.EqvGen.setoid (⇑(r.mapOfSurjective f h hf) : β → β → Prop)
Tactic: rw [← eqvGen_of_setoid (mapOfSurjective r f h hf)]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid β
x y : α
⊢ (comap f r : α → α → Prop) x y ↔ ⟦f x⟧ = ⟦f y⟧
have rw : (comap f r : α → α → Prop) x y ↔ (r : β → β → Prop) (f x) (f y)
Tactic: rw [Quotient.eq]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r_1 : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : (r : α → α → Prop) x y
⊢ (comap Quotient.mk' s : α → α → Prop) x y
have rw : (s : Quotient r → Quotient r → Prop) (Quotient.mk' x) (Quotient.mk' y)
Tactic: rw [comap_rel, Quotient.eq'.2 h]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
r_1 : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : (r : α → α → Prop) x y
rw : (s : Quotient r → Quotient r → Prop) (Quotient.mk' x) (Quotient.mk' y)
⊢ (comap Quotient.mk' s : α → α → Prop) x y
have rw₁ : (s : Quotient r → Quotient r → Prop) (Quotient.mk' y) (Quotient.mk' y)
Tactic: rw [comap_rel, Quotient.eq'.2 h]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
s : Setoid α
⊢ Subsingleton.{u_1 + 1} (Quotient s) ↔ s = ⊤
have simp : (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → (s : α → α → Prop) x y
Tactic: simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
s : Setoid α
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → (s : α → α → Prop) x y
have refine : ∀ (a : α), (∀ (y : Quotient s), Quotient.mk' a = y) ↔ ∀ {y : α}, ⊤ → (s : α → α → Prop) a y
Tactic: refine Quotient.mk'_surjective.forall.trans (forall_congr' fun a => ?_)
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
s : Setoid α
a : α
⊢ (∀ (y : Quotient s), Quotient.mk' a = y) ↔ ∀ {y : α}, ⊤ → (s : α → α → Prop) a y
have refine : ∀ (b : α), Eq (α := Quotient s) (Quotient.mk' a) (Quotient.mk' b) ↔ ⊤ → (s : α → α → Prop) a b
Tactic: refine Quotient.mk'_surjective.forall.trans (forall_congr' fun b => ?_)
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
s : Setoid α
a b : α
⊢ Eq (α := Quotient s) (Quotient.mk' a) (Quotient.mk' b) ↔ ⊤ → (s : α → α → Prop) a b
have simp_rw : Eq (α := Quotient s) (Quotient.mk' a) (Quotient.mk' b) ↔ True → (s : α → α → Prop) a b
Tactic: simp_rw [Prop.top_eq_true, true_implies, Quotient.eq']
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
s : Setoid α
a b : α
simp_rw : Eq (α := Quotient s) (Quotient.mk' a) (Quotient.mk' b) ↔ True → (s : α → α → Prop) a b
⊢ Eq (α := Quotient s) (Quotient.mk' a) (Quotient.mk' b) ↔ ⊤ → (s : α → α → Prop) a b
have simp_rw₁ : Eq (α := Quotient s) (Quotient.mk' a) (Quotient.mk' b) ↔ (s : α → α → Prop) a b
Tactic: simp_rw [Prop.top_eq_true, true_implies, Quotient.eq']
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
r : α → α → Prop
⊢ Subsingleton.{u_1 + 1} (Quot r) ↔ Relation.EqvGen r = ⊤
have simp : (∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ Relation.EqvGen r i i_1
Tactic: simp only [_root_.subsingleton_iff, _root_.eq_top_iff, Pi.le_def, Pi.top_apply]
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
r : α → α → Prop
⊢ (∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ Relation.EqvGen r i i_1
have refine : ∀ (a : α), (∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ Relation.EqvGen r a i
Tactic: refine Quot.mk_surjective.forall.trans (forall_congr' fun a => ?_)
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
r : α → α → Prop
a : α
⊢ (∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ Relation.EqvGen r a i
have refine : ∀ (b : α), mk r a = mk r b ↔ ⊤ ≤ Relation.EqvGen r a b
Tactic: refine Quot.mk_surjective.forall.trans (forall_congr' fun b => ?_)
-- Lean 4 proof step from Mathlib.Data.Setoid.Basic (goal)
Goal:
α : Type u_1
r : α → α → Prop
a b : α
⊢ mk r a = mk r b ↔ ⊤ ≤ Relation.EqvGen r a b
have rw : Relation.EqvGen r a b ↔ ⊤ ≤ Relation.EqvGen r a b
Tactic: rw [Quot.eq]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (hypothesis)
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
⊢ s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
have hst : ∀ (t : Set α), (s ∩ t).Finite
Tactic: have hst (t : Set α) : (s ∩ t).Finite := hs.inter_of_left t
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (hypothesis)
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
⊢ s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
have hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = sorry.toFinset (s := s ∩ t).card
Tactic: have hst' (t : Set α) : Nat.card ↑(s ∩ t) = (hst t).toFinset.card :=
    Nat.card_eq_card_finite_toFinset (hst t)
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
⊢ s.ncard = ∑ᶠ (t : (↑P : Type u_1)), (s ∩ (↑t : Set α)).ncard
have rw : s.ncard =
  ∑ i ∈ Set.Finite.toFinset (s := Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) hs',
    (s ∩ (↑i : Set α)).ncard
Tactic: rw [finsum_def, dif_pos hs']
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition.Card (goal)
Goal:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card.{u_1} (↑(s ∩ t) : Type u_1) = ⋯.toFinset (s := s ∩ t).card
hs' : Function.HasFiniteSupport (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard
⊢ s.ncard =
    ∑ i ∈ Set.Finite.toFinset (s := Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ (s ∩ (↑t : Set α)).ncard) hs',
      (s ∩ (↑i : Set α)).ncard
have simp : hs.toFinset (s := s).card =
  ∑
    t ∈
      Set.Finite.toFinset (s :=
        Function.support (M := ℕ) fun (t : (↑P : Type u_1)) ↦ Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1)) sorry,
    Nat.card.{u_1} (↑(s ∩ (↑t : Set α)) : Type u_1)
Tactic: simp only [← Nat.card_coe_set_eq, Nat.card_eq_card_finite_toFinset hs]