awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → b = a → b = r
pos₁ : r = a → ¬b = a → b = b → a = r
neg : r = a → ¬b = a → ¬b = b → b = r
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
have pos₂ : ¬r = a → r = b → a = a → b = r
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → b = a → b = r
pos₁ : r = a → ¬b = a → b = b → a = r
neg : r = a → ¬b = a → ¬b = b → b = r
pos₂ : ¬r = a → r = b → a = a → b = r
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
have pos₃ : ¬r = a → r = b → ¬a = a → a = b → a = r
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → b = a → b = r
pos₁ : r = a → ¬b = a → b = b → a = r
neg : r = a → ¬b = a → ¬b = b → b = r
pos₂ : ¬r = a → r = b → a = a → b = r
pos₃ : ¬r = a → r = b → ¬a = a → a = b → a = r
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
have neg₁ : ¬r = a → r = b → ¬a = a → ¬a = b → a = r
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → b = a → b = r
pos₁ : r = a → ¬b = a → b = b → a = r
neg : r = a → ¬b = a → ¬b = b → b = r
pos₂ : ¬r = a → r = b → a = a → b = r
pos₃ : ¬r = a → r = b → ¬a = a → a = b → a = r
neg₁ : ¬r = a → r = b → ¬a = a → ¬a = b → a = r
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
have neg₂ : ¬r = a → ¬r = b → r = r
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
⊢ swapCore a b r = swapCore b a r
have unfold : (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
Tactic: unfold swapCore
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
have pos : r = a → r = b → b = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → r = b → b = a
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
have neg : r = a → ¬r = b → b = b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → r = b → b = a
neg : r = a → ¬r = b → b = b
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
have pos₁ : ¬r = a → r = b → a = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → r = b → b = a
neg : r = a → ¬r = b → b = b
pos₁ : ¬r = a → r = b → a = a
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
have neg₁ : ¬r = a → ¬r = b → r = r
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
a b x : α
h : (swap a b : (a : α) → α) x ≠ x
⊢ x = a ∨ x = b
have contrapose! : ∀ (h : x ≠ a ∧ x ≠ b), (swap a b : (a : α) → α) x = x
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
a b x : α
π : Perm α
⊢ (Equiv.trans π (swap a b) : (a : α) → α) x =
    if (π : (a : α) → α) x = a then b else if (π : (a : α) → α) x = b then a else (π : (a : α) → α) x
have mk : ∀ (toFun invFun : α → α) (left_inv : LeftInverse invFun toFun) (right_inv : RightInverse invFun toFun),
  ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α }.trans (swap a b) :
        (a : α) → α)
      x =
    if
        ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α } : (a : α) → α) x =
          a then
      b
    else
      if
          ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α } : (a : α) → α) x =
            b then
        a
      else ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α } : (a : α) → α) x
Tactic: cases π
Cleared hypotheses: π
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
a c d : α
h : Eq.{max 1 u_1} (swap a c) (swap a d)
⊢ c = d
have rw : (swap a c : (a : α) → α) a = d
Tactic: rw [← Equiv.swap_apply_left a c, h, Equiv.swap_apply_left]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
a c d : α
h : Eq.{max 1 u_1} (swap a c) (swap a d)
rw : (swap a c : (a : α) → α) a = d
⊢ c = d
have rw₁ : (swap a d : (a : α) → α) a = d
Tactic: rw [← Equiv.swap_apply_left a c, h, Equiv.swap_apply_left]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
a c d : α
h : Eq.{max 1 u_1} (swap a c) (swap a d)
rw : (swap a c : (a : α) → α) a = d
rw₁ : (swap a d : (a : α) → α) a = d
⊢ c = d
have rw₂ : d = d
Tactic: rw [← Equiv.swap_apply_left a c, h, Equiv.swap_apply_left]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
a : α
⊢ Injective (β := Perm α) fun (x : α) ↦ swap x a
have simp_rw : Injective (β := Perm α) fun (x : α) ↦ swap a x
Tactic: simp_rw [swap_comm _ a]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
inst : DecidableEq α_1
α : Type u_9
inst_1 : Nontrivial α
⊢ Nontrivial.{u_9} (Perm α)
have obtain : ∀ (a : α), Nontrivial.{u_9} (Perm α)
Tactic: obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
inst : DecidableEq α_1
α : Type u_9
inst_1 : Nontrivial α
⊢ Nontrivial.{u_9} (Perm α)
have obtain : ∀ (a : α), Nontrivial.{u_9} (Perm α)
Tactic: classical
  obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)
  exact Function.Injective.nontrivial (Equiv.swap_injective_of_left a)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
⊢ Membership.mem (γ := Set α) (Set.image (⇑(swap i j) : (a : α) → α) s) a ↔ a ∈ insert j s \ {i}
have mp : Membership.mem (γ := Set α) (Set.image (⇑(swap i j) : (a : α) → α) s) a → a ∈ insert j s \ {i}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
mp : Membership.mem (γ := Set α) (Set.image (⇑(swap i j) : (a : α) → α) s) a → a ∈ insert j s \ {i}
⊢ Membership.mem (γ := Set α) (Set.image (⇑(swap i j) : (a : α) → α) s) a ↔ a ∈ insert j s \ {i}
have mpr : a ∈ insert j s \ {i} → Membership.mem (γ := Set α) (Set.image (⇑(swap i j) : (a : α) → α) s) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
⊢ Membership.mem (α := α) (insert j s \ {i}) ((swap i j : (a : α) → α) a : α)
have mp : ∀ (hi : a ∈ s), Membership.mem (α := α) (insert j s \ {a}) ((swap a j : (a : α) → α) a : α)
Tactic: obtain rfl | ne := eq_or_ne a i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
mp : ∀ (hi : a ∈ s), Membership.mem (α := α) (insert j s \ {a}) ((swap a j : (a : α) → α) a : α)
⊢ Membership.mem (α := α) (insert j s \ {i}) ((swap i j : (a : α) → α) a : α)
have mp₁ : ∀ (ne : a ≠ i), Membership.mem (α := α) (insert j s \ {i}) ((swap i j : (a : α) → α) a : α)
Tactic: obtain rfl | ne := eq_or_ne a i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ Membership.mem (α := α) (insert j s \ {a}) ((swap a j : (a : α) → α) a : α)
have mp : j ∈ insert j s \ {a}
Tactic: rw [swap_apply_left]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ Membership.mem (α := α) (insert j s \ {i}) ((swap i j : (a : α) → α) a : α)
have mp : a ∈ insert j s \ {i}
Tactic: rw [swap_apply_of_ne_of_ne ne (ne_of_mem_of_not_mem ha hj)]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
⊢ Eq (α := ((b : β) → P) ≃ ((a : α) → P))
    (Equiv.symm (piCongrLeft' (fun (x : α) ↦ P) e) : ((b : β) → P) ≃ ((a : α) → P))
    (piCongrLeft' (fun (a : β) ↦ P) e.symm : ((a : β) → P) ≃ ((b : α) → P))
have H : ∀ (x : (b : β) → P) (x_1 : α),
  Eq.{u_9} (α := P)
    (((Equiv.symm (piCongrLeft' (fun (x : α) ↦ P) e) : ((b : β) → P) ≃ ((a : α) → P)) : (a : (b : β) → P) → (a : α) → P)
        x x_1 :
      P)
    ((piCongrLeft' (fun (a : β) ↦ P) e.symm : (a : (b : β) → P) → (a : α) → P) x x_1 : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P ((e.symm : (a : β) → α) b)
b : β
⊢ ((piCongrLeft' P e).symm : (a : (b : β) → P ((e.symm : (a : β) → α) b)) → (a : α) → P a) g
      ((e.symm : (a : β) → α) b) =
    g b
have rw : HEq (α := P ((e.symm : (a : β) → α) ((e : (a : α) → β) ((e.symm : (a : β) → α) b : α) : β)))
  (g ((e : (a : α) → β) ((e.symm : (a : β) → α) b : α))) (g b)
Tactic: rw [piCongrLeft'_symm_apply, ← heq_iff_eq, eqRec_heq_iff_heq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → Equiv.{w, z} (W a) (Z ((h₁ : (a : α) → β) a))
f : (a : α) → W a
a : α
⊢ Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((h₁.piCongr (W := W) (Z := Z) h₂ : (a : (a : α) → W a) → (b : β) → Z b) f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
have rw : Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
  (((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂).trans (piCongrLeft Z h₁) :
        (a : (a : α) → W a) → (b : β) → Z b)
      f ((h₁ : (a : α) → β) a) :
    Z ((h₁ : (a : α) → β) a))
  ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
Tactic: rw [piCongr, trans_apply, piCongrLeft_apply_apply, piCongrRight_apply, Pi.map_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → Equiv.{w, z} (W a) (Z ((h₁ : (a : α) → β) a))
f : (a : α) → W a
a : α
rw :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    (((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂).trans (piCongrLeft Z h₁) :
          (a : (a : α) → W a) → (b : β) → Z b)
        f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
⊢ Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((h₁.piCongr (W := W) (Z := Z) h₂ : (a : (a : α) → W a) → (b : β) → Z b) f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
have rw₁ : Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
  ((piCongrLeft Z h₁ : (a : (a : α) → Z ((h₁ : (a : α) → β) a)) → (b : β) → Z b)
      ((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂ :
            (a : (a : α) → W a) → (a : α) → Z ((h₁ : (a : α) → β) a))
          f :
        (a : α) → Z ((h₁ : (a : α) → β) a))
      ((h₁ : (a : α) → β) a) :
    Z ((h₁ : (a : α) → β) a))
  ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
Tactic: rw [piCongr, trans_apply, piCongrLeft_apply_apply, piCongrRight_apply, Pi.map_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → Equiv.{w, z} (W a) (Z ((h₁ : (a : α) → β) a))
f : (a : α) → W a
a : α
rw :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    (((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂).trans (piCongrLeft Z h₁) :
          (a : (a : α) → W a) → (b : β) → Z b)
        f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
rw₁ :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((piCongrLeft Z h₁ : (a : (a : α) → Z ((h₁ : (a : α) → β) a)) → (b : β) → Z b)
        ((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂ :
              (a : (a : α) → W a) → (a : α) → Z ((h₁ : (a : α) → β) a))
            f :
          (a : α) → Z ((h₁ : (a : α) → β) a))
        ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
⊢ Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((h₁.piCongr (W := W) (Z := Z) h₂ : (a : (a : α) → W a) → (b : β) → Z b) f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
have rw₂ : Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
  ((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂ :
        (a : (a : α) → W a) → (a : α) → Z ((h₁ : (a : α) → β) a))
      f a :
    Z ((h₁ : (a : α) → β) a))
  ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
Tactic: rw [piCongr, trans_apply, piCongrLeft_apply_apply, piCongrRight_apply, Pi.map_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → Equiv.{w, z} (W a) (Z ((h₁ : (a : α) → β) a))
f : (a : α) → W a
a : α
rw :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    (((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂).trans (piCongrLeft Z h₁) :
          (a : (a : α) → W a) → (b : β) → Z b)
        f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
rw₁ :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((piCongrLeft Z h₁ : (a : (a : α) → Z ((h₁ : (a : α) → β) a)) → (b : β) → Z b)
        ((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂ :
              (a : (a : α) → W a) → (a : α) → Z ((h₁ : (a : α) → β) a))
            f :
          (a : α) → Z ((h₁ : (a : α) → β) a))
        ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
rw₂ :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂ :
          (a : (a : α) → W a) → (a : α) → Z ((h₁ : (a : α) → β) a))
        f a :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
⊢ Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((h₁.piCongr (W := W) (Z := Z) h₂ : (a : (a : α) → W a) → (b : β) → Z b) f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
have rw₃ : Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
  (Pi.map.{u_1, w, z} (α := W) (β := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a))
      (fun (a : α) ↦ ((⇑(h₂ a) : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) : (a_1 : W a) → Z ((h₁ : (a : α) → β) a))) f
      a :
    Z ((h₁ : (a : α) → β) a))
  ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
Tactic: rw [piCongr, trans_apply, piCongrLeft_apply_apply, piCongrRight_apply, Pi.map_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → Equiv.{w, z} (W a) (Z ((h₁ : (a : α) → β) a))
f : (a : α) → W a
a : α
rw :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    (((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂).trans (piCongrLeft Z h₁) :
          (a : (a : α) → W a) → (b : β) → Z b)
        f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
rw₁ :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((piCongrLeft Z h₁ : (a : (a : α) → Z ((h₁ : (a : α) → β) a)) → (b : β) → Z b)
        ((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂ :
              (a : (a : α) → W a) → (a : α) → Z ((h₁ : (a : α) → β) a))
            f :
          (a : α) → Z ((h₁ : (a : α) → β) a))
        ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
rw₂ :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((piCongrRight (β₁ := W) (β₂ := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a)) h₂ :
          (a : (a : α) → W a) → (a : α) → Z ((h₁ : (a : α) → β) a))
        f a :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
rw₃ :
  Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    (Pi.map.{u_1, w, z} (α := W) (β := fun (a : α) ↦ Z ((h₁ : (a : α) → β) a))
        (fun (a : α) ↦ ((⇑(h₂ a) : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) : (a_1 : W a) → Z ((h₁ : (a : α) → β) a))) f
        a :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
⊢ Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
    ((h₁.piCongr (W := W) (Z := Z) h₂ : (a : (a : α) → W a) → (b : β) → Z b) f ((h₁ : (a : α) → β) a) :
      Z ((h₁ : (a : α) → β) a))
    ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
have rw₄ : Eq.{z} (α := Z ((h₁ : (a : α) → β) a))
  ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
  ((h₂ a : (a_1 : W a) → Z ((h₁ : (a : α) → β) a)) (f a) : Z ((h₁ : (a : α) → β) a))
Tactic: rw [piCongr, trans_apply, piCongrLeft_apply_apply, piCongrRight_apply, Pi.map_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_11
α' : Sort u_12
β : Sort u_13
β' : Sort u_14
ε₁ : α ≃ α'
ε₂ : β' ≃ β
f : α → β
f' : α' → β'
⊢ (⇑ε₂.symm : (a : β) → β') ∘ f ∘ (⇑ε₁.symm : (a : α') → α) = f' ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
have rw : f ∘ (⇑ε₁.symm : (a : α') → α) = (⇑ε₂ : (a : β') → β) ∘ f' ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
Tactic: rw [Equiv.symm_comp_eq, Equiv.comp_symm_eq, Function.comp_assoc]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_11
α' : Sort u_12
β : Sort u_13
β' : Sort u_14
ε₁ : α ≃ α'
ε₂ : β' ≃ β
f : α → β
f' : α' → β'
rw : f ∘ (⇑ε₁.symm : (a : α') → α) = (⇑ε₂ : (a : β') → β) ∘ f' ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
⊢ (⇑ε₂.symm : (a : β) → β') ∘ f ∘ (⇑ε₁.symm : (a : α') → α) = f' ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
have rw₁ : f = ((⇑ε₂ : (a : β') → β) ∘ f') ∘ (⇑ε₁ : (a : α) → α') ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
Tactic: rw [Equiv.symm_comp_eq, Equiv.comp_symm_eq, Function.comp_assoc]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_11
α' : Sort u_12
β : Sort u_13
β' : Sort u_14
ε₁ : α ≃ α'
ε₂ : β' ≃ β
f : α → β
f' : α' → β'
rw : f ∘ (⇑ε₁.symm : (a : α') → α) = (⇑ε₂ : (a : β') → β) ∘ f' ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
rw₁ : f = ((⇑ε₂ : (a : β') → β) ∘ f') ∘ (⇑ε₁ : (a : α) → α') ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
⊢ (⇑ε₂.symm : (a : β) → β') ∘ f ∘ (⇑ε₁.symm : (a : α') → α) = f' ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
have rw₂ : f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α') ↔ f = (⇑ε₂ : (a : β') → β) ∘ f' ∘ (⇑ε₁ : (a : α) → α')
Tactic: rw [Equiv.symm_comp_eq, Equiv.comp_symm_eq, Function.comp_assoc]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
α' : Sort u_9
inst : DecidableEq α'
inst_1 : DecidableEq α
f : α → β
g : α' ≃ α
a : α
v : β
⊢ Eq (α := α' → β) (update (β := fun (a : α) ↦ β) f a v ∘ (⇑g : (a : α') → α) : α' → β)
    (update (β := fun (a : α') ↦ β) (f ∘ (⇑g : (a : α') → α)) ((g.symm : (a : α) → α') a) v : (a : α') → β)
have rw : Eq (α := α' → β) (update (β := fun (a : α) ↦ β) f a v ∘ (⇑g : (a : α') → α))
  (update (β := fun (a : α) ↦ β) f ((g : (a : α') → α) ((g.symm : (a : α) → α') a : α')) v ∘ (⇑g : (a : α') → α))
Tactic: rw [← update_comp_eq_of_injective _ g.injective, g.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
α' : Sort u_9
inst : DecidableEq α'
inst_1 : DecidableEq α
f : α → β
g : α' ≃ α
a : α
v : β
rw :
  Eq (α := α' → β) (update (β := fun (a : α) ↦ β) f a v ∘ (⇑g : (a : α') → α))
    (update (β := fun (a : α) ↦ β) f ((g : (a : α') → α) ((g.symm : (a : α) → α') a : α')) v ∘ (⇑g : (a : α') → α))
⊢ Eq (α := α' → β) (update (β := fun (a : α) ↦ β) f a v ∘ (⇑g : (a : α') → α) : α' → β)
    (update (β := fun (a : α') ↦ β) (f ∘ (⇑g : (a : α') → α)) ((g.symm : (a : α) → α') a) v : (a : α') → β)
have rw₁ : Eq (α := α' → β) (update (β := fun (a : α) ↦ β) f a v ∘ (⇑g : (a : α') → α))
  (update (β := fun (a : α) ↦ β) f a v ∘ (⇑g : (a : α') → α))
Tactic: rw [← update_comp_eq_of_injective _ g.injective, g.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P ((e.symm : (a : β) → α) b)
⊢ Eq (α := (b : β) → P ((e.symm : (a : β) → α) b))
    ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
        (update (β := P) f ((e.symm : (a : β) → α) b) x) :
      (b : β) → P ((e.symm : (a : β) → α) b))
    (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
        ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b x :
      (a : β) → P ((e.symm : (a : β) → α) a))
have h : ∀ (b' : β),
  Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
    ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
        (update (β := P) f ((e.symm : (a : β) → α) b) x) b' :
      P ((e.symm : (a : β) → α) b'))
    (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
        ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b x b' :
      P ((e.symm : (a : β) → α) b'))
Tactic: ext b'