awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Part (hypothesis)
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : b ∈ x >>= f
⊢ b ∈ y
have h'₁ : ∃ (a : α), a ∈ x ∧ b ∈ f a
Tactic: simp only [bind_eq_bind, mem_bind_iff] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : ∃ (a : α), a ∈ x ∧ b ∈ f a
⊢ b ∈ y
have mpr : ∀ (a : α) (h₀ : a ∈ x) (h₁ : b ∈ f a), b ∈ y
Tactic: rcases h' with ⟨a, h₀, h₁⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ a ∈ restrict p o h ↔ p ∧ a ∈ o
have dsimp : (∃ (h_1 : p), o.get sorry = a) ↔ p ∧ ∃ (h : o.Dom), o.get h = a
Tactic: dsimp [restrict, mem_eq]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ (h_1 : p), o.get ⋯ = a) ↔ p ∧ ∃ (h : o.Dom), o.get h = a
have mp : (∃ (h_1 : p), o.get sorry = a) → p ∧ ∃ (h : o.Dom), o.get h = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
mp : (∃ (h_1 : p), o.get ⋯ = a) → p ∧ ∃ (h : o.Dom), o.get h = a
⊢ (∃ (h_1 : p), o.get ⋯ = a) ↔ p ∧ ∃ (h : o.Dom), o.get h = a
have mpr : (p ∧ ∃ (h : o.Dom), o.get h = a) → ∃ (h_1 : p), o.get sorry = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = ma * mb
have simp : (a * b).get sorry = a.get sorry * b.get sorry
Tactic: simp only [← ha.2, ← hb.2]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ma⁻¹ ∈ a⁻¹
have simp : ∃ (a_1 : α), a_1 ∈ a ∧ a_1⁻¹ = ma⁻¹
Tactic: simp [inv_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma / mb ∈ a / b
have simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 / a = ma / mb
Tactic: simp [div_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Div α
a b : Part α
hab : (a / b).Dom
⊢ (a / b).get hab = a.get ⋯ / b.get ⋯
have simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y / x) b) sorry = a.get sorry / b.get sorry
Tactic: simp [div_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma % mb ∈ a % b
have simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 % a = ma % mb
Tactic: simp [mod_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Mod α
a b : Part α
hab : (a % b).Dom
⊢ (a % b).get hab = a.get ⋯ % b.get ⋯
have simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y % x) b) sorry = a.get sorry % b.get sorry
Tactic: simp [mod_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ++ mb ∈ a ++ b
have simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 ++ a = ma ++ mb
Tactic: simp [append_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ (a ++ b).get hab = a.get ⋯ ++ b.get ⋯
have simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y ++ x) b) sorry = a.get sorry ++ b.get sorry
Tactic: simp [append_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∩ mb ∈ a ∩ b
have simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 ∩ a = ma ∩ mb
Tactic: simp [inter_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ (a ∩ b).get hab = a.get ⋯ ∩ b.get ⋯
have simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y ∩ x) b) sorry = a.get sorry ∩ b.get sorry
Tactic: simp [inter_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∪ mb ∈ a ∪ b
have simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 ∪ a = ma ∪ mb
Tactic: simp [union_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ (a ∪ b).get hab = a.get ⋯ ∪ b.get ⋯
have simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y ∪ x) b) sorry = a.get sorry ∪ b.get sorry
Tactic: simp [union_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma \ mb ∈ a \ b
have simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 \ a = ma \ mb
Tactic: simp [sdiff_def]
-- Lean 4 proof step from Mathlib.Data.Part (goal)
Goal:
α : Type u_1
inst : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a \ b).get hab = a.get ⋯ \ b.get ⋯
have simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y \ x) b) sorry = a.get sorry \ b.get sorry
Tactic: simp [sdiff_def]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b x : (i : ι) → α i
simp_rw simp_rw₁ :
  Membership.mem (γ := Finset ((i : ι) → α i)) (piFinset (δ := α) fun (i : ι) ↦ Icc (a i) (b i)) x ↔ a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset ((i : ι) → α i))
      ((fun (a b : (i : ι) → α i) ↦ (piFinset (δ := α) fun (i : ι) ↦ Icc (a i) (b i) : Finset ((a : ι) → α a))) a b) x ↔
    a ≤ x ∧ x ≤ b
have simp_rw₂ : (∀ (a_1 : ι), x a_1 ∈ Icc (a a_1) (b a_1)) ↔ a ≤ x ∧ x ≤ b
Tactic: simp_rw [mem_piFinset, mem_Icc, le_def, forall_and]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b x : (i : ι) → α i
simp_rw simp_rw₁ :
  Membership.mem (γ := Finset ((i : ι) → α i)) (piFinset (δ := α) fun (i : ι) ↦ Icc (a i) (b i)) x ↔ a ≤ x ∧ x ≤ b
simp_rw₂ : (∀ (a_1 : ι), x a_1 ∈ Icc (a a_1) (b a_1)) ↔ a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset ((i : ι) → α i))
      ((fun (a b : (i : ι) → α i) ↦ (piFinset (δ := α) fun (i : ι) ↦ Icc (a i) (b i) : Finset ((a : ι) → α a))) a b) x ↔
    a ≤ x ∧ x ≤ b
have simp_rw₃ : (∀ (a_1 : ι), a a_1 ≤ x a_1 ∧ x a_1 ≤ b a_1) ↔ a ≤ x ∧ x ≤ b
Tactic: simp_rw [mem_piFinset, mem_Icc, le_def, forall_and]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b x : (i : ι) → α i
simp_rw simp_rw₁ :
  Membership.mem (γ := Finset ((i : ι) → α i)) (piFinset (δ := α) fun (i : ι) ↦ Icc (a i) (b i)) x ↔ a ≤ x ∧ x ≤ b
simp_rw₂ : (∀ (a_1 : ι), x a_1 ∈ Icc (a a_1) (b a_1)) ↔ a ≤ x ∧ x ≤ b
simp_rw₃ : (∀ (a_1 : ι), a a_1 ≤ x a_1 ∧ x a_1 ≤ b a_1) ↔ a ≤ x ∧ x ≤ b
⊢ Membership.mem (γ := Finset ((i : ι) → α i))
      ((fun (a b : (i : ι) → α i) ↦ (piFinset (δ := α) fun (i : ι) ↦ Icc (a i) (b i) : Finset ((a : ι) → α a))) a b) x ↔
    a ≤ x ∧ x ≤ b
have simp_rw₄ : (∀ (a_1 : ι), a a_1 ≤ x a_1 ∧ x a_1 ≤ b a_1) ↔ (∀ (i : ι), a i ≤ x i) ∧ ∀ (i : ι), x i ≤ b i
Tactic: simp_rw [mem_piFinset, mem_Icc, le_def, forall_and]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ico a b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
have rw : #(Icc a b) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
Tactic: rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
rw : #(Icc a b) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
⊢ #(Ico a b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
have rw₁ : HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
Tactic: rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ioc a b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
have rw : #(Icc a b) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
Tactic: rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
rw : #(Icc a b) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
⊢ #(Ioc a b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
have rw₁ : HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
Tactic: rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ioo a b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 2
have rw : #(Icc a b) - 2 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 2
Tactic: rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
rw : #(Icc a b) - 2 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 2
⊢ #(Ioo a b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 2
have rw₁ : HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 2 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 2
Tactic: rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderBot (α i)
b_1 b x : (i : ι) → α i
simp_rw simp_rw₁ : Membership.mem (γ := Finset ((i : ι) → α i)) (piFinset (δ := α) fun (i : ι) ↦ Iic (b i)) x ↔ x ≤ b
⊢ Membership.mem (γ := Finset ((i : ι) → α i))
      ((fun (b : (i : ι) → α i) ↦ (piFinset (δ := α) fun (i : ι) ↦ Iic (b i) : Finset ((a : ι) → α a))) b) x ↔
    x ≤ b
have simp_rw₂ : (∀ (a : ι), x a ∈ Iic (b a)) ↔ x ≤ b
Tactic: simp_rw [mem_piFinset, mem_Iic, le_def]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderBot (α i)
b_1 b x : (i : ι) → α i
simp_rw simp_rw₁ : Membership.mem (γ := Finset ((i : ι) → α i)) (piFinset (δ := α) fun (i : ι) ↦ Iic (b i)) x ↔ x ≤ b
simp_rw₂ : (∀ (a : ι), x a ∈ Iic (b a)) ↔ x ≤ b
⊢ Membership.mem (γ := Finset ((i : ι) → α i))
      ((fun (b : (i : ι) → α i) ↦ (piFinset (δ := α) fun (i : ι) ↦ Iic (b i) : Finset ((a : ι) → α a))) b) x ↔
    x ≤ b
have simp_rw₃ : (∀ (a : ι), x a ≤ b a) ↔ x ≤ b
Tactic: simp_rw [mem_piFinset, mem_Iic, le_def]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderBot (α i)
b : (i : ι) → α i
⊢ #(Iio b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Iic (b i))) 1
have rw : #(Iic b) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Iic (b i))) 1
Tactic: rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderBot (α i)
b : (i : ι) → α i
rw : #(Iic b) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Iic (b i))) 1
⊢ #(Iio b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Iic (b i))) 1
have rw₁ : HSub.hSub (α := ℕ) (∏ i : ι, #(Iic (b i))) 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Iic (b i))) 1
Tactic: rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderTop (α i)
a_1 a x : (i : ι) → α i
simp_rw simp_rw₁ : Membership.mem (γ := Finset ((i : ι) → α i)) (piFinset (δ := α) fun (i : ι) ↦ Ici (a i)) x ↔ a ≤ x
⊢ Membership.mem (γ := Finset ((i : ι) → α i))
      ((fun (a : (i : ι) → α i) ↦ (piFinset (δ := α) fun (i : ι) ↦ Ici (a i) : Finset ((a : ι) → α a))) a) x ↔
    a ≤ x
have simp_rw₂ : (∀ (a_2 : ι), x a_2 ∈ Ici (a a_2)) ↔ a ≤ x
Tactic: simp_rw [mem_piFinset, mem_Ici, le_def]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderTop (α i)
a_1 a x : (i : ι) → α i
simp_rw simp_rw₁ : Membership.mem (γ := Finset ((i : ι) → α i)) (piFinset (δ := α) fun (i : ι) ↦ Ici (a i)) x ↔ a ≤ x
simp_rw₂ : (∀ (a_2 : ι), x a_2 ∈ Ici (a a_2)) ↔ a ≤ x
⊢ Membership.mem (γ := Finset ((i : ι) → α i))
      ((fun (a : (i : ι) → α i) ↦ (piFinset (δ := α) fun (i : ι) ↦ Ici (a i) : Finset ((a : ι) → α a))) a) x ↔
    a ≤ x
have simp_rw₃ : (∀ (a_2 : ι), a a_2 ≤ x a_2) ↔ a ≤ x
Tactic: simp_rw [mem_piFinset, mem_Ici, le_def]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ #(Ioi a) = HSub.hSub (α := ℕ) (∏ i : ι, #(Ici (a i))) 1
have rw : #(Ici a) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Ici (a i))) 1
Tactic: rw [card_Ioi_eq_card_Ici_sub_one, card_Ici]
-- Lean 4 proof step from Mathlib.Data.Pi.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
rw : #(Ici a) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Ici (a i))) 1
⊢ #(Ioi a) = HSub.hSub (α := ℕ) (∏ i : ι, #(Ici (a i))) 1
have rw₁ : HSub.hSub (α := ℕ) (∏ i : ι, #(Ici (a i))) 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Ici (a i))) 1
Tactic: rw [card_Ioi_eq_card_Ici_sub_one, card_Ici]
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x₁ : α
y₁ : β
x₂ : α
y₂ : β
h : (x₁, y₁) = (x₂, y₂)
P : Sort u_5
w : x₁ = x₂ → y₁ = y₂ → P
⊢ P
have refl : (w : x₁ = x₁ → y₁ = y₁ → P) → P
Tactic: cases h
Cleared hypotheses: x₂, y₂, h, w
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n : ℕ
⊢ (map f g)^[n] = map f^[n] g^[n]
have zero : (map f g)^[0] = map f^[0] g^[0]
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n : ℕ
zero : (map f g)^[0] = map f^[0] g^[0]
⊢ (map f g)^[n] = map f^[n] g^[n]
have succ : ∀ (n : ℕ), (map f g)^[n] = map f^[n] g^[n] → (map f g)^[n + 1] = map f^[n + 1] g^[n + 1]
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Total s
x_1 x_2 : α × β
i : α
a : β
j : α
b : β
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
have inl : ∀ (hij : r i j), Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Tactic: obtain hij | rfl | hji := trichotomous_of r i j
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Total s
x_1 x_2 : α × β
i : α
a : β
j : α
b : β
inl : ∀ (hij : r i j), Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
have inr : Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)
Tactic: obtain hij | rfl | hji := trichotomous_of r i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Total s
x_1 x_2 : α × β
i : α
a : β
j : α
b : β
inl : ∀ (hij : r i j), Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
inr : Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
have inr₁ : ∀ (hji : r j i), Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Tactic: obtain hij | rfl | hji := trichotomous_of r i j
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst : Std.Trichotomous r
inst_1 : Std.Trichotomous s
i : α
a : β
⊢ ∀ {b : α × β}, Prod.Lex r s (i, a) b ∨ (i, a) = b ∨ Prod.Lex r s b (i, a)
have this : ∀ (j : α) (b : β), Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Tactic: ⟨j, b⟩
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst : Std.Trichotomous r
inst_1 : Std.Trichotomous s
i : α
a : β
j : α
b : β
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
have inl : ∀ (hij : r i j), Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Tactic: obtain hij | rfl | hji := trichotomous_of r i j
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst : Std.Trichotomous r
inst_1 : Std.Trichotomous s
i : α
a : β
j : α
b : β
inl : ∀ (hij : r i j), Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
have inr : Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)
Tactic: obtain hij | rfl | hji := trichotomous_of r i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst : Std.Trichotomous r
inst_1 : Std.Trichotomous s
i : α
a : β
j : α
b : β
inl : ∀ (hij : r i j), Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
inr : Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
have inr₁ : ∀ (hji : r j i), Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Tactic: obtain hij | rfl | hji := trichotomous_of r i j
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
⊢ map f₁ g₁ (map f₂ g₂ a) = a
have rw : map (f₁ ∘ f₂) (g₁ ∘ g₂) a = a
Tactic: rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
rw : map (f₁ ∘ f₂) (g₁ ∘ g₂) a = a
⊢ map f₁ g₁ (map f₂ g₂ a) = a
have rw₁ : map id (g₁ ∘ g₂) a = a
Tactic: rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
rw : map (f₁ ∘ f₂) (g₁ ∘ g₂) a = a
rw₁ : map id (g₁ ∘ g₂) a = a
⊢ map f₁ g₁ (map f₂ g₂ a) = a
have rw₂ : map id id a = a
Tactic: rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
rw : map (f₁ ∘ f₂) (g₁ ∘ g₂) a = a
rw₁ : map id (g₁ ∘ g₂) a = a
rw₂ : map id id a = a
⊢ map f₁ g₁ (map f₂ g₂ a) = a
have rw₃ : id a = a
Tactic: rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
rw : map (f₁ ∘ f₂) (g₁ ∘ g₂) a = a
rw₁ : map id (g₁ ∘ g₂) a = a
rw₂ : map id id a = a
rw₃ : id a = a
⊢ map f₁ g₁ (map f₂ g₂ a) = a
have rw₄ : a = a
Tactic: rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
⊢ a₁ = a₂
have inhabit : ∀ (inhabited_h : Inhabited β), a₁ = a₂
Tactic: inhabit β
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
⊢ b₁ = b₂
have inhabit : ∀ (inhabited_h : Inhabited α), b₁ = b₂
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
⊢ ∃ (a : α), f a = c
have inhabit : ∀ (inhabited_h : Inhabited δ), ∃ (a : α), f a = c
Tactic: inhabit δ
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
⊢ ∃ (a : α), f a = c
have obtain : ∀ (a : α) (b : β) (h : map f g (a, b) = (c, default)), ∃ (a : α), f a = c
Tactic: obtain ⟨⟨a, b⟩, h⟩ := h (c, default)
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
⊢ ∃ (a : β), g a = d
have inhabit : ∀ (inhabited_h : Inhabited γ), ∃ (a : β), g a = d
Tactic: inhabit γ
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
⊢ ∃ (a : β), g a = d
have obtain : ∀ (a : α) (b : β) (h : map f g (a, b) = (default, d)), ∃ (a : β), g a = d
Tactic: obtain ⟨⟨a, b⟩, h⟩ := h (default, d)
-- Lean 4 proof step from Mathlib.Data.Prod.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
have this : Nonempty γ
Tactic: haveI := Nonempty.map f ‹_›