mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
⊢ (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)

Tactic:
refine Finset.induction_on s
      (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h), fun _ ↦ rfl⟩) ?_
    intro a s ha ih H
    have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
    rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
      forall_mem_insert, ih this]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

Tactic:
rw [Subsingleton.elim D]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ DecidablePred p
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
G : Type u_9
inst✝² : AddCommGroup G
inst✝¹ : LinearOrder G
inst✝ : AddLeftMono G
f : ι → G
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
⊢ |∑ i ∈ s, f i| = ∑ i ∈ s, f i

Tactic:
by
  rw [abs_of_nonneg (Finset.sum_nonneg' hf)]

Goal state after:
Module: Mathlib.Data.Finsupp.SMulWithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
a : R
a✝ : α
⊢ (a • 0) a✝ = 0 a✝

Tactic:
apply smul_zero

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case pos
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
hx : ∃ x ∈ s, f x ≠ 0
⊢ ∑ x ∈ s, f x ≤ 1

Tactic:
obtain ⟨x, hsx, hfx⟩ := hx
      have hs : ∀ y ∈ s \ {x}, f y = 0 := by grind
      simp [← sum_sdiff (singleton_subset_iff.2 hsx), sum_congr rfl hs, (h x x hsx hsx hfx hfx).2]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case neg
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
hx : ∀ x ∈ s, f x = 0
⊢ ∑ x ∈ s, f x ≤ 1

Tactic:
simp [sum_congr rfl hx]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
l : α →₀ M
h : l ∈ supported M R ∅
⊢ l = 0

Tactic:
by ext; simp_all [mem_supported']

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
⊢ (↑↑(ringHomEndFinsupp ι)).toFun ((fun f ↦ { toFun := fun m ↦ (f (single i m)) i, map_add' := ⋯, map_smul' := ⋯ }) f) =
    f

Tactic:
ext x j

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
x : ι →₀ M
j : ι
⊢ (((↑↑(ringHomEndFinsupp ι)).toFun
          ((fun f ↦ { toFun := fun m ↦ (f (single i m)) i, map_add' := ⋯, map_smul' := ⋯ }) f))
        x)
      j =
    (f x) j
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ (v.sum fun i c_1 ↦ (h i) (c • c_1)) = σ c • v.sum fun a ↦ ⇑(h a)

pp: α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ∀ (i : α), (h i) 0 = 0

Tactic:
Finsupp.smul_sum

Goal state after:
α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ (v.sum fun i c_1 ↦ (h i) (c • c_1)) = v.sum fun a b ↦ σ c • (h a) b

α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ∀ (i : α), (h i) 0 = 0
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case inr.refine_2
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
⊢ (lmapDomain M R f) ((lmapDomain M R (Function.invFunOn f s)) l) = l

Tactic:
rw [← LinearMap.comp_apply, ← lmapDomain_comp]

Goal state after:
case inr.refine_2
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
⊢ (lmapDomain M R (f ∘ Function.invFunOn f s)) l = l
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
h : mulSupport f ⊆ s
hs : s.Finite
⊢ mulSupport f ⊆ ↑hs.toFinset

Tactic:
by rwa [Set.Finite.coe_toFinset]

Goal state after:
Module: Mathlib.Data.Finset.Fin

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ ↑s ⊆ Set.range Fin.val

Tactic:
exact fun m hm ↦ ⟨⟨m, h m hm⟩, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ span R (v '' s) = map (linearCombination R v) (supported R R s)

Tactic:
by
  apply span_eq_of_le
  · intro x hx
    rw [Set.mem_image] at hx
    apply Exists.elim hx
    intro i hi
    exact ⟨_, Finsupp.single_mem_supported R 1 hi.1, by simp [hi.2]⟩
  · refine map_le_iff_le_comap.2 fun z hz => ?_
    have : ∀ i, z i • v i ∈ span R (v '' s) := by
      intro c
      have := Classical.decPred fun x => x ∈ s
      by_cases h : c ∈ s
      · exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))
      · simp [(Finsupp.mem_supported' R _).1 hz _ h]
    rw [mem_comap, linearCombination_apply]
    refine sum_mem ?_
    simp [this]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' Ico i j = Ico (i.addNat m) (j.addNat m)

Tactic:
← preimage_addNat_Ico_addNat,

Goal state after:
n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Ico (i.addNat ?m) (j.addNat ?m) = Ico (i.addNat m) (j.addNat m)

case m
n m : ℕ
i j : Fin n
⊢ ℕ
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ image val (Ici a) = Ico (↑a) n

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ image val (Ioi a) = Ioo (↑a) n

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ image val (Iic a) = Iic ↑a

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
b : Fin n
⊢ image val (Iio b) = Iio ↑b

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Icc a b) = Icc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ico a b) = Ico (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ioc a b) = Ioc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ioo a b) = Ioo (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (uIcc a b) = uIcc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ image (castLE h) (Iic a) = Iic (castLE h a)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ image (castLE h) (Iio a) = Iio (castLE h a)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Icc a b) = Icc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ico a b) = Ico (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ioc a b) = Ioc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ioo a b) = Ioo (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (uIcc a b) = uIcc (castLE h a) (castLE h b)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Iic a) = Iic (castLE h a)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Iio a) = Iio (castLE h a)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ image (castAdd m) (Ici i) = Ico (castAdd m i) (natAdd n 0)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ image (castAdd m) (Ioi i) = Ioo (castAdd m i) (natAdd n 0)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ map (castAddEmb m) (Ioi i) = Ioo (castAdd m i) (natAdd n 0)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Icc i j) = Icc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Ico i j) = Ico (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Ioc i j) = Ioc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Ioo i j) = Ioo (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (uIcc i j) = uIcc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Ici i) = Ici (Fin.cast h i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Ioi i) = Ioi (Fin.cast h i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Iic i) = Iic (Fin.cast h i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Iio i) = Iio (Fin.cast h i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Icc i j) = Icc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Ico i j) = Ico (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Ioc i j) = Ioc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (Ioo i j) = Ioo (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ map (finCongr h).toEmbedding (uIcc i j) = uIcc (Fin.cast h i) (Fin.cast h j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Ici i) = Ici (Fin.cast h i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Ioi i) = Ioi (Fin.cast h i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Iic i) = Iic (Fin.cast h i)

Tactic:
simp [← coe_inj]

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
m : ℕ
x : α
u : Fin m → α
i : Fin m
⊢ vecCons x u i.succ = u i

Tactic:
simp [vecCons]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Iio i) = Iio (Fin.cast h i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Icc i j) = Icc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Ico i j) = Ico (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Ioc i j) = Ioc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Ioo i j) = Ioo (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (natAdd m) (uIcc i j) = uIcc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (natAdd m) (Ici i) = Ici (natAdd m i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (natAdd m) (Ioi i) = Ioi (natAdd m i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Icc i j) = Icc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Ico i j) = Ico (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Ioc i j) = Ioc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Ioo i j) = Ioo (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hi : i ≠ Fin.last n
hj : j ≠ i
⊢ (finSuccEquiv' i) j = some ((i.castLT ⋯).predAbove j)

Tactic:
rcases Fin.exists_succAbove_eq hj with ⟨j, rfl⟩
  rcases Fin.exists_castSucc_eq.2 hi with ⟨i, rfl⟩
  simp

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (uIcc i j) = uIcc (natAdd m i) (natAdd m j)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (natAddEmb m) (Ici i) = Ici (natAdd m i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (natAddEmb m) (Ioi i) = Ioi (natAdd m i)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Icc i j) = Icc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Ico i j) = Ico (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Ioc i j) = Ioc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Ioo i j) = Ioo (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (uIcc i j) = uIcc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (fun x ↦ x.addNat m) (Ici i) = Ici (i.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (fun x ↦ x.addNat m) (Ioi i) = Ioi (i.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Icc i j) = Icc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ico i j) = Ico (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ioc i j) = Ioc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ioo i j) = Ioo (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (uIcc i j) = uIcc (i.addNat m) (j.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (addNatEmb m) (Ici i) = Ici (i.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (addNatEmb m) (Ioi i) = Ioi (i.addNat m)

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image succ (Iic i) = Ioc 0 i.succ

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image succ (Iio i) = Ioo 0 i.succ

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (succEmb n) (Iic i) = Ioc 0 i.succ

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (succEmb n) (Iio i) = Ioo 0 i.succ

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Icc i j) = Icc j.rev i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Ico i j) = Ioc j.rev i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Ioc i j) = Ico j.rev i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Ioo i j) = Ioo j.rev i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (uIcc i j) = uIcc i.rev j.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Ici i) = Iic i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Ioi i) = Iio i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Iic i) = Ici i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Iio i) = Ioi i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Icc i j) = Icc j.rev i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ico i j) = Ioc j.rev i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioc i j) = Ico j.rev i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioo i j) = Ioo j.rev i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (uIcc i j) = uIcc i.rev j.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ici i) = Iic i.rev

Tactic:
simp [← coe_inj]

Goal state after: