awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
N : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Fintype ι
inst_6 : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (Ms i) N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
h : i ∉ Finset.univ
⊢ Eq.{u_4 + 1} (α := N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x i) : N ⧸ q)
    (0 : N ⧸ q)
have this : Membership.mem (γ := Finset ι) Finset.univ i
Tactic: have := Finset.mem_univ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
N : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
Ns : ι → Type u_5
inst_5 : (i : ι) → AddCommGroup (Ns i)
inst_6 : (i : ι) → Module.{u_2, u_5} R (Ns i)
p : (i : ι) → Submodule R (Ms i)
f : (i : ι) → LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id R) (Ms i) (Ns i)
hf : ∀ (i : ι), p i ≤ (f i).ker
x : (i : ι) → Ms i
hx : x ∈ pi (φ := Ms) Set.univ p
⊢ Eq (α := (i : ι) → Ns i)
    (((LinearMap.pi (φ := Ns) fun (i : ι) ↦ f i ∘ₗ proj (φ := Ms) i : ((i : ι) → Ms i) →ₗ[R] (i : ι) → Ns i) :
          (a : (i : ι) → Ms i) → (i : ι) → Ns i)
        x :
      (i : ι) → Ns i)
    (0 : (i : ι) → Ns i)
have h : ∀ (i : ι),
  Eq.{u_5 + 1} (α := Ns i)
    (((LinearMap.pi (φ := Ns) fun (i : ι) ↦ f i ∘ₗ proj (φ := Ms) i : ((i : ι) → Ms i) →ₗ[R] (i : ι) → Ns i) :
          (a : (i : ι) → Ms i) → (i : ι) → Ns i)
        x i :
      Ns i)
    (0 i : Ns i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst_3 : Fintype ι
inst_4 : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi (φ := Ms) Set.univ p
x' : (i : ι) → Ms i
⊢ invFun (Ms := Ms) p (toFun (Ms := Ms) p (Quotient.mk x')) = Quotient.mk x'
have dsimp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: dsimp only [toFun, invFun]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Subsingleton M
x y : M
⊢ SameRay R x y
have rw : SameRay R 0 y
Tactic: rw [Subsingleton.elim x 0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
⊢ SameRay R x z
have inl : ∀ (hxy : SameRay R 0 y) (hy : y = 0 → Eq.{u_2 + 1} (α := M) 0 0 ∨ z = 0), SameRay R 0 z
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x, hxy, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
inl : ∀ (hxy : SameRay R 0 y) (hy : y = 0 → Eq.{u_2 + 1} (α := M) 0 0 ∨ z = 0), SameRay R 0 z
⊢ SameRay R x z
have inr : ∀ (hx : x ≠ 0), SameRay R x z
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
⊢ SameRay R x z
have inr : ∀ (hyz : SameRay R y 0) (hy : y = 0 → x = 0 ∨ Eq.{u_2 + 1} (α := M) 0 0), SameRay R x 0
Tactic: rcases eq_or_ne z 0 with (rfl | hz)
Cleared hypotheses: z, hyz, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
inr : ∀ (hyz : SameRay R y 0) (hy : y = 0 → x = 0 ∨ Eq.{u_2 + 1} (α := M) 0 0), SameRay R x 0
⊢ SameRay R x z
have inr₁ : ∀ (hz : z ≠ 0), SameRay R x z
Tactic: rcases eq_or_ne z 0 with (rfl | hz)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
⊢ SameRay R x z
have inr : ∀ (hxy : SameRay R x 0) (hyz : SameRay R 0 z) (hy : Eq.{u_2 + 1} (α := M) 0 0 → x = 0 ∨ z = 0), SameRay R x z
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
Cleared hypotheses: y, hxy, hyz, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
inr : ∀ (hxy : SameRay R x 0) (hyz : SameRay R 0 z) (hy : Eq.{u_2 + 1} (α := M) 0 0 → x = 0 ∨ z = 0), SameRay R x z
⊢ SameRay R x z
have inr₁ : ∀ (hy : y ≠ 0), SameRay R x z
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy_1 : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
⊢ SameRay R x z
have inr : ∀ (r₁ r₂ : R) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (h₁ : r₁ • x = r₂ • y), SameRay R x z
Tactic: rcases hxy.exists_pos hx hy with ⟨r₁, r₂, hr₁, hr₂, h₁⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy_1 : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
⊢ SameRay R x z
have inr : ∀ (r₃ r₄ : R) (hr₃ : 0 < r₃) (hr₄ : 0 < r₄) (h₂ : r₃ • y = r₄ • z), SameRay R x z
Tactic: rcases hyz.exists_pos hy hz with ⟨r₃, r₄, hr₃, hr₄, h₂⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy_1 : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ SameRay R x z
have inr : (r₃ * r₁) • x = (r₂ * r₄) • z
Tactic: refine Or.inr (Or.inr <| ⟨r₃ * r₁, r₂ * r₄, mul_pos hr₃ hr₁, mul_pos hr₂ hr₄, ?_⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy_1 : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ (r₃ * r₁) • x = (r₂ * r₄) • z
have inr : r₃ • r₁ • x = (r₂ * r₄) • z
Tactic: rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy_1 : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
inr : r₃ • r₁ • x = (r₂ * r₄) • z
⊢ (r₃ * r₁) • x = (r₂ * r₄) • z
have inr₁ : r₃ • r₁ • x = r₂ • r₄ • z
Tactic: rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy_1 : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
inr : r₃ • r₁ • x = (r₂ * r₄) • z
inr₁ : r₃ • r₁ • x = r₂ • r₄ • z
⊢ (r₃ * r₁) • x = (r₂ * r₄) • z
have inr₂ : r₃ • r₂ • y = r₂ • r₄ • z
Tactic: rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy_1 : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
inr : r₃ • r₁ • x = (r₂ * r₄) • z
inr₁ : r₃ • r₁ • x = r₂ • r₄ • z
inr₂ : r₃ • r₂ • y = r₂ • r₄ • z
⊢ (r₃ * r₁) • x = (r₂ * r₄) • z
have inr₃ : r₃ • r₂ • y = r₂ • r₃ • y
Tactic: rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy_1 : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
inr : r₃ • r₁ • x = (r₂ * r₄) • z
inr₁ : r₃ • r₁ • x = r₂ • r₄ • z
inr₂ : r₃ • r₂ • y = r₂ • r₄ • z
inr₃ : r₃ • r₂ • y = r₂ • r₃ • y
⊢ (r₃ * r₁) • x = (r₂ * r₄) • z
have inr₄ : r₂ • r₃ • y = r₂ • r₃ • y
Tactic: rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
v : M
h : 0 ≤ a
⊢ SameRay R v (a • v)
have inl : ∀ (h : Eq.{u_1 + 1} (α := R) ((algebraMap S R : (a : S) → R) a : R) (0 : R)), SameRay R v (a • v)
Tactic: obtain h | h := (algebraMap_nonneg R h).eq_or_lt'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
v : M
h : 0 ≤ a
inl : ∀ (h : Eq.{u_1 + 1} (α := R) ((algebraMap S R : (a : S) → R) a : R) (0 : R)), SameRay R v (a • v)
⊢ SameRay R v (a • v)
have inr : ∀ (h : LT.lt.{u_1} (α := R) (0 : R) ((algebraMap S R : (a : S) → R) a : R)), SameRay R v (a • v)
Tactic: obtain h | h := (algebraMap_nonneg R h).eq_or_lt'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
v : M
h_1 : 0 ≤ a
h : Eq.{u_1 + 1} (α := R) ((algebraMap S R : (a : S) → R) a : R) (0 : R)
⊢ SameRay R v (a • v)
have inl : SameRay R v 0
Tactic: rw [← algebraMap_smul R a v, h, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
v : M
h_1 : 0 ≤ a
h : LT.lt.{u_1} (α := R) (0 : R) ((algebraMap S R : (a : S) → R) a : R)
⊢ LT.lt.{u_1} (α := R) 0 1
have inst : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
v : M
h_1 : 0 ≤ a
h : LT.lt.{u_1} (α := R) (0 : R) ((algebraMap S R : (a : S) → R) a : R)
⊢ SameRay R v (a • v)
have inr : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) a : R) v =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (a • v)
Tactic: refine Or.inr <| Or.inr ⟨algebraMap S R a, 1, h, by nontriviality R; exact zero_lt_one, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y : M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
h : SameRay R x y
ha : 0 ≤ a
hy : y = 0
⊢ a • y = 0
have rw : HSMul.hSMul (β := M) a 0 = 0
Tactic: rw [hy, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y : M
S : Type u_5
inst_5 : CommSemiring S
inst_6 : PartialOrder S
inst_7 : Algebra S R
inst_8 : Module S M
inst_9 : SMulPosMono S R
inst_10 : IsScalarTower S R M
a : S
h : SameRay R x y
ha : 0 ≤ a
hy : y = 0
rw : HSMul.hSMul (β := M) a 0 = 0
⊢ a • y = 0
have rw₁ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [hy, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hx : x = 0
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
have rw : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
Tactic: rw [hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hx : x = 0
rw : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
have rw₁ : Eq.{u_3 + 1} (α := N) 0 0
Tactic: rw [hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) y : N) (0 : N)
have rw : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
Tactic: rw [hy, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
rw : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) y : N) (0 : N)
have rw₁ : Eq.{u_3 + 1} (α := N) 0 0
Tactic: rw [hy, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
f : M →ₗ[R] N
h_1 : SameRay R x y
h_2 : ∃ (r₁ : R) (r₂ : R), 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ HSMul.hSMul (β := N) r₁ ((f : (a : M) → N) x : N) = HSMul.hSMul (β := N) r₂ ((f : (a : M) → N) y : N)
have rw : (f : (a : M) → N) (r₁ • x) = HSMul.hSMul (β := N) r₂ ((f : (a : M) → N) y : N)
Tactic: rw [← f.map_smul, ← f.map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
f : M →ₗ[R] N
h_1 : SameRay R x y
h_2 : ∃ (r₁ : R) (r₂ : R), 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
rw : (f : (a : M) → N) (r₁ • x) = HSMul.hSMul (β := N) r₂ ((f : (a : M) → N) y : N)
⊢ HSMul.hSMul (β := N) r₁ ((f : (a : M) → N) x : N) = HSMul.hSMul (β := N) r₂ ((f : (a : M) → N) y : N)
have rw₁ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (r₁ • x) : N) ((f : (a : M) → N) (r₂ • y) : N)
Tactic: rw [← f.map_smul, ← f.map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
x y : M
f : M →ₗ[R] N
h_1 : SameRay R x y
h_2 : ∃ (r₁ : R) (r₂ : R), 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
rw : (f : (a : M) → N) (r₁ • x) = HSMul.hSMul (β := N) r₂ ((f : (a : M) → N) y : N)
rw₁ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (r₁ • x) : N) ((f : (a : M) → N) (r₂ • y) : N)
⊢ HSMul.hSMul (β := N) r₁ ((f : (a : M) → N) x : N) = HSMul.hSMul (β := N) r₂ ((f : (a : M) → N) y : N)
have rw₂ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (r₂ • y) : N) ((f : (a : M) → N) (r₂ • y) : N)
Tactic: rw [← f.map_smul, ← f.map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
⊢ SameRay R (x + y) z
have inl : ∀ (hx : SameRay R 0 z), SameRay R (0 + y) z
Tactic: rcases eq_or_ne x 0 with (rfl | hx₀)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
inl : ∀ (hx : SameRay R 0 z), SameRay R (0 + y) z
⊢ SameRay R (x + y) z
have inr : ∀ (hx₀ : x ≠ 0), SameRay R (x + y) z
Tactic: rcases eq_or_ne x 0 with (rfl | hx₀)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
⊢ SameRay R (x + y) z
have inr : ∀ (hy : SameRay R 0 z), SameRay R (x + 0) z
Tactic: rcases eq_or_ne y 0 with (rfl | hy₀)
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
inr : ∀ (hy : SameRay R 0 z), SameRay R (x + 0) z
⊢ SameRay R (x + y) z
have inr₁ : ∀ (hy₀ : y ≠ 0), SameRay R (x + y) z
Tactic: rcases eq_or_ne y 0 with (rfl | hy₀)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ SameRay R (x + y) z
have inr : ∀ (hx : SameRay R x 0) (hy : SameRay R y 0), SameRay R (x + y) 0
Tactic: rcases eq_or_ne z 0 with (rfl | hz₀)
Cleared hypotheses: z, hx, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
inr : ∀ (hx : SameRay R x 0) (hy : SameRay R y 0), SameRay R (x + y) 0
⊢ SameRay R (x + y) z
have inr₁ : ∀ (hz₀ : z ≠ 0), SameRay R (x + y) z
Tactic: rcases eq_or_ne z 0 with (rfl | hz₀)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
⊢ SameRay R (x + y) z
have inr : ∀ (rx rz₁ : R) (hrx : 0 < rx) (hrz₁ : 0 < rz₁) (Hx : rx • x = rz₁ • z), SameRay R (x + y) z
Tactic: rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
⊢ SameRay R (x + y) z
have inr : ∀ (ry rz₂ : R) (hry : 0 < ry) (hrz₂ : 0 < rz₂) (Hy : ry • y = rz₂ • z), SameRay R (x + y) z
Tactic: rcases hy.exists_pos hy₀ hz₀ with ⟨ry, rz₂, hry, hrz₂, Hy⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ SameRay R (x + y) z
have inr : 0 < ry * rz₁ + rx * rz₂
Tactic: refine Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
inr : 0 < ry * rz₁ + rx * rz₂
⊢ SameRay R (x + y) z
have inr₁ : (rx * ry) • (x + y) = (ry * rz₁ + rx * rz₂) • z
Tactic: refine Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Ray (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (rx * ry) • (x + y) = (ry * rz₁ + rx * rz₂) • z
have h : (rx * ry) • (x + y) = ry • rx • x + rx • ry • y
Tactic: convert! congr(ry • $Hx + rx • $Hy) using 1