internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.symm
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g : (x : α) → β x
x✝ : ∀ (x : α), f x ≃ g x
⊢ g ≃ f
Tactic:
show ∀ (x : α), g x ≃ f x
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g : (x : α) → β x
x✝ : ∀ (x : α), f x ≃ g x
⊢ ∀ (x : α), g x ≃ f x
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.symm
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g : (x : α) → β x
x✝ : ∀ (x : α), f x ≃ g x
⊢ ∀ (x : α), g x ≃ f x
Tactic:
intro x
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g : (x : α) → β x
x✝ : ∀ (x : α), f x ≃ g x
x : α
⊢ g x ≃ f x
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.symm
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g : (x : α) → β x
x✝ : ∀ (x : α), f x ≃ g x
x : α
⊢ g x ≃ f x
Tactic:
have : f x ≃ g x := ‹∀ (x : α), f x ≃ g x› x
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g : (x : α) → β x
x✝ : ∀ (x : α), f x ≃ g x
x : α
this : f x ≃ g x
⊢ g x ≃ f x
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.symm
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g : (x : α) → β x
x✝ : ∀ (x : α), f x ≃ g x
x : α
this : f x ≃ g x
⊢ g x ≃ f x
Tactic:
exact indexed_eqvOp.symm ‹f x ≃ g x›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.trans
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
⊢ f ≃ g → g ≃ h → f ≃ h
Tactic:
intro (_ : ∀ (x : α), f x ≃ g x) (_ : ∀ (x : α), g x ≃ h x)
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
⊢ f ≃ h
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.trans
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
⊢ f ≃ h
Tactic:
show ∀ (x : α), f x ≃ h x
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
⊢ ∀ (x : α), f x ≃ h x
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.trans
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
⊢ ∀ (x : α), f x ≃ h x
Tactic:
intro x
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
⊢ f x ≃ h x
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.trans
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
⊢ f x ≃ h x
Tactic:
have : f x ≃ g x := ‹∀ (x : α), f x ≃ g x› x
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
this : f x ≃ g x
⊢ f x ≃ h x
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.trans
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
this : f x ≃ g x
⊢ f x ≃ h x
Tactic:
have : g x ≃ h x := ‹∀ (x : α), g x ≃ h x› x
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
this✝ : f x ≃ g x
this : g x ≃ h x
⊢ f x ≃ h x
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.trans
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
this✝ : f x ≃ g x
this : g x ≃ h x
⊢ f x ≃ h x
Tactic:
exact indexed_eqvOp.trans ‹f x ≃ g x› ‹g x ≃ h x›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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
Proof 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₂
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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
Proof 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₂
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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
Proof 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₂)
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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₂))
Proof 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₂
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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₂)›
Proof 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₂
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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
Proof 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₂
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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
Proof 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₂
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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₂))
Proof 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₂)
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.Prod.eqv_defn
Proof 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₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_subst
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
⊢ a₁ ≃ a₂ → Sqrt1 a₁ → Sqrt1 a₂
Tactic:
intro (_ : a₁ ≃ a₂) (_ : Sqrt1 a₁)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Sqrt1 a₁
⊢ Sqrt1 a₂
Theorem: Lean4Axiomatic.Integer.sqrt1_subst
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Sqrt1 a₁
⊢ Sqrt1 a₂
Tactic:
have : a₂ * a₂ ≃ 1 := calc
  a₂ * a₂ ≃ _ := AA.substL (Rel.symm ‹a₁ ≃ a₂›)
  a₁ * a₂ ≃ _ := AA.substR (Rel.symm ‹a₁ ≃ a₂›)
  a₁ * a₁ ≃ _ := ‹Sqrt1 a₁›.elim
  1       ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Sqrt1 a₁
this : a₂ * a₂ ≃ 1
⊢ Sqrt1 a₂
Theorem: Lean4Axiomatic.Integer.sqrt1_subst
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : Sqrt1 a₁
this : a₂ * a₂ ≃ 1
⊢ Sqrt1 a₂
Tactic:
exact Sqrt1.mk ‹a₂ * a₂ ≃ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.one_mul_one_eqv_one
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
⊢ 1 * 1 ≃ 1
Tactic:
exact AA.identL
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.neg_one_mul_neg_one_eqv_one
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
⊢ -1 * -1 ≃ 1
Tactic:
calc
  (-1 : ℤ) * (-1) ≃ _ := Rel.symm AA.scompatL
  (-(1 * (-1)))   ≃ _ := AA.subst₁ (Rel.symm AA.scompatR)
  (-(-(1 * 1)))   ≃ _ := neg_involutive
  1 * 1           ≃ _ := one_mul_one_eqv_one
  1               ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.NonzeroWithSign.subst_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ s : ℤ
x✝ : Sqrt1 s
⊢ a₁ ≃ a₂ → NonzeroWithSign a₁ s → NonzeroWithSign a₂ s
Tactic:
intro (_ : a₁ ≃ a₂)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ s : ℤ
x✝¹ : Sqrt1 s
x✝ : a₁ ≃ a₂
⊢ NonzeroWithSign a₁ s → NonzeroWithSign a₂ s
Theorem: Lean4Axiomatic.Integer.NonzeroWithSign.subst_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ s : ℤ
x✝¹ : Sqrt1 s
x✝ : a₁ ≃ a₂
⊢ NonzeroWithSign a₁ s → NonzeroWithSign a₂ s
Tactic:
intro (NonzeroWithSign.intro (m : ℕ) (_ : Positive m) (_ : a₁ ≃ s * coe m))
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ s : ℤ
x✝¹ : Sqrt1 s
x✝ : a₁ ≃ a₂
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ s * coe m
⊢ NonzeroWithSign a₂ s
Theorem: Lean4Axiomatic.Integer.NonzeroWithSign.subst_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ s : ℤ
x✝¹ : Sqrt1 s
x✝ : a₁ ≃ a₂
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ s * coe m
⊢ NonzeroWithSign a₂ s
Tactic:
have : a₂ ≃ s * coe m := Rel.trans (Rel.symm ‹a₁ ≃ a₂›) ‹a₁ ≃ s * coe m›
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ s : ℤ
x✝¹ : Sqrt1 s
x✝ : a₁ ≃ a₂
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ s * coe m
this : a₂ ≃ s * coe m
⊢ NonzeroWithSign a₂ s
Theorem: Lean4Axiomatic.Integer.NonzeroWithSign.subst_nonzero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ s : ℤ
x✝¹ : Sqrt1 s
x✝ : a₁ ≃ a₂
m : ℕ
pos✝ : Positive m
eqv✝ : a₁ ≃ s * coe m
this : a₂ ≃ s * coe m
⊢ NonzeroWithSign a₂ s
Tactic:
exact NonzeroWithSign.intro m ‹Positive m› ‹a₂ ≃ s * coe m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.NonzeroWithSign.subst_sign
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s₁ s₂ : ℤ
x✝² : Sqrt1 s₁
x✝¹ : Sqrt1 s₂
x✝ : s₁ ≃ s₂
⊢ NonzeroWithSign a s₁ → NonzeroWithSign a s₂
Tactic:
intro (NonzeroWithSign.intro (m : ℕ) (_ : Positive m) (_ : a ≃ s₁ * coe m))
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s₁ s₂ : ℤ
x✝² : Sqrt1 s₁
x✝¹ : Sqrt1 s₂
x✝ : s₁ ≃ s₂
m : ℕ
pos✝ : Positive m
eqv✝ : a ≃ s₁ * coe m
⊢ NonzeroWithSign a s₂
Theorem: Lean4Axiomatic.Integer.NonzeroWithSign.subst_sign
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s₁ s₂ : ℤ
x✝² : Sqrt1 s₁
x✝¹ : Sqrt1 s₂
x✝ : s₁ ≃ s₂
m : ℕ
pos✝ : Positive m
eqv✝ : a ≃ s₁ * coe m
⊢ NonzeroWithSign a s₂
Tactic:
have : a ≃ s₂ * coe m := Rel.trans ‹a ≃ s₁ * coe m› (AA.substL ‹s₁ ≃ s₂›)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s₁ s₂ : ℤ
x✝² : Sqrt1 s₁
x✝¹ : Sqrt1 s₂
x✝ : s₁ ≃ s₂
m : ℕ
pos✝ : Positive m
eqv✝ : a ≃ s₁ * coe m
this : a ≃ s₂ * coe m
⊢ NonzeroWithSign a s₂
Theorem: Lean4Axiomatic.Integer.NonzeroWithSign.subst_sign
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s₁ s₂ : ℤ
x✝² : Sqrt1 s₁
x✝¹ : Sqrt1 s₂
x✝ : s₁ ≃ s₂
m : ℕ
pos✝ : Positive m
eqv✝ : a ≃ s₁ * coe m
this : a ≃ s₂ * coe m
⊢ NonzeroWithSign a s₂
Tactic:
exact NonzeroWithSign.intro m ‹Positive m› ‹a ≃ s₂ * coe m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
⊢ NonzeroWithSign a as → NonzeroWithSign b bs → NonzeroWithSign (a * b) (as * bs)
Tactic:
intro
  (NonzeroWithSign.intro (am : ℕ) (_ : Positive am) (_ : a ≃ as * coe am))
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝ : Positive am
eqv✝ : a ≃ as * coe am
⊢ NonzeroWithSign b bs → NonzeroWithSign (a * b) (as * bs)
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝ : Positive am
eqv✝ : a ≃ as * coe am
⊢ NonzeroWithSign b bs → NonzeroWithSign (a * b) (as * bs)
Tactic:
intro
  (NonzeroWithSign.intro (bm : ℕ) (_ : Positive bm) (_ : b ≃ bs * coe bm))
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
⊢ NonzeroWithSign (a * b) (as * bs)
Theorem: Lean4Axiomatic.Integer.mul_preserves_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
⊢ NonzeroWithSign (a * b) (as * bs)
Tactic:
have : Positive (am * bm) := Natural.mul_positive ‹Positive am› ‹Positive bm›
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
this : Positive (am * bm)
⊢ NonzeroWithSign (a * b) (as * bs)