Theorem: SciLean.Tactic.GTrans.HAdd.hAdd.arg_a0a1.ParametricRightInverse_rule (SciLean/Tactic/GTrans/Test.lean)

State before:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
⊢ ParametricRightInverse (fun xy => xy.1 + xy.2) α fun a z => ((1 / 2) • z + a, (1 / 2) • z - a)
Tactic:
unfold ParametricRightInverse
State after:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
⊢ ∀ (y c : α), (fun xy => xy.1 + xy.2) ((fun a z => ((1 / 2) • z + a, (1 / 2) • z - a)) c y) = y

State before:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
⊢ ∀ (y c : α), (fun xy => xy.1 + xy.2) ((fun a z => ((1 / 2) • z + a, (1 / 2) • z - a)) c y) = y
Tactic:
intros
State after:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
y✝ c✝ : α
⊢ (fun xy => xy.1 + xy.2) ((fun a z => ((1 / 2) • z + a, (1 / 2) • z - a)) c✝ y✝) = y✝

State before:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
y✝ c✝ : α
⊢ (fun xy => xy.1 + xy.2) ((fun a z => ((1 / 2) • z + a, (1 / 2) • z - a)) c✝ y✝) = y✝
Tactic:
simp
State after:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
y✝ c✝ : α
⊢ 2⁻¹ • y✝ + 2⁻¹ • y✝ = y✝

State before:
α : Type
inst✝¹ : AddCommGroup α
inst✝ : _root_.Module ℚ α
y✝ c✝ : α
⊢ 2⁻¹ • y✝ + 2⁻¹ • y✝ = y✝
Tactic:
sorry_proof
State after:
no goals