Theorem: FormalSum.func_eql_of_move_equiv (UnitConjecture/FreeModule.lean)

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
⊢ (∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂) → ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Tactic:
intro hyp
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Tactic:
let fbar : FreeModuleAux R X → β := Quot.lift f hyp
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Tactic:
let fct : ∀ s : FormalSum R X, f s = fbar (sum s) := by
  apply Quot.liftBeta
  apply hyp
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
⊢ ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂
Tactic:
intro s₁ s₂ sim
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
⊢ f s₁ = f s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
⊢ f s₁ = f s₂
Tactic:
have ec : eqlCoords R X s₁ s₂ := sim
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : eqlCoords R X s₁ s₂
⊢ f s₁ = f s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : eqlCoords R X s₁ s₂
⊢ f s₁ = f s₂
Tactic:
rw [eqlCoords] at ec
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ f s₁ = f s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ f s₁ = f s₂
Tactic:
have pullback : sum s₁ = sum s₂ := by
  apply equiv_of_equal_coeffs
  intro x
  exact congrFun ec x
State after:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
pullback : sum s₁ = sum s₂
⊢ f s₁ = f s₂

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
pullback : sum s₁ = sum s₂
⊢ f s₁ = f s₂
Tactic:
simp [fct, pullback]
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (s : FormalSum R X), f s = fbar (sum s)
Tactic:
apply Quot.liftBeta
State after:
case c
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (a b : FormalSum R X), ?r a b → f a = f b

case r
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ FormalSum R X → FormalSum R X → Prop

State before:
case c
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ ∀ (a b : FormalSum R X), ?r a b → f a = f b

case r
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
⊢ FormalSum R X → FormalSum R X → Prop
Tactic:
apply hyp
State after:
no goals

State before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ sum s₁ = sum s₂
Tactic:
apply equiv_of_equal_coeffs
State after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ ∀ (x : X), coords s₁ x = coords s₂ x

State before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
⊢ ∀ (x : X), coords s₁ x = coords s₂ x
Tactic:
intro x
State after:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
x : X
⊢ coords s₁ x = coords s₂ x

State before:
case hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
β : Sort u
f : FormalSum R X → β
hyp : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂
fbar : FreeModuleAux R X → β := Quot.lift f hyp
fct : ∀ (s : FormalSum R X), f s = fbar (sum s) := Quot.liftBeta (fun a => f a) hyp
s₁ s₂ : FormalSum R X
sim : s₁ ≈ s₂
ec : coords s₁ = coords s₂
x : X
⊢ coords s₁ x = coords s₂ x
Tactic:
exact congrFun ec x
State after:
no goals