Theorem: FreeModule.eq_of_beq_true (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₂ = true → x₁ = x₂
Tactic:
apply Quotient.ind₂ (motive := fun (x₁ x₂ : R[X]) => x₁.beq_quot x₂ = true → 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) = true →
      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) = true →
      Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) b
Tactic:
intro s₁ s₂ eqv
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
eqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = true
⊢ 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
eqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = true
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
let eql := of_decide_eq_true eqv
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
eqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = true
eql : Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂ := of_decide_eq_true eqv
⊢ 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
eqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = true
eql : Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂ := of_decide_eq_true eqv
⊢ Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂
Tactic:
assumption
State after:
no goals