Theorem: FreeModule.neq_of_beq_false (UnitConjecture/FreeModule.lean)

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (x₁ x₂ : R[X]), beq_quot x₁ x₂ = false → ¬x₁ = x₂
Tactic:
apply Quotient.ind₂ (motive := fun (x₁ x₂ : R[X]) => x₁.beq_quot x₂ = false → Not (x₁ = x₂))
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (a b : FormalSum R X),
    beq_quot (Quotient.mk (formalSumSetoid R X) a) (Quotient.mk (formalSumSetoid R X) b) = false →
      ¬Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) b

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (a b : FormalSum R X),
    beq_quot (Quotient.mk (formalSumSetoid R X) a) (Quotient.mk (formalSumSetoid R X) b) = false →
      ¬Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) b
Tactic:
intro s₁ s₂ neqv
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
let neql := of_decide_eq_false neqv
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
neql : ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂ := of_decide_eq_false neqv
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
neql : ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂ := of_decide_eq_false neqv
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
assumption
State after:
no goals