awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s (↑t : Set β)
hfs : InjOn f s
let let₁ let₂ : ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
let₃ :
  let s' := s.toFinset;
  ∀ (hfst' : Finset.image f s' ⊆ t), ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
let₄ :
  let s' := s.toFinset;
  ∀ (hfst' : Finset.image f s' ⊆ t) (hfs' : InjOn f (↑s' : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
let₅ :
  let s' := s.toFinset;
  ∀ (hfst' : Finset.image f s' ⊆ t) (hfs' : InjOn f (↑s' : Set α)) (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t)
    (hg : ∀ i ∈ s', (↑((g : (a : α) → ↥t) i) : β) = f i),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
let₆ :
  let s' := s.toFinset;
  ∀ (hfst' : Finset.image f s' ⊆ t) (hfs' : InjOn f (↑s' : Set α)) (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t)
    (hg : ∀ i ∈ s', (↑((g : (a : α) → ↥t) i) : β) = f i) (i : α) (hi : i ∈ s), (↑((g : (a : α) → ↥t) i) : β) = f i
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have a : let s' := s.toFinset;
∀ (hfst' : Finset.image f s' ⊆ t) (hfs' : InjOn f (↑s' : Set α)) (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t)
  (hg : ∀ i ∈ s', (↑((g : (a : α) → ↥t) i) : β) = f i) (i : α) (hi : i ∈ s), i ∈ s'
Tactic: classical
    let s' : Finset α := s.toFinset
    have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using hfst
    have hfs' : Set.InjOn f s' := by simpa [s'] using hfs
    obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
    refine ⟨g, fun i hi => ?_⟩
    apply hg
    simpa [s'] using hi
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
⊢ card.{u_1} { x : α // p x ∨ q x } ≤ card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x }
have h : card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })
Tactic: convert! Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
⊢ card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })
have h : card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x }
Tactic: rw [Fintype.card_sum]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
⊢ card.{u_1} { x : α // p x ∨ q x } ≤ card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x }
have h : card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })
Tactic: classical
    convert! Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
    rw [Fintype.card_sum]
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
p q : α → Prop
h : Disjoint p q
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
⊢ card.{u_1} { x : α // p x ∨ q x } = card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x }
have h₁ : card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })
Tactic: convert! Fintype.card_congr (subtypeOrEquiv p q h)
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
p q : α → Prop
h : Disjoint p q
inst : Fintype { x : α // p x }
inst_1 : Fintype { x : α // q x }
inst_2 : Fintype { x : α // p x ∨ q x }
⊢ card.{u_1} { x : α // p x ∨ q x } = card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x }
have h₁ : card.{u_1} { x : α // p x } + card.{u_1} { x : α // q x } = card.{u_1} ({ x : α // p x } ⊕ { x : α // q x })
Tactic: classical
    convert! Fintype.card_congr (subtypeOrEquiv p q h)
    simp
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
⊢ Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β
have refine : ∀ (H : Infinite (α ⊕ β)), Infinite α ∨ Infinite β
Tactic: refine ⟨fun H => ?_, fun H => H.elim (@Sum.infinite_of_left α β) (@Sum.infinite_of_right α β)⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
H : Infinite (α ⊕ β)
⊢ Infinite α ∨ Infinite β
have contrapose! : ∀ (H : Finite α ∧ Finite β), Finite (α ⊕ β)
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (hypothesis)
Goal:
α : Type u_1
β : Type u_2
H : Finite α ∧ Finite β
⊢ Finite (α ⊕ β)
have left : Finite α
Tactic: cases H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (hypothesis)
Goal:
α : Type u_1
β : Type u_2
H : Finite α ∧ Finite β
left : Finite α
⊢ Finite (α ⊕ β)
have right : Finite β
Tactic: cases H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
x : ℤˣ
⊢ Membership.mem (γ := Finset ℤˣ) {1, -1} x
have inl : x = 1 → Membership.mem (γ := Finset ℤˣ) {1, -1} x
Tactic: cases Int.units_eq_one_or x
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
x : ℤˣ
inl : x = 1 → Membership.mem (γ := Finset ℤˣ) {1, -1} x
⊢ Membership.mem (γ := Finset ℤˣ) {1, -1} x
have inr : x = -1 → Membership.mem (γ := Finset ℤˣ) {1, -1} x
Tactic: cases Int.units_eq_one_or x
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
⊢ Nat.card.{u_1} αˣ = Nat.card α - 1
have rw : Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
have inl : Finite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 } →
  Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: rcases finite_or_infinite {a : α // a ≠ 0}
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inl :
  Finite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 } →
    Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
have inr : Infinite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 } →
  Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: rcases finite_or_infinite {a : α // a ≠ 0}
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
h : Finite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
have inl : Nat.card.{u_1} { a : α // a = 0 } + Nat.card.{u_1} { a : α // ¬a = 0 } - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
h : Finite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 }
inl : Nat.card.{u_1} { a : α // a = 0 } + Nat.card.{u_1} { a : α // ¬a = 0 } - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
have inl₁ : 1 + Nat.card.{u_1} { a : α // ¬a = 0 } - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
h : Finite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 }
inl : Nat.card.{u_1} { a : α // a = 0 } + Nat.card.{u_1} { a : α // ¬a = 0 } - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
inl₁ : 1 + Nat.card.{u_1} { a : α // ¬a = 0 } - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
have inl₂ : Nat.card.{u_1} { a : α // ¬a = 0 } = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
h : Infinite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
have inr : HSub.hSub (α := ℕ) 0 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
h : Infinite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 }
inr : HSub.hSub (α := ℕ) 0 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
have inr₁ : HSub.hSub (α := ℕ) 0 1 = 0
Tactic: rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
h : Infinite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 }
inr : HSub.hSub (α := ℕ) 0 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
inr₁ : HSub.hSub (α := ℕ) 0 1 = 0
⊢ Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
have inr₂ : Eq (α := ℕ) 0 0
Tactic: rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
⊢ Nat.card.{u_1} αˣ = Nat.card α - 1
have rw : Nat.card.{u_1} { a : α // a ≠ 0 } = Nat.card α - 1
Tactic: classical
  rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]
  rcases finite_or_infinite {a : α // a ≠ 0}
  · rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
  · rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
rw : Nat.card.{u_1} { a : α // a ≠ 0 } = Nat.card α - 1
⊢ Nat.card.{u_1} αˣ = Nat.card α - 1
have rw₁ : Nat.card α - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: classical
  rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]
  rcases finite_or_infinite {a : α // a ≠ 0}
  · rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
  · rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
rw : Nat.card.{u_1} { a : α // a ≠ 0 } = Nat.card α - 1
rw₁ : Nat.card α - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} αˣ = Nat.card α - 1
have rw₂ : Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: classical
  rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]
  rcases finite_or_infinite {a : α // a ≠ 0}
  · rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
  · rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
rw : Nat.card.{u_1} { a : α // a ≠ 0 } = Nat.card α - 1
rw₁ : Nat.card α - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
rw₂ rw₃ rw₄ : Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} αˣ = Nat.card α - 1
have inl : Finite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 } →
  Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: classical
  rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]
  rcases finite_or_infinite {a : α // a ≠ 0}
  · rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
  · rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
rw : Nat.card.{u_1} { a : α // a ≠ 0 } = Nat.card α - 1
rw₁ : Nat.card α - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
rw₂ rw₃ rw₄ : Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
inl :
  Finite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 } →
    Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
⊢ Nat.card.{u_1} αˣ = Nat.card α - 1
have inr : Infinite.{max 1 (u_1 + 1)} { a : α // a ≠ 0 } →
  Nat.card.{u_1} ({ a : α // a = 0 } ⊕ { a : α // ¬a = 0 }) - 1 = Nat.card.{u_1} { a : α // a ≠ 0 }
Tactic: classical
  rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]
  rcases finite_or_infinite {a : α // a ≠ 0}
  · rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
  · rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : Finite α
⊢ Nat.card α = Nat.card.{u_1} αˣ + 1
have rw : Nat.card α = Nat.card α - 1 + 1
Tactic: rw [Nat.card_units, tsub_add_cancel_of_le Nat.card_pos]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : Finite α
rw : Nat.card α = Nat.card α - 1 + 1
⊢ Nat.card α = Nat.card.{u_1} αˣ + 1
have rw₁ : Nat.card α = Nat.card α
Tactic: rw [Nat.card_units, tsub_add_cancel_of_le Nat.card_pos]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : Fintype α
inst_2 : DecidableEq α
⊢ card.{u_1} αˣ = card α - 1
have rw : Nat.card.{u_1} αˣ = card α - 1
Tactic: rw [← Nat.card_eq_fintype_card, Nat.card_units, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : Fintype α
inst_2 : DecidableEq α
rw : Nat.card.{u_1} αˣ = card α - 1
⊢ card.{u_1} αˣ = card α - 1
have rw₁ : Nat.card α - 1 = card α - 1
Tactic: rw [← Nat.card_eq_fintype_card, Nat.card_units, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : Fintype α
inst_2 : DecidableEq α
rw : Nat.card.{u_1} αˣ = card α - 1
rw₁ : Nat.card α - 1 = card α - 1
⊢ card.{u_1} αˣ = card α - 1
have rw₂ : card α - 1 = card α - 1
Tactic: rw [← Nat.card_eq_fintype_card, Nat.card_units, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : Fintype α
inst_2 : DecidableEq α
⊢ card α = card.{u_1} αˣ + 1
have rw : card α = card α - 1 + 1
Tactic: rw [Fintype.card_units, tsub_add_cancel_of_le Fintype.card_pos]
-- Lean 4 proof step from Mathlib.Data.Fintype.Units (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : Fintype α
inst_2 : DecidableEq α
rw : card α = card α - 1 + 1
⊢ card α = card.{u_1} αˣ + 1
have rw₁ : card α = card α
Tactic: rw [Fintype.card_units, tsub_add_cancel_of_le Fintype.card_pos]
-- Lean 4 proof step from Mathlib.Data.FunLike.Basic (goal)
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h : f = g
⊢ (⇑f : (a : α) → β a) = (⇑g : (a : α) → β a)
have refl : (⇑f : (a : α) → β a) = (⇑f : (a : α) → β a)
Tactic: cases h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Data.FunLike.Basic (goal)
Goal:
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst : Decidable P
f : P → F
g : ¬P → F
x : α
⊢ Eq.{u_3} (α := β) ((if h : P then f h else g h : (a : α) → β) x : β)
    (if h : P then (f h : (a : α) → β) x else (g h : (a : α) → β) x : β)
have pos : ∀ (h : P), Eq.{u_3} (α := β) ((f h : (a : α) → β) x : β) ((f h : (a : α) → β) x : β)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.FunLike.Basic (goal)
Goal:
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst : Decidable P
f : P → F
g : ¬P → F
x : α
pos : ∀ (h : P), Eq.{u_3} (α := β) ((f h : (a : α) → β) x : β) ((f h : (a : α) → β) x : β)
⊢ Eq.{u_3} (α := β) ((if h : P then f h else g h : (a : α) → β) x : β)
    (if h : P then (f h : (a : α) → β) x else (g h : (a : α) → β) x : β)
have neg : ∀ (h : ¬P), Eq.{u_3} (α := β) ((g h : (a : α) → β) x : β) ((g h : (a : α) → β) x : β)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.FunLike.Equiv (goal)
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
b : β
a : α
⊢ inv e b = a ↔ b = (e : (a : α) → β) a
have mp : inv e b = a → b = (e : (a : α) → β) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.FunLike.Equiv (goal)
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
b : β
a : α
mp : inv e b = a → b = (e : (a : α) → β) a
⊢ inv e b = a ↔ b = (e : (a : α) → β) a
have mpr : b = (e : (a : α) → β) a → inv e b = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.FunLike.Graded (goal)
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
⊢ Membership.mem.{u_3, u_5} (α := B) (ℬ i) ((e : (a : A) → B) (EquivLike.inv e (↑y : B)) : B)
have rw : (↑y : B) ∈ ℬ i
Tactic: rw [EquivLike.apply_inv_apply]
-- Lean 4 proof step from Mathlib.Data.FunLike.Graded (goal)
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x : ↥(𝒜 i)
⊢ (fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) ⋯ : ↥(𝒜 i)))
      (subtypeMap e i x) =
    x
have a : (↑((fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) sorry : ↥(𝒜 i)))
        (subtypeMap e i x)) :
    A) =
  (↑x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Graded (goal)
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x : ↥(ℬ i)
⊢ subtypeMap e i
      ((fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) ⋯ : ↥(𝒜 i))) x) =
    x
have a : (↑(subtypeMap e i
        ((fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) sorry : ↥(𝒜 i))) x)) :
    B) =
  (↑x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Group (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsMulApply F α β
⊢ Function.Injective (α := F) (β := α → β) (⇑(coeMulHom F α β) : (a : F) → α → β)
have rw : Function.Injective (α := F) (β := α → β) (DFunLike.coe (β := fun (a : α) ↦ β))
Tactic: rw [coe_coeMulHom]
-- Lean 4 proof step from Mathlib.Data.FunLike.Group (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : MulOne F
inst_2 : MulOneClass β
inst_3 : IsOneApply F α β
inst_4 : IsMulApply F α β
⊢ Function.Injective (α := F) (β := α → β) (⇑(coeMonoidHom F α β) : (a : F) → α → β)
have rw : Function.Injective (α := F) (β := α → β) (DFunLike.coe (β := fun (a : α) ↦ β))
Tactic: rw [coe_coeMonoidHom]
-- Lean 4 proof step from Mathlib.Data.FunLike.IsApply (goal)
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : One F
inst_2 : One β
inst_3 : IsOneApply F α β
⊢ Eq (α := α → β) (⇑1 : (a : α) → β) 1
have h : ∀ (x : α), Eq.{u_6 + 1} (α := β) ((1 : (a : α) → β) x : β) (1 x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FunLike.IsApply (goal)
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsMulApply F α β
f g : F
⊢ (⇑(f * g) : (a : α) → β) = HMul.hMul (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
have h : ∀ (x : α),
  (f * g : (a : α) → β) x = HMul.hMul (α := (a : α) → β) (β := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FunLike.IsApply (goal)
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Div F
inst_2 : Div β
inst_3 : IsDivApply F α β
f g : F
⊢ (⇑(f / g) : (a : α) → β) = HDiv.hDiv (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
have h : ∀ (x : α),
  (f / g : (a : α) → β) x = HDiv.hDiv (α := (a : α) → β) (β := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FunLike.IsApply (goal)
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Inv F
inst_2 : Inv β
inst_3 : IsInvApply F α β
f : F
⊢ Eq (α := (a : α) → β) (⇑f⁻¹ : (a : α) → β) (⇑f : (a : α) → β)⁻¹
have h : ∀ (x : α), Eq.{u_6 + 1} (α := β) ((f⁻¹ : (a : α) → β) x : β) ((⇑f : (a : α) → β)⁻¹ x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FunLike.IsApply (goal)
Goal:
M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : SMul M F
inst_2 : SMul M β
inst_3 : IsSMulApply M F α β
n : M
f : F
⊢ (⇑(n • f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β)
have h : ∀ (x : α), (n • f : (a : α) → β) x = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FunLike.IsApply (goal)
Goal:
M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Pow F M
inst_2 : Pow β M
inst_3 : IsPowApply M F α β
f : F
n : M
⊢ (⇑(f ^ n) : (a : α) → β) = HPow.hPow (α := (a : α) → β) (⇑f : (a : α) → β) n
have h : ∀ (x : α), (f ^ n : (a : α) → β) x = HPow.hPow (α := (a : α) → β) (⇑f : (a : α) → β) n x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FunLike.IsApply (goal)
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : One F'
inst_2 : IsOneApplyEqSelf F' α
⊢ Eq.{u_5 + 1} (α := (a : α) → α) (⇑1 : (a : α) → α) id
have h : ∀ (x : α), (1 : (a : α) → α) x = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FunLike.IsApply (goal)
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : Mul F'
inst_2 : IsMulApplyEqComp F' α
f g : F'
⊢ Eq.{u_5 + 1} (α := α → α) (⇑(f * g) : (a : α) → α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α))
have h : ∀ (x : α),
  Eq (α := α) ((f * g : (a : α) → α) x : α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FunLike.IsApply (goal)
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : NatCast F'
inst_2 : One F'
inst_3 : SMul Nat α
inst_4 : SMul Nat F'
inst_5 : IsSMulApply Nat F' α α
inst_6 : IsNatCastApply F' α
inst_7 : IsOneApplyEqSelf F' α
n : Nat
⊢ (↑n : F') = HSMul.hSMul (β := F') n 1
have h : ∀ (x : α), Eq (α := α) (((↑n : F') : (a : α) → α) x : α) ((HSMul.hSMul (β := F') n 1 : (a : α) → α) x : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.IsApply (goal)
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : IntCast F'
inst_2 : One F'
inst_3 : SMul Int α
inst_4 : SMul Int F'
inst_5 : IsSMulApply Int F' α α
inst_6 : IsIntCastApply F' α
inst_7 : IsOneApplyEqSelf F' α
n : Int
⊢ (↑n : F') = HSMul.hSMul (β := F') n 1
have h : ∀ (x : α), Eq (α := α) (((↑n : F') : (a : α) → α) x : α) ((HSMul.hSMul (β := F') n 1 : (a : α) → α) x : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Module (goal)
Goal:
M : Type u_1
M' : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst : SMul M β
inst_1 : SMul M' β
inst_2 : SMul M F
inst_3 : SMul M' F
inst_4 : IsSMulApply M F α β
inst_5 : IsSMulApply M' F α β
inst_6 : SMul M M'
inst_7 : IsScalarTower M M' β
x : M
x_1 : M'
x_2 : F
⊢ (x • x_1) • x_2 = x • x_1 • x_2
have h : ∀ (x_3 : α), Eq.{u_5 + 1} (α := β) (((x • x_1) • x_2 : (a : α) → β) x_3 : β) ((x • x_1 • x_2 : (a : α) → β) x_3 : β)
Tactic: apply DFunLike.ext