Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn (Lean4Axiomatic/Relation/Equivalence/Impl.lean)

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ≃ (a₂, b₂) ↔ a₁ ≃ a₂ ∧ b₁ ≃ b₂
Tactic:
let dffp := @depFn_from_prod
State after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
⊢ (a₁, b₁) ≃ (a₂, b₂) ↔ a₁ ≃ a₂ ∧ b₁ ≃ b₂

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
⊢ (a₁, b₁) ≃ (a₂, b₂) ↔ a₁ ≃ a₂ ∧ b₁ ≃ b₂
Tactic:
let expanded_eqv := (hand : Hand) → dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
State after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ (a₁, b₁) ≃ (a₂, b₂) ↔ a₁ ≃ a₂ ∧ b₁ ≃ b₂

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ (a₁, b₁) ≃ (a₂, b₂) ↔ a₁ ≃ a₂ ∧ b₁ ≃ b₂
Tactic:
apply Iff.intro
State after:
case mp
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ (a₁, b₁) ≃ (a₂, b₂) → a₁ ≃ a₂ ∧ b₁ ≃ b₂

case mpr
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂ → (a₁, b₁) ≃ (a₂, b₂)

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ (a₁, b₁) ≃ (a₂, b₂) → a₁ ≃ a₂ ∧ b₁ ≃ b₂
Tactic:
case mp =>
  intro (_ : (a₁, b₁) ≃ (a₂, b₂))
  show a₁ ≃ a₂ ∧ b₁ ≃ b₂
  have elem_eqv : expanded_eqv := ‹(a₁, b₁) ≃ (a₂, b₂)›
  have : a₁ ≃ a₂ := elem_eqv Hand.L
  have : b₁ ≃ b₂ := elem_eqv Hand.R
  exact And.intro ‹a₁ ≃ a₂› ‹b₁ ≃ b₂›
State after:
no goals

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂ → (a₁, b₁) ≃ (a₂, b₂)
Tactic:
case mpr =>
  intro (And.intro (_ : a₁ ≃ a₂) (_ : b₁ ≃ b₂))
  show (a₁, b₁) ≃ (a₂, b₂)
  show expanded_eqv
  intro hand
  cases hand
  case L => exact ‹a₁ ≃ a₂›
  case R => exact ‹b₁ ≃ b₂›
State after:
no goals

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ (a₁, b₁) ≃ (a₂, b₂) → a₁ ≃ a₂ ∧ b₁ ≃ b₂
Tactic:
intro (_ : (a₁, b₁) ≃ (a₂, b₂))
State after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
x✝ : (a₁, b₁) ≃ (a₂, b₂)
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
x✝ : (a₁, b₁) ≃ (a₂, b₂)
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂
Tactic:
have elem_eqv : expanded_eqv := ‹(a₁, b₁) ≃ (a₂, b₂)›
State after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
x✝ : (a₁, b₁) ≃ (a₂, b₂)
elem_eqv : expanded_eqv
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
x✝ : (a₁, b₁) ≃ (a₂, b₂)
elem_eqv : expanded_eqv
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂
Tactic:
have : a₁ ≃ a₂ := elem_eqv Hand.L
State after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
x✝ : (a₁, b₁) ≃ (a₂, b₂)
elem_eqv : expanded_eqv
this : a₁ ≃ a₂
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
x✝ : (a₁, b₁) ≃ (a₂, b₂)
elem_eqv : expanded_eqv
this : a₁ ≃ a₂
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂
Tactic:
have : b₁ ≃ b₂ := elem_eqv Hand.R
State after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
x✝ : (a₁, b₁) ≃ (a₂, b₂)
elem_eqv : expanded_eqv
this✝ : a₁ ≃ a₂
this : b₁ ≃ b₂
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
x✝ : (a₁, b₁) ≃ (a₂, b₂)
elem_eqv : expanded_eqv
this✝ : a₁ ≃ a₂
this : b₁ ≃ b₂
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂
Tactic:
exact And.intro ‹a₁ ≃ a₂› ‹b₁ ≃ b₂›
State after:
no goals

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂ → (a₁, b₁) ≃ (a₂, b₂)
Tactic:
intro (And.intro (_ : a₁ ≃ a₂) (_ : b₁ ≃ b₂))
State after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ (a₁, b₁) ≃ (a₂, b₂)

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ (a₁, b₁) ≃ (a₂, b₂)
Tactic:
show expanded_eqv
State after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ expanded_eqv

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ expanded_eqv
Tactic:
intro hand
State after:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
hand : Hand
⊢ dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
hand : Hand
⊢ dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
Tactic:
cases hand
State after:
case L
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ dffp (a₁, b₁) Hand.L ≃ dffp (a₂, b₂) Hand.L

case R
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ dffp (a₁, b₁) Hand.R ≃ dffp (a₂, b₂) Hand.R

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ dffp (a₁, b₁) Hand.L ≃ dffp (a₂, b₂) Hand.L
Tactic:
case L => exact ‹a₁ ≃ a₂›
State after:
no goals

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ dffp (a₁, b₁) Hand.R ≃ dffp (a₂, b₂) Hand.R
Tactic:
case R => exact ‹b₁ ≃ b₂›
State after:
no goals

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ dffp (a₁, b₁) Hand.L ≃ dffp (a₂, b₂) Hand.L
Tactic:
exact ‹a₁ ≃ a₂›
State after:
no goals

State before:
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ dffp (a₁, b₁) Hand.R ≃ dffp (a₂, b₂) Hand.R
Tactic:
exact ‹b₁ ≃ b₂›
State after:
no goals