Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_impossible (Lean4Axiomatic/Rational/Impl/Fraction/Naive.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ¬∀ (p q r : Fraction ℤ), p ≃ q → q ≃ r → p ≃ r
Tactic:
intro (trans : {p q r : Naive.Fraction ℤ} → p ≃ q → q ≃ r → p ≃ r)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
⊢ False
Tactic:
let p : Naive.Fraction ℤ := 1//0
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
⊢ False
Tactic:
let q : Naive.Fraction ℤ := 0//0
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
⊢ False
Tactic:
let r : Naive.Fraction ℤ := 1//1
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ False
Tactic:
have : p ≃ q := by
  show 1//0 ≃ 0//0
  show 1 * 0 ≃ 0 * 0
  calc
    (1 : ℤ) * 0 ≃ _ := AA.absorbR
    0           ≃ _ := Rel.symm AA.absorbR
    0 * 0       ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ False
Tactic:
have : q ≃ r := by
  show 0//0 ≃ 1//1
  show 0 * 1 ≃ 1 * 0
  exact AA.comm
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
⊢ False
Tactic:
have : p ≄ r := by
  intro (_ : p ≃ r)
  show False
  have : (1 : ℤ)//0 ≃ 1//1 := ‹p ≃ r›
  have : (1 : ℤ) * 1 ≃ 1 * 0 := ‹(1 : ℤ)//0 ≃ 1//1›
  have : (1 : ℤ) ≃ 0 := calc
    (1 : ℤ) ≃ _ := Rel.symm AA.identR
    1 * 1   ≃ _ := ‹(1 : ℤ) * 1 ≃ 1 * 0›
    1 * 0   ≃ _ := AA.absorbR
    0       ≃ _ := Rel.refl
  have : (1 : ℤ) ≄ 0 := Integer.one_neqv_zero
  exact absurd ‹(1 : ℤ) ≃ 0› ‹(1 : ℤ) ≄ 0›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝¹ : p ≃ q
this✝ : q ≃ r
this : p ≄ r
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝¹ : p ≃ q
this✝ : q ≃ r
this : p ≄ r
⊢ False
Tactic:
have : p ≃ r := trans ‹p ≃ q› ‹q ≃ r›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝² : p ≃ q
this✝¹ : q ≃ r
this✝ : p ≄ r
this : p ≃ r
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝² : p ≃ q
this✝¹ : q ≃ r
this✝ : p ≄ r
this : p ≃ r
⊢ False
Tactic:
exact absurd ‹p ≃ r› ‹p ≄ r›
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ p ≃ q
Tactic:
show 1//0 ≃ 0//0
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ 1//0 ≃ 0//0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ 1//0 ≃ 0//0
Tactic:
show 1 * 0 ≃ 0 * 0
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ 1 * 0 ≃ 0 * 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
⊢ 1 * 0 ≃ 0 * 0
Tactic:
calc
  (1 : ℤ) * 0 ≃ _ := AA.absorbR
  0           ≃ _ := Rel.symm AA.absorbR
  0 * 0       ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ q ≃ r
Tactic:
show 0//0 ≃ 1//1
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ 0//0 ≃ 1//1

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ 0//0 ≃ 1//1
Tactic:
show 0 * 1 ≃ 1 * 0
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ 0 * 1 ≃ 1 * 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this : p ≃ q
⊢ 0 * 1 ≃ 1 * 0
Tactic:
exact AA.comm
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
⊢ p ≄ r
Tactic:
intro (_ : p ≃ r)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
x✝ : p ≃ r
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝ : p ≃ q
this : q ≃ r
x✝ : p ≃ r
⊢ False
Tactic:
have : (1 : ℤ)//0 ≃ 1//1 := ‹p ≃ r›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝¹ : p ≃ q
this✝ : q ≃ r
x✝ : p ≃ r
this : 1//0 ≃ 1//1
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝¹ : p ≃ q
this✝ : q ≃ r
x✝ : p ≃ r
this : 1//0 ≃ 1//1
⊢ False
Tactic:
have : (1 : ℤ) * 1 ≃ 1 * 0 := ‹(1 : ℤ)//0 ≃ 1//1›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝² : p ≃ q
this✝¹ : q ≃ r
x✝ : p ≃ r
this✝ : 1//0 ≃ 1//1
this : 1 * 1 ≃ 1 * 0
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝² : p ≃ q
this✝¹ : q ≃ r
x✝ : p ≃ r
this✝ : 1//0 ≃ 1//1
this : 1 * 1 ≃ 1 * 0
⊢ False
Tactic:
have : (1 : ℤ) ≃ 0 := calc
  (1 : ℤ) ≃ _ := Rel.symm AA.identR
  1 * 1   ≃ _ := ‹(1 : ℤ) * 1 ≃ 1 * 0›
  1 * 0   ≃ _ := AA.absorbR
  0       ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝³ : p ≃ q
this✝² : q ≃ r
x✝ : p ≃ r
this✝¹ : 1//0 ≃ 1//1
this✝ : 1 * 1 ≃ 1 * 0
this : 1 ≃ 0
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝³ : p ≃ q
this✝² : q ≃ r
x✝ : p ≃ r
this✝¹ : 1//0 ≃ 1//1
this✝ : 1 * 1 ≃ 1 * 0
this : 1 ≃ 0
⊢ False
Tactic:
have : (1 : ℤ) ≄ 0 := Integer.one_neqv_zero
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝⁴ : p ≃ q
this✝³ : q ≃ r
x✝ : p ≃ r
this✝² : 1//0 ≃ 1//1
this✝¹ : 1 * 1 ≃ 1 * 0
this✝ : 1 ≃ 0
this : 1 ≄ 0
⊢ False

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
trans : ∀ {p q r : Fraction ℤ}, p ≃ q → q ≃ r → p ≃ r
p : Fraction ℤ := 1//0
q : Fraction ℤ := 0//0
r : Fraction ℤ := 1//1
this✝⁴ : p ≃ q
this✝³ : q ≃ r
x✝ : p ≃ r
this✝² : 1//0 ≃ 1//1
this✝¹ : 1 * 1 ≃ 1 * 0
this✝ : 1 ≃ 0
this : 1 ≄ 0
⊢ False
Tactic:
exact absurd ‹(1 : ℤ) ≃ 0› ‹(1 : ℤ) ≄ 0›
State after:
no goals