mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
⊢ #∅ • 𝔼 i ∈ ∅, f i = ∑ i ∈ ∅, f i

pp: case inr
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
·

Goal state after:
case inl
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
⊢ #∅ • 𝔼 i ∈ ∅, f i = ∑ i ∈ ∅, f i
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
·

Goal state after:
case inr
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
this : ∀ j < k + 1, a ≤ (F.intervalGapsWithin h a b ↑j).1
hj : ¬j < k + 1
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
this : ∀ j < k + 1, a ≤ (F.intervalGapsWithin h a b ↑j).1
hj : ¬j < k + 1
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : j = 0
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = 0
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : j = 0
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = 0
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = 0
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝² : Semifield K
inst✝¹ : CharZero K
inst✝ : Fintype ι
s : Finset ι
⊢ 𝔼 i, (↑s).indicator 1 i = ↑s.dens

Tactic:
simp [expect, sum_indicator_eq_sum_inter, dens, div_eq_inv_mul, NNRat.smul_def]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).2 ≤ b
hj : ¬j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).2 ≤ b
hj : ¬j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : j = k
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = k
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : j = k
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = k
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = k
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
hj : ¬j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
hj : ¬j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: case hi
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a ∈ range k, ((p ↑a).2, (p ↑a.succ).1) ∈ F

pp: case i_inj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a₁ ∈ range k, ∀ a₂ ∈ range k, ((p ↑a₁).2, (p ↑a₁.succ).1) = ((p ↑a₂).2, (p ↑a₂.succ).1) → a₁ = a₂

pp: case i_surj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ b ∈ F, ∃ a, ∃ (_ : a ∈ range k), ((p ↑a).2, (p ↑a.succ).1) = b

pp: case h
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a ∈ range k, f (p ↑a).2 (p ↑a.succ).1 = f ((p ↑a).2, (p ↑a.succ).1).1 ((p ↑a).2, (p ↑a.succ).1).2

Tactic:
·

Goal state after:
case hi
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a ∈ range k, ((p ↑a).2, (p ↑a.succ).1) ∈ F
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: case i_inj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a₁ ∈ range k, ∀ a₂ ∈ range k, ((p ↑a₁).2, (p ↑a₁.succ).1) = ((p ↑a₂).2, (p ↑a₂.succ).1) → a₁ = a₂

pp: case i_surj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ b ∈ F, ∃ a, ∃ (_ : a ∈ range k), ((p ↑a).2, (p ↑a.succ).1) = b

pp: case h
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a ∈ range k, f (p ↑a).2 (p ↑a.succ).1 = f ((p ↑a).2, (p ↑a.succ).1).1 ((p ↑a).2, (p ↑a.succ).1).2

Tactic:
·

Goal state after:
case i_inj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a₁ ∈ range k, ∀ a₂ ∈ range k, ((p ↑a₁).2, (p ↑a₁.succ).1) = ((p ↑a₂).2, (p ↑a₂.succ).1) → a₁ = a₂
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: case i_surj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ b ∈ F, ∃ a, ∃ (_ : a ∈ range k), ((p ↑a).2, (p ↑a.succ).1) = b

pp: case h
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a ∈ range k, f (p ↑a).2 (p ↑a.succ).1 = f ((p ↑a).2, (p ↑a.succ).1).1 ((p ↑a).2, (p ↑a.succ).1).2

Tactic:
·

Goal state after:
case i_surj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ b ∈ F, ∃ a, ∃ (_ : a ∈ range k), ((p ↑a).2, (p ↑a.succ).1) = b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a ∈ range k, f (p ↑a).2 (p ↑a.succ).1 = f ((p ↑a).2, (p ↑a.succ).1).1 ((p ↑a).2, (p ↑a.succ).1).2

Tactic:
·

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a ∈ range k, f (p ↑a).2 (p ↑a.succ).1 = f ((p ↑a).2, (p ↑a.succ).1).1 ((p ↑a).2, (p ↑a.succ).1).2
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
hk : 0 = k
⊢ (F.intervalGapsWithin h a b ↑0).1 ≤ (F.intervalGapsWithin h a b ↑0).2

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
hk : ¬0 = k
⊢ (F.intervalGapsWithin h a b ↑0).1 ≤ (F.intervalGapsWithin h a b ↑0).2

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
hk : 0 = k
⊢ (F.intervalGapsWithin h a b ↑0).1 ≤ (F.intervalGapsWithin h a b ↑0).2
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
hk : ¬0 = k
⊢ (F.intervalGapsWithin h a b ↑0).1 ≤ (F.intervalGapsWithin h a b ↑0).2

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
hk : ¬0 = k
⊢ (F.intervalGapsWithin h a b ↑0).1 ≤ (F.intervalGapsWithin h a b ↑0).2
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : j = k
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : j = k
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case mp
a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, a + ↑a_1 = x) → a ≤ x ∧ x ≤ b

pp: case mpr
a b x : ℤ
⊢ a ≤ x ∧ x ≤ b → ∃ a_2 < (b + 1 - a).toNat, a + ↑a_2 = x

Tactic:
·

Goal state after:
case mp
a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, a + ↑a_1 = x) → a ≤ x ∧ x ≤ b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case mpr
a b x : ℤ
⊢ a ≤ x ∧ x ≤ b → ∃ a_2 < (b + 1 - a).toNat, a + ↑a_2 = x

Tactic:
·

Goal state after:
case mpr
a b x : ℤ
⊢ a ≤ x ∧ x ≤ b → ∃ a_2 < (b + 1 - a).toNat, a + ↑a_2 = x
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + ↑a_1 = x) → a ≤ x ∧ x < b

pp: case mpr
a b x : ℤ
⊢ a ≤ x ∧ x < b → ∃ a_2 < (b - a).toNat, a + ↑a_2 = x

Tactic:
·

Goal state after:
case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + ↑a_1 = x) → a ≤ x ∧ x < b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case mpr
a b x : ℤ
⊢ a ≤ x ∧ x < b → ∃ a_2 < (b - a).toNat, a + ↑a_2 = x

Tactic:
·

Goal state after:
case mpr
a b x : ℤ
⊢ a ≤ x ∧ x < b → ∃ a_2 < (b - a).toNat, a + ↑a_2 = x
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ lift (mk R M N) = LinearMap.id

pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ Function.Bijective ⇑LinearMap.id

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ lift (mk R M N) = LinearMap.id
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ Function.Bijective ⇑LinearMap.id

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ Function.Bijective ⇑LinearMap.id
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + 1 + ↑a_1 = x) → a < x ∧ x ≤ b

pp: case mpr
a b x : ℤ
⊢ a < x ∧ x ≤ b → ∃ a_2 < (b - a).toNat, a + 1 + ↑a_2 = x

Tactic:
·

Goal state after:
case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + 1 + ↑a_1 = x) → a < x ∧ x ≤ b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case mpr
a b x : ℤ
⊢ a < x ∧ x ≤ b → ∃ a_2 < (b - a).toNat, a + 1 + ↑a_2 = x

Tactic:
·

Goal state after:
case mpr
a b x : ℤ
⊢ a < x ∧ x ≤ b → ∃ a_2 < (b - a).toNat, a + 1 + ↑a_2 = x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ -(↑N + 1) ≠ ↑N + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + ↑a_1 = x) → a < x ∧ x < b

pp: case mpr
a b x : ℤ
⊢ a < x ∧ x < b → ∃ a_2 < (b - a - 1).toNat, a + 1 + ↑a_2 = x

Tactic:
·

Goal state after:
case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + ↑a_1 = x) → a < x ∧ x < b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case mpr
a b x : ℤ
⊢ a < x ∧ x < b → ∃ a_2 < (b - a - 1).toNat, a + 1 + ↑a_2 = x

Tactic:
·

Goal state after:
case mpr
a b x : ℤ
⊢ a < x ∧ x < b → ∃ a_2 < (b - a - 1).toNat, a + 1 + ↑a_2 = x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
⊢ ∏ m ∈ Icc (-(↑0 + 1)) (↑0 + 1), f m = f (↑0 + 1) * f (-(↑0 + 1)) * ∏ m ∈ Icc (-↑0) ↑0, f m

pp: case succ
R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
n✝ : ℕ
a✝ : ∏ m ∈ Icc (-(↑n✝ + 1)) (↑n✝ + 1), f m = f (↑n✝ + 1) * f (-(↑n✝ + 1)) * ∏ m ∈ Icc (-↑n✝) ↑n✝, f m
⊢ ∏ m ∈ Icc (-(↑(n✝ + 1) + 1)) (↑(n✝ + 1) + 1), f m =
    f (↑(n✝ + 1) + 1) * f (-(↑(n✝ + 1) + 1)) * ∏ m ∈ Icc (-↑(n✝ + 1)) ↑(n✝ + 1), f m

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
⊢ ∏ m ∈ Icc (-(↑0 + 1)) (↑0 + 1), f m = f (↑0 + 1) * f (-(↑0 + 1)) * ∏ m ∈ Icc (-↑0) ↑0, f m
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
n✝ : ℕ
a✝ : ∏ m ∈ Icc (-(↑n✝ + 1)) (↑n✝ + 1), f m = f (↑n✝ + 1) * f (-(↑n✝ + 1)) * ∏ m ∈ Icc (-↑n✝) ↑n✝, f m
⊢ ∏ m ∈ Icc (-(↑(n✝ + 1) + 1)) (↑(n✝ + 1) + 1), f m =
    f (↑(n✝ + 1) + 1) * f (-(↑(n✝ + 1) + 1)) * ∏ m ∈ Icc (-↑(n✝ + 1)) ↑(n✝ + 1), f m

Tactic:
·

Goal state after:
case succ
R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
n✝ : ℕ
a✝ : ∏ m ∈ Icc (-(↑n✝ + 1)) (↑n✝ + 1), f m = f (↑n✝ + 1) * f (-(↑n✝ + 1)) * ∏ m ∈ Icc (-↑n✝) ↑n✝, f m
⊢ ∏ m ∈ Icc (-(↑(n✝ + 1) + 1)) (↑(n✝ + 1) + 1), f m =
    f (↑(n✝ + 1) + 1) * f (-(↑(n✝ + 1) + 1)) * ∏ m ∈ Icc (-↑(n✝ + 1)) ↑(n✝ + 1), f m
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inl
n : ℤ
h : 0 ≤ 0
⊢ image (fun x ↦ x % 0) (Ico n (n + 0)) = Ico 0 0

pp: case inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = Ico 0 a

Tactic:
·

Goal state after:
case inl
n : ℤ
h : 0 ≤ 0
⊢ image (fun x ↦ x % 0) (Ico n (n + 0)) = Ico 0 0
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mp
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → 0 ≤ i ∧ i < a

pp: case inr.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ 0 ≤ i ∧ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i

Tactic:
·

Goal state after:
case inr.mp
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → 0 ≤ i ∧ i < a
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inl
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

pp: case inr.mpr.inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
·

Goal state after:
case inr.mpr.inl
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inl.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)

pp: case inr.mpr.inl.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

pp: case inr.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
·

Goal state after:
case inr.mpr.inl.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inl.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

pp: case inr.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
·

Goal state after:
case inr.mpr.inl.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
·

Goal state after:
case inr.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
i : M₁ →ₗ[R] M₁
j : M₂ →ₗ[R] M₂
n : ℕ
⊢ hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp only [pow_succ, ih, hf.map_mul]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
·

Goal state after:
case inr.mpr.inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i