awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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
⊢ Membership.mem (γ := Finset ι) Finset.univ i

Tactic:
have := Finset.mem_univ i
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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
this : Membership.mem (γ := Finset ι) Finset.univ i
⊢ 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)

Tactic:
contradiction
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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
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)
⊢ 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)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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
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:
simpa using hf i (mem_pi.mp hx i (Set.mem_univ i))

Premises used: Submodule.mem_pi, Iff.mp, Set.mem_univ
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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)
Ns : ι → Type u_5
inst_3 : (i : ι) → AddCommGroup (Ns i)
inst_4 : (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
⊢ Eq (α := (i : ι) → Ns i)
    ((quotientPiLift (Ms := Ms) (Ns := Ns) p f hf : (a : ((i : ι) → Ms i) ⧸ pi Set.univ p) → (i : ι) → Ns i)
        (Quotient.mk x) :
      (i : ι) → Ns i)
    fun (i : ι) ↦ ((f i : (a : Ms i) → Ns i) (x i) : Ns i)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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)
x y : ((i : ι) → Ms i) ⧸ pi (φ := Ms) Set.univ p
⊢ toFun (Ms := Ms) p (x + y) = toFun (Ms := Ms) p x + toFun (Ms := Ms) p y

Tactic:
LinearMap.map_add (quotientPiLift p (fun i => (p i).mkQ) fun i => (ker_mkQ (p i)).ge) x y

Premises used: LinearMap.map_add, Submodule.quotientPi_aux.toFun, Eq.ge, Submodule.mkQ, Submodule.ker_mkQ, Submodule.quotientPiLift
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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)
r : R
x : ((i : ι) → Ms i) ⧸ pi (φ := Ms) Set.univ p
⊢ toFun (Ms := Ms) p (r • x) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (toFun (Ms := Ms) p x)

Tactic:
LinearMap.map_smul (quotientPiLift p (fun i => (p i).mkQ) fun i => (ker_mkQ (p i)).ge) r x

Premises used: Submodule.quotientPi_aux.toFun, Eq.ge, LinearMap.map_smul, Submodule.mkQ, Submodule.ker_mkQ, Submodule.quotientPiLift
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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
dsimp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ invFun (Ms := Ms) p (toFun (Ms := Ms) p (Quotient.mk x')) = Quotient.mk x'

Tactic:
dsimp only [toFun, invFun]

Premises used: Submodule.quotientPi_aux.toFun, Submodule.quotientPi_aux.invFun
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
M : Type u_2
inst : Zero M
v : M
h : v ≠ 0
⊢ (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 })
          ((Equiv.symm (equiv R M) : (a : { v : M // v ≠ 0 }) → RayVector R M)
            (Subtype.mk (p := fun (v : M) ↦ v ≠ 0) v h))) :
      M) =
    v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
M : Type u_2
inst : Zero M
x y : RayVector R M
h :
  Eq.{u_2 + 1} (α := M) (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) x) : M)
    (↑((equiv R M : (a : RayVector R M) → { v : M // v ≠ 0 }) y) : M)
⊢ x = y

Tactic:
Subtype.ext h

Premises used: Subtype.ext, RayVector
-- Module: Mathlib.LinearAlgebra.Ray
Goal:
R : Type u_1
M : Type u_2
inst : Zero M
inst_1 : Nontrivial M
⊢ Nonempty.{u_2 + 1} (RayVector R M)

Tactic:
⟨Classical.indefiniteDescription _ <| exists_ne (0 : M)⟩

Premises used: Classical.indefiniteDescription, exists_ne, Nonempty.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Ray
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
y : M
⊢ SameRay R 0 y

Tactic:
Or.inl rfl

Premises used: SameRay, Or.inl, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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 : M
⊢ SameRay R x 0

Tactic:
Or.inr <| Or.inl rfl

Premises used: SameRay, Or.inl, Or.inr, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
rw : SameRay R 0 y
⊢ SameRay R x y

Tactic:
rw [Subsingleton.elim x 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Ray
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 0 y

Tactic:
zero_left _

Premises used: SameRay.zero_left
-- Module: Mathlib.LinearAlgebra.Ray
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 0 y

Tactic:
exact zero_left _

Premises used: SameRay.zero_left
-- Module: Mathlib.LinearAlgebra.Ray
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 R
x y : M
⊢ SameRay R x y

Tactic:
haveI := Module.subsingleton R M
  of_subsingleton x y

Premises used: SameRay.of_subsingleton
-- Module: Mathlib.LinearAlgebra.Ray
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 : M
⊢ SameRay R x x

Tactic:
Or.inr (Or.inr <| ⟨1, 1, zero_lt_one, zero_lt_one, rfl⟩)

Premises used: zero_lt_one, And.intro, Exists.intro, SameRay, OfNat.ofNat, Or.inr, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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 : M
⊢ SameRay R x x

Tactic:
refl _

Premises used: SameRay.refl
-- Module: Mathlib.LinearAlgebra.Ray
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
h : SameRay R x y
⊢ SameRay R y x

Tactic:
(or_left_comm.1 h).imp_right <| Or.imp_right fun ⟨r₁, r₂, h₁, h₂, h⟩ => ⟨r₂, r₁, h₂, h₁, h.symm⟩

Premises used: or_left_comm, Iff.mp, SameRay, Or.imp_right
-- Module: Mathlib.LinearAlgebra.Ray
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
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ (r₁ : R) (r₂ : R), 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y

Tactic:
(h.resolve_left hx).resolve_left hy

Premises used: Or.resolve_left
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ SameRay R x y ↔ SameRay R y x

Tactic:
⟨SameRay.symm, SameRay.symm⟩

Premises used: SameRay.symm, Iff.intro
-- Module: Mathlib.LinearAlgebra.Ray
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
inr : ∀ (hx : x ≠ 0), SameRay R x z
⊢ SameRay R x z

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
y z : M
hyz : SameRay R y z
hxy : SameRay R 0 y
hy : y = 0 → Eq.{u_2 + 1} (α := M) 0 0 ∨ z = 0
⊢ SameRay R 0 z

Tactic:
zero_left z

Premises used: SameRay.zero_left
-- Module: Mathlib.LinearAlgebra.Ray
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
y z : M
hyz : SameRay R y z
hxy : SameRay R 0 y
hy : y = 0 → Eq.{u_2 + 1} (α := M) 0 0 ∨ z = 0
⊢ SameRay R 0 z

Tactic:
exact zero_left z

Premises used: SameRay.zero_left
-- Module: Mathlib.LinearAlgebra.Ray
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
inr₁ : ∀ (hz : z ≠ 0), SameRay R x z
⊢ SameRay R x z

Tactic:
rcases eq_or_ne z 0 with (rfl | hz)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
hxy : SameRay R x y
hx : x ≠ 0
hyz : SameRay R y 0
hy : y = 0 → x = 0 ∨ Eq.{u_2 + 1} (α := M) 0 0
⊢ SameRay R x 0

Tactic:
zero_right x

Premises used: SameRay.zero_right
-- Module: Mathlib.LinearAlgebra.Ray
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
hxy : SameRay R x y
hx : x ≠ 0
hyz : SameRay R y 0
hy : y = 0 → x = 0 ∨ Eq.{u_2 + 1} (α := M) 0 0
⊢ SameRay R x 0

Tactic:
exact zero_right x

Premises used: SameRay.zero_right
-- Module: Mathlib.LinearAlgebra.Ray
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
inr₁ : ∀ (hy : y ≠ 0), SameRay R x z
⊢ SameRay R x z

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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 z : M
hx : x ≠ 0
hz : z ≠ 0
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:
(hy rfl).elim (fun h => (hx h).elim) fun h => (hz h).elim

Premises used: False.elim, Or.elim, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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 z : M
hx : x ≠ 0
hz : z ≠ 0
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:
exact (hy rfl).elim (fun h => (hx h).elim) fun h => (hz h).elim

Premises used: False.elim, Or.elim, rfl
-- Module: Mathlib.LinearAlgebra.Ray
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
inr : ∀ (r₁ r₂ : R) (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (h₁ : r₁ • x = r₂ • y), SameRay R x z
⊢ SameRay R x z

Tactic:
rcases hxy.exists_pos hx hy with ⟨r₁, r₂, hr₁, hr₂, h₁⟩

Premises used: SameRay.exists_pos
-- Module: Mathlib.LinearAlgebra.Ray
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
inr : ∀ (r₃ r₄ : R) (hr₃ : 0 < r₃) (hr₄ : 0 < r₄) (h₂ : r₃ • y = r₄ • z), SameRay R x z
⊢ SameRay R x z

Tactic:
rcases hyz.exists_pos hy hz with ⟨r₃, r₄, hr₃, hr₄, h₂⟩

Premises used: SameRay.exists_pos
-- Module: Mathlib.LinearAlgebra.Ray
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

Tactic:
Or.inr (Or.inr <| ⟨r₃ * r₁, r₂ * r₄, mul_pos hr₃ hr₁, mul_pos hr₂ hr₄, ?_⟩)

Premises used: HMul.hMul, mul_pos, And.intro, Exists.intro, SameRay, Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
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
⊢ SameRay R x z

Tactic:
refine Or.inr (Or.inr <| ⟨r₃ * r₁, r₂ * r₄, mul_pos hr₃ hr₁, mul_pos hr₂ hr₄, ?_⟩)

Premises used: Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
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
inr₄ inr₅ : r₂ • r₃ • y = r₂ • r₃ • y
⊢ (r₃ * r₁) • x = (r₂ * r₄) • z

Tactic:
rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]

Premises used: SMulCommClass.smul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Ray
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)
inr : ∀ (h : LT.lt.{u_1} (α := R) (0 : R) ((algebraMap S R : (a : S) → R) a : R)), SameRay R v (a • v)
⊢ SameRay R v (a • v)

Tactic:
obtain h | h := (algebraMap_nonneg R h).eq_or_lt'

Premises used: algebraMap_nonneg, LE.le.eq_or_lt'
-- Module: Mathlib.LinearAlgebra.Ray
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)
inl : SameRay R v 0
⊢ SameRay R v (a • v)

Tactic:
rw [← algebraMap_smul R a v, h, zero_smul]

Premises used: algebraMap_smul, zero_smul
-- Module: Mathlib.LinearAlgebra.Ray
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 0

Tactic:
zero_right _

Premises used: SameRay.zero_right
-- Module: Mathlib.LinearAlgebra.Ray
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 0

Tactic:
exact zero_right _

Premises used: SameRay.zero_right
-- Module: Mathlib.LinearAlgebra.Ray
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)
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Ray
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)
inst_11 : Nontrivial R
⊢ LT.lt.{u_1} (α := R) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.LinearAlgebra.Ray
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)
inst_11 : Nontrivial R
⊢ LT.lt.{u_1} (α := R) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.LinearAlgebra.Ray
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)
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)
⊢ SameRay R v (a • v)

Tactic:
refine Or.inr <| Or.inr ⟨algebraMap S R a, 1, h, by nontriviality R; exact zero_lt_one, ?_⟩

Premises used: Or.inr
-- Module: Mathlib.LinearAlgebra.Ray
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)
⊢ 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:
module
-- Module: Mathlib.LinearAlgebra.Ray
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
ha : 0 ≤ a
⊢ SameRay R (a • v) v

Tactic:
(sameRay_nonneg_smul_right v ha).symm

Premises used: SameRay.symm, SameRay.sameRay_nonneg_smul_right
-- Module: Mathlib.LinearAlgebra.Ray
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
ha : 0 < a
⊢ SameRay R v (a • v)

Tactic:
sameRay_nonneg_smul_right v ha.le

Premises used: LT.lt.le, SameRay.sameRay_nonneg_smul_right
-- Module: Mathlib.LinearAlgebra.Ray
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
ha : 0 < a
⊢ SameRay R (a • v) v

Tactic:
sameRay_nonneg_smul_left v ha.le

Premises used: SameRay.sameRay_nonneg_smul_left, LT.lt.le