awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
h : ¬a ∈ s
h_1 : 1 ∈ s
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (∅ ∪ Uᶜ)

Tactic:
simp
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
h : ¬a ∈ s
h_1 : ¬1 ∈ s
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (∅ ∪ ∅)

Tactic:
simp
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
rw rw₁ rw₂ : Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅)
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((U.mulIndicator fun (x : α) ↦ a) ⁻¹' s)

Tactic:
classical
    rw [mulIndicator_const_preimage_eq_union]
    split_ifs <;> simp

Premises used: Set.mulIndicator_const_preimage_eq_union
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
t : Set M
ht : ¬1 ∈ t
⊢ s.mulIndicator f ⁻¹' t = f ⁻¹' t ∩ s

Tactic:
simp [mulIndicator_preimage, Pi.one_def, Set.preimage_const_of_notMem ht]

Premises used: Set.mulIndicator_preimage, Set.preimage_const_of_notMem, Pi.one_def
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
r : M
s : Set α
f : α → M
⊢ r ∈ range (s.mulIndicator f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s

Tactic:
simp [mulIndicator, ite_eq_iff, exists_or, eq_univ_iff_forall, and_comm, or_comm,
    @eq_comm _ r 1]

Premises used: exists_or, Set.eq_univ_iff_forall, Set.mulIndicator, and_comm, eq_comm, ite_eq_iff, or_comm
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
simp : r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)
⊢ r (s.mulIndicator f a) (s.mulIndicator g a)

Tactic:
simp only [mulIndicator]

Premises used: Set.mulIndicator
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha pos : ∀ (has : a ∈ s), r (f a) (g a)
neg : ∀ (has : ¬a ∈ s), r 1 1
⊢ r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)

Tactic:
split_ifs with has
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∈ s
⊢ r (f a) (g a)

Tactic:
ha has
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : ¬a ∈ s
⊢ r 1 1

Tactic:
h1
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∈ s
⊢ r (f a) (g a)

Tactic:
exacts [ha has, h1]
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
inst_1 : Zero M
U : Set α
s : Set M
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (U.indicator 1 ⁻¹' s)

Tactic:
indicator_const_preimage _ _ 1

Premises used: Set.Mem, Set.indicator_const_preimage, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
F' : Type u_5
E₁' : Type u_6
E₂' : Type u_7
inst : FunLike F' E₁' E₂'
inst_1 : AddGroup E₁'
inst_2 : LE E₁'
inst_3 : AddRightMono E₁'
inst_4 : AddGroup E₂'
inst_5 : LE E₂'
inst_6 : AddRightMono E₂'
inst_7 : AddMonoidHomClass F' E₁' E₂'
h : ∀ (f : F') (x : E₁'), 0 ≤ x → LE.le.{u_7} (α := E₂') (0 : E₂') ((f : (a : E₁') → E₂') x : E₂')
f : F'
a b : E₁'
hab : a ≤ b
⊢ LE.le.{u_7} (α := E₂') ((f : (a : E₁') → E₂') a : E₂') ((f : (a : E₁') → E₂') b : E₂')

Tactic:
simpa using h f (b - a) (sub_nonneg.mpr hab)

Premises used: Iff.mpr, HSub.hSub, sub_nonneg
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
f g : E₁ →ₚ[R] E₂
h : Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) f) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) g)
mk :
  ∀ (toLinearMap : E₁ →ₗ[R] E₂) (monotone' : Monotone toLinearMap.toFun)
    (h :
      Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
        ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) g)),
    { toLinearMap := toLinearMap, monotone' := monotone' : E₁ →ₚ[R] E₂ } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
g : E₁ →ₚ[R] E₂
toLinearMap : E₁ →ₗ[R] E₂
monotone' : Monotone toLinearMap.toFun
h :
  Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
    ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) g)
mk :
  ∀ (toLinearMap_1 : E₁ →ₗ[R] E₂) (monotone'_1 : Monotone toLinearMap_1.toFun)
    (h :
      Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
        ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap_1, monotone' := monotone'_1 })),
    { toLinearMap := toLinearMap, monotone' := monotone' : E₁ →ₚ[R] E₂ } =
      { toLinearMap := toLinearMap_1, monotone' := monotone'_1 }
⊢ { toLinearMap := toLinearMap, monotone' := monotone' : E₁ →ₚ[R] E₂ } = g

Tactic:
cases g
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
toLinearMap : E₁ →ₗ[R] E₂
monotone' : Monotone toLinearMap.toFun
toLinearMap_1 : E₁ →ₗ[R] E₂
monotone'_1 : Monotone toLinearMap_1.toFun
h :
  Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
    ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap_1, monotone' := monotone'_1 })
mk : toLinearMap = toLinearMap_1
⊢ { toLinearMap := toLinearMap, monotone' := monotone' : E₁ →ₚ[R] E₂ } =
    { toLinearMap := toLinearMap_1, monotone' := monotone'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
toLinearMap : E₁ →ₗ[R] E₂
monotone' : Monotone toLinearMap.toFun
toLinearMap_1 : E₁ →ₗ[R] E₂
monotone'_1 : Monotone toLinearMap_1.toFun
h :
  Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
    ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap_1, monotone' := monotone'_1 })
mk : Eq (α := (a : E₁) → E₂) (⇑toLinearMap : (a : E₁) → E₂) (⇑toLinearMap_1 : (a : E₁) → E₂)
⊢ toLinearMap = toLinearMap_1

Tactic:
apply DFunLike.coe_injective'

Premises used: DFunLike.coe_injective'
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
toLinearMap : E₁ →ₗ[R] E₂
monotone' : Monotone toLinearMap.toFun
toLinearMap_1 : E₁ →ₗ[R] E₂
monotone'_1 : Monotone toLinearMap_1.toFun
h :
  Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
    ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap_1, monotone' := monotone'_1 })
⊢ Eq (α := (a : E₁) → E₂) (⇑toLinearMap : (a : E₁) → E₂) (⇑toLinearMap_1 : (a : E₁) → E₂)

Tactic:
h
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
toLinearMap : E₁ →ₗ[R] E₂
monotone' : Monotone toLinearMap.toFun
toLinearMap_1 : E₁ →ₗ[R] E₂
monotone'_1 : Monotone toLinearMap_1.toFun
h :
  Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
    ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap_1, monotone' := monotone'_1 })
⊢ Eq (α := (a : E₁) → E₂) (⇑toLinearMap : (a : E₁) → E₂) (⇑toLinearMap_1 : (a : E₁) → E₂)

Tactic:
exact h
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
f g : E₁ →ₚ[R] E₂
h : ∀ (x : E₁), Eq.{u_3 + 1} (α := E₂) ((f : (a : E₁) → E₂) x : E₂) ((g : (a : E₁) → E₂) x : E₂)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
S : Type u_4
inst_7 : SMul S E₁
inst_8 : SMul S E₂
inst_9 : LinearMap.CompatibleSMul E₁ E₂ S R
f : E₁ →ₚ[R] E₂
c : S
x : E₁
⊢ (f : (a : E₁) → E₂) (c • x) = HSMul.hSMul (β := E₂) c ((f : (a : E₁) → E₂) x : E₂)

Tactic:
LinearMapClass.map_smul_of_tower f _ _

Premises used: LinearMapClass.map_smul_of_tower
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
f : E₁ →ₚ[R] E₂
x : E₁
hx : 0 ≤ x
⊢ LE.le.{u_3} (α := E₂) (0 : E₂) ((f : (a : E₁) → E₂) x : E₂)

Tactic:
_root_.map_nonneg f hx

Premises used: map_nonneg
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
f : E₁ →ₚ[R] E₂
⊢ Eq (α := (a : E₁) → E₂) (⇑f.toLinearMap : (a : E₁) → E₂) (⇑f : (a : E₁) → E₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
x x_1 : E₁ →ₚ[R] E₂
h : x.toLinearMap = x_1.toLinearMap
h₁ : ∀ (x_2 : E₁), Eq.{u_3 + 1} (α := E₂) ((x : (a : E₁) → E₂) x_2 : E₂) ((x_1 : (a : E₁) → E₂) x_2 : E₂)
⊢ x = x_1

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
x_1 x_2 : E₁ →ₚ[R] E₂
h : x_1.toLinearMap = x_2.toLinearMap
x : E₁
⊢ Eq.{u_3 + 1} (α := E₂) ((x_1 : (a : E₁) → E₂) x : E₂) ((x_2 : (a : E₁) → E₂) x : E₂)

Tactic:
congrm($h x)
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
f g : E₁ →ₚ[R] E₂
⊢ f.toLinearMap = g.toLinearMap ↔ f = g

Tactic:
toLinearMap_injective.eq_iff

Premises used: Function.Injective.eq_iff, PositiveLinearMap.toLinearMap_injective
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
x : E₁
⊢ ∀ ⦃b : E₁⦄,
    x ≤ b →
      LE.le.{u_3} (α := E₂)
        (AddHom.toFun (LinearMap.toAddHom.{u_1, u_1, u_2, u_3} (R := R) (S := R) (σ := RingHom.id R) 0) x)
        (AddHom.toFun (LinearMap.toAddHom.{u_1, u_1, u_2, u_3} (R := R) (S := R) (σ := RingHom.id R) 0) b)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
⊢ Eq (α := E₁ →ₗ[R] E₂) (toLinearMap 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
x : E₁
⊢ Eq.{u_3 + 1} (α := E₂) ((0 : (a : E₁) → E₂) x : E₂) (0 : E₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
inst_7 : IsOrderedAddMonoid E₂
f g : E₁ →ₚ[R] E₂
⊢ (f + g).toLinearMap = f.toLinearMap + g.toLinearMap

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
inst_7 : IsOrderedAddMonoid E₂
f g : E₁ →ₚ[R] E₂
x : E₁
⊢ (f + g : (a : E₁) → E₂) x = HAdd.hAdd (α := E₂) (β := E₂) ((f : (a : E₁) → E₂) x : E₂) ((g : (a : E₁) → E₂) x : E₂)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
inst_7 : IsOrderedAddMonoid E₂
f : E₁ →ₚ[R] E₂
x y : E₁
h : x ≤ y
⊢ (HSMul.hSMul (α := ℕ) 0 f.toLinearMap).toFun x ≤ (HSMul.hSMul (α := ℕ) 0 f.toLinearMap).toFun y

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
inst_7 : IsOrderedAddMonoid E₂
f : E₁ →ₚ[R] E₂
x y : E₁
h : x ≤ y
n : ℕ
ih : (n • f.toLinearMap).toFun x ≤ (n • f.toLinearMap).toFun y
⊢ ((n + 1) • f.toLinearMap).toFun x ≤ ((n + 1) • f.toLinearMap).toFun y

Tactic:
simpa [add_nsmul] using add_le_add ih (OrderHomClass.mono f h)

Premises used: add_le_add, OrderHomClass.mono, add_nsmul
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
inst_7 : IsOrderedAddMonoid E₂
n : ℕ
f : E₁ →ₚ[R] E₂
x y : E₁
h : x ≤ y
zero : (HSMul.hSMul (α := ℕ) 0 f.toLinearMap).toFun x ≤ (HSMul.hSMul (α := ℕ) 0 f.toLinearMap).toFun y
succ :
  ∀ (n : ℕ) (ih : (n • f.toLinearMap).toFun x ≤ (n • f.toLinearMap).toFun y),
    ((n + 1) • f.toLinearMap).toFun x ≤ ((n + 1) • f.toLinearMap).toFun y
⊢ (n • f.toLinearMap).toFun x ≤ (n • f.toLinearMap).toFun y

Tactic:
induction n with
    | zero => simp
    | succ n ih => simpa [add_nsmul] using add_le_add ih (OrderHomClass.mono f h)

Premises used: add_nsmul
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
inst_7 : IsOrderedAddMonoid E₂
f : E₁ →ₚ[R] E₂
n : ℕ
⊢ (n • f).toLinearMap = n • f.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
inst_7 : IsOrderedAddMonoid E₂
f : E₁ →ₚ[R] E₂
n : ℕ
x : E₁
⊢ (n • f : (a : E₁) → E₂) x = HSMul.hSMul (β := E₂) n ((f : (a : E₁) → E₂) x : E₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommGroup E₁
inst_2 : PartialOrder E₁
inst_3 : IsOrderedAddMonoid E₁
inst_4 : AddCommGroup E₂
inst_5 : PartialOrder E₂
inst_6 : IsOrderedAddMonoid E₂
inst_7 : Module R E₁
inst_8 : Module R E₂
f : E₁ →ₗ[R] E₂
hf : ∀ (x : E₁), 0 ≤ x → LE.le.{u_3} (α := E₂) (0 : E₂) ((f : (a : E₁) → E₂) x : E₂)
a b : E₁
hab : a ≤ b
rw : ∀ (hab : 0 ≤ b - a), 0 ≤ f.toFun b - f.toFun a
⊢ f.toFun a ≤ f.toFun b

Tactic:
rw [← sub_nonneg] at hab ⊢

Premises used: sub_nonneg
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommGroup E₁
inst_2 : PartialOrder E₁
inst_3 : IsOrderedAddMonoid E₁
inst_4 : AddCommGroup E₂
inst_5 : PartialOrder E₂
inst_6 : IsOrderedAddMonoid E₂
inst_7 : Module R E₁
inst_8 : Module R E₂
f : E₁ →ₗ[R] E₂
hf : ∀ (x : E₁), 0 ≤ x → LE.le.{u_3} (α := E₂) (0 : E₂) ((f : (a : E₁) → E₂) x : E₂)
a b : E₁
hab : 0 ≤ b - a
⊢ LE.le.{u_3} (α := E₂) (0 : E₂) ((f : (a : E₁) → E₂) (b - a) : E₂)

Tactic:
have : 0 ≤ f (b - a) := hf _ hab
-- Module: Mathlib.Algebra.Order.Module.PositiveLinearMap
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommGroup E₁
inst_2 : PartialOrder E₁
inst_3 : IsOrderedAddMonoid E₁
inst_4 : AddCommGroup E₂
inst_5 : PartialOrder E₂
inst_6 : IsOrderedAddMonoid E₂
inst_7 : Module R E₁
inst_8 : Module R E₂
f : E₁ →ₗ[R] E₂
hf : ∀ (x : E₁), 0 ≤ x → LE.le.{u_3} (α := E₂) (0 : E₂) ((f : (a : E₁) → E₂) x : E₂)
a b : E₁
hab : 0 ≤ b - a
this : LE.le.{u_3} (α := E₂) (0 : E₂) ((f : (a : E₁) → E₂) (b - a) : E₂)
⊢ 0 ≤ f.toFun b - f.toFun a

Tactic:
simpa using this
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Nontrivial R
k : R
⊢ 0 < 2 * k + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
⊢ MulLeftMono R

Tactic:
⟨fun a b c h => ?_⟩

Premises used: CovariantClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
refine : ∀ (a b c : R) (h : b ≤ c), a * b ≤ a * c
⊢ MulLeftMono R

Tactic:
refine ⟨fun a b c h => ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ c
rcases : ∀ (c : R) (h : b ≤ b + c), a * b ≤ a * (b + c)
⊢ a * b ≤ a * c

Tactic:
rcases exists_add_of_le h with ⟨c, rfl⟩

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
rw : a * b ≤ a * b + a * c
⊢ a * b ≤ a * (b + c)

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ a * b ≤ a * b + a * c

Tactic:
apply self_le_add_right

Premises used: self_le_add_right
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
⊢ MulRightMono R

Tactic:
⟨fun a b c h => ?_⟩

Premises used: CovariantClass.mk
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
refine :
  ∀ (a b c : R) (h : b ≤ c),
    LE.le (α := R) (swap (φ := fun (a a_1 : R) ↦ R) (fun (x1 x2 : R) ↦ x1 * x2) a b : R)
      (swap (φ := fun (a a_1 : R) ↦ R) (fun (x1 x2 : R) ↦ x1 * x2) a c : R)
⊢ MulRightMono R

Tactic:
refine ⟨fun a b c h => ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ c
dsimp : b * a ≤ c * a
⊢ LE.le (α := R) (swap (φ := fun (a a_1 : R) ↦ R) (fun (x1 x2 : R) ↦ x1 * x2) a b : R)
    (swap (φ := fun (a a_1 : R) ↦ R) (fun (x1 x2 : R) ↦ x1 * x2) a c : R)

Tactic:
dsimp [swap]

Premises used: Function.swap
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ c
rcases : ∀ (c : R) (h : b ≤ b + c), b * a ≤ (b + c) * a
⊢ b * a ≤ c * a

Tactic:
rcases exists_add_of_le h with ⟨c, rfl⟩

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
rw : b * a ≤ b * a + c * a
⊢ b * a ≤ (b + c) * a

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : LE R
inst_2 : CanonicallyOrderedAdd R
a b c : R
h : b ≤ b + c
⊢ b * a ≤ b * a + c * a

Tactic:
apply self_le_add_right

Premises used: self_le_add_right
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : NoZeroDivisors R
a b : R
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b

Tactic:
simp only [pos_iff_ne_zero, ne_eq, mul_eq_zero, not_or]

Premises used: mul_eq_zero, ne_eq, not_or, pos_iff_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : NoZeroDivisors R
a : R
ha : 0 < a
n : ℕ
⊢ 0 < a ^ n

Tactic:
pos_iff_ne_zero.2 <| pow_ne_zero _ ha.ne'

Premises used: Iff.mpr, pow_ne_zero, LT.lt.ne', pos_iff_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
⊢ MulPosStrictMono R

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
this : MulPosStrictMono R
inl : ∀ (hcd : 0 < d), a * 0 < b * d
inr : ∀ (hc : 0 < c), a * c < b * d
⊢ a * c < b * d

Tactic:
obtain rfl | hc := eq_zero_or_pos c

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
inl : 0 < b * d
⊢ a * 0 < b * d

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ 0 < b * d

Tactic:
mul_pos hab.pos hcd

Premises used: LT.lt.pos, mul_pos
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ 0 < b * d

Tactic:
exact mul_pos hab.pos hcd

Premises used: LT.lt.pos, mul_pos