mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharZero R
⊢ CharZero R

pp: case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ CharZero R

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharZero R
⊢ CharZero R
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ CharZero R

Tactic:
·

Goal state after:
case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ CharZero R
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ q = 1 → p = 0

pp: case mpr
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ p = 0 → q = 1

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ q = 1 → p = 0
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ p = 0 → q = 1

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p q : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R q
⊢ p = 0 → q = 1
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ f ≤ g

Tactic:
by
  constructor
  · intro x hx
    rw [mem_domain_iff] at hx ⊢
    obtain ⟨y, hx⟩ := hx
    use y
    exact h hx
  rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
  rw [image_iff]
  refine h ?_
  simp only at hxy
  rw [hxy] at hx
  rw [← image_iff hx]
  simp [hxy]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f ≤ g
⊢ f.graph ≤ g.graph

Tactic:
intro x hx
  rw [mem_graph_iff] at hx ⊢
  obtain ⟨y, hx⟩ := hx
  use ⟨y, h.1 y.2⟩
  simp only [hx, true_and]
  convert! hx.2 using 1
  refine (h.2 ?_).symm
  simp only [hx.1]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ f.domain = g.domain

pp: case h'
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y

Tactic:
·

Goal state after:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ f.domain = g.domain
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h'
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y

Tactic:
·

Goal state after:
case h'
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∃ x, (a, x) ∈ g

pp: case refine_2
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∀ (y₁ y₂ : F), (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∃ x, (a, x) ∈ g
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (g.toLinearPMapAux ?hc) x = valFromGraph hg ⋯

pp: case hc
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ∀ x ∈ g, x.1 = 0 → x.2 = 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (g.toLinearPMapAux ?hc) x = valFromGraph hg ⋯
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case hc
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ∀ x ∈ g, x.1 = 0 → x.2 = 0

Tactic:
·

Goal state after:
case hc
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ∀ x ∈ g, x.1 = 0 → x.2 = 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g.toLinearPMap.graph
⊢ (x_fst, x_snd) ∈ g

pp: case mpr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g.toLinearPMap.graph
⊢ (x_fst, x_snd) ∈ g
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ioo a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Ioc a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Icc a c
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Icc a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Icc a c
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Icc a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Icc a c
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
⊢ (r • p).support ⊆ p.support

Tactic:
intro i hi
  rw [mem_support_iff] at hi ⊢
  contrapose hi
  simp [hi]

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ici a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ici a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ici a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ici a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ici a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ f (0 • v) = (RingHom.id R[M]) 0 • f v

pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ ∀ (m : M) (r : R) (x : R[M]),
    m ∉ x.coeff.support →
      r ≠ 0 →
        f (x • v) = (RingHom.id R[M]) x • f v → f ((single m r + x) • v) = (RingHom.id R[M]) (single m r + x) • f v

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ f (0 • v) = (RingHom.id R[M]) 0 • f v
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ ∀ (m : M) (r : R) (x : R[M]),
    m ∉ x.coeff.support →
      r ≠ 0 →
        f (x • v) = (RingHom.id R[M]) x • f v → f ((single m r + x) • v) = (RingHom.id R[M]) (single m r + x) • f v

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ ∀ (m : M) (r : R) (x : R[M]),
    m ∉ x.coeff.support →
      r ≠ 0 →
        f (x • v) = (RingHom.id R[M]) x • f v → f ((single m r + x) • v) = (RingHom.id R[M]) (single m r + x) • f v
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → p.coeff b.1 * (X ^ n).coeff b.2 = 0

pp: case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = 0

Tactic:
·

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → p.coeff b.1 * (X ^ n).coeff b.2 = 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = 0

Tactic:
·

Goal state after:
case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
⊢ (p * X ^ n).coeff d = p.coeff (d - n)

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ (p * X ^ n).coeff d = 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
⊢ (p * X ^ n).coeff d = p.coeff (d - n)
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ (p * X ^ n).coeff d = 0

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ (p * X ^ n).coeff d = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ degt 0 ≤ 0

pp: case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ ∀ (a b : A), degt (a + b) ≤ degt a + degt b

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ degt 0 ≤ 0