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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
s✝ : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
⊢ (g a).prod h * (∑ i ∈ s, g i).prod h = (∑ i ∈ cons a s has, g i).prod h

Tactic:
sum_cons,

Goal state after:
α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
s✝ : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
⊢ (g a).prod h * (∑ i ∈ s, g i).prod h = (g a + ∑ x ∈ s, g x).prod h
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
inst✝² : Semiring R
S : Type u_6
inst✝¹ : Semiring S
inst✝ : PartialOrder S
v : AbsoluteValue R S
⊢ ¬v.IsNontrivial ↔ ∀ (x : R), x ≠ 0 → v x = 1

Tactic:
by
  simp only [IsNontrivial]
  push Not
  rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst f.graph = f.support

Tactic:
simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
⊢ mapDomain id x = x

Tactic:
mapDomain_id

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
⊢ x = x
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
⊢ ∏ u ∈ image g s, f u ≤ ∏ u ∈ s, f (g u)

Tactic:
by
  rw [prod_comp f g]
  refine prod_le_prod' fun a hag ↦ ?_
  obtain ⟨i, hi, hig⟩ := Finset.mem_image.mp hag
  apply le_self_pow (hf a hag)
  rw [← Nat.pos_iff_ne_zero, card_pos]
  exact ⟨i, mem_filter.mpr ⟨hi, hig⟩⟩

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
by
  rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _]
  simp

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n
⊢ ∑ t ∈ B, #(s ∩ t) ≤ #s * n

Tactic:
by
  refine le_trans ?_ (s.sum_le_card_nsmul _ _ h)
  simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
  exact sum_comm.le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ mapDomain id f = f

Tactic:
mapDomain_id

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ f = f
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
c : R
⊢ b.repr.symm (c • single i 1) = c • b i

Tactic:
rw [map_smul, repr_symm_single_one]

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

Goal state before:
pp: case h₁
α : 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 α
⊢ v '' s ⊆ ↑(map (linearCombination R v) (supported R R s))

Tactic:
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]⟩

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s

Tactic:
· refine ((mem_inter_iff x s (mulSupport f)).mp ?_).1
      rw [Set.ext_iff.mp h x, mem_inter_iff]
      exact ⟨hx, hxf⟩

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (mapDomain (⇑((Equiv.refl M).subtypeEquiv ⋯)) (b.reindexRange.repr (b i))) ⟨bi, hbi⟩ = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩

Tactic:
Finsupp.mapDomain_equiv_apply,

Goal state after:
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ (b.reindexRange.repr (b i)) (((Equiv.refl M).subtypeEquiv ⋯).symm ⟨bi, hbi⟩) = (single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j

Tactic:
← finprod_mem_univ f,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ univ), f i = ∏ᶠ (j : β), g j
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k.castSucc] i
⊢ ↑((finCycle k.succ) i) = ↑((⇑(finRotate (n + 1)))^[↑k.succ] i)

Tactic:
Fin.val_castSucc

Goal state after:
case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k] i
⊢ ↑((finCycle k.succ) i) = ↑((⇑(finRotate (n + 1)))^[↑k.succ] i)
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inl
y z : ℕ∞
⊢ (1 * y) ^ ⊤ = 1 ^ ⊤ * y ^ ⊤

Tactic:
simp only [one_mul, one_epow]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr
a b c : ℕ
ha0 : a > 0
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rcases Nat.eq_or_lt_of_le ha0 with rfl | ha1

Goal state after:
case inr.inl
b c : ℕ
ha0 : succ 0 > 0
⊢ (succ 0 ^ c - 1) % (succ 0 ^ b - 1) = succ 0 ^ (c % b) - 1

case inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
⊢ ∀ (c : ι →₀ R), (Finsupp.linearCombination R v) c ∈ (Finsupp.linearCombination R v).range

Tactic:
exact fun c ↦ ⟨c, rfl⟩

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

Goal state before:
pp: case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : g i ≤ f i
⊢ f i = g i

pp: case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : ¬g i ≤ f i
⊢ f i = g i

Tactic:
· apply hi'.antisymm'
      simpa [hi', tsub_eq_zero_iff_le] using h.1 i ⟨hi, hi'⟩

Goal state after:
case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : ¬g i ≤ f i
⊢ f i = g i
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
⊢ card α ≠ 0 ↔ Nonempty α

Tactic:
card_ne_zero_iff_nonempty

Goal state after:
α : Type u_3
⊢ Nonempty α ↔ Nonempty α
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inl.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Infinite β
⊢ card α ≠ 0

Tactic:
card_ne_zero_iff_nonempty

Goal state after:
case inr.inl.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Infinite β
⊢ Nonempty α
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ (∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ xᶜ, x_1 i • v i), ∃ x, ¬x_1 x = 0) ↔
    ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
refine ⟨fun ⟨t, f, heq, i, hfi⟩ => ?_, fun ⟨t, f, heq, i, hi, hfi⟩ =>
    ⟨t, f, heq, i, hfi⟩⟩

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ xᶜ, x_1 i • v i), ∃ x, ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hfi : ¬f i = 0
⊢ ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, f i ≠ 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ s.Finite

Tactic:
← encard_lt_top_iff

Goal state after:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ s.encard < ⊤
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
⊢ (LinearIndependent K fun (x : ↑s) ↦ v ↑x) ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))

Tactic:
linearIndependent_iff_notMem_span,

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
⊢ (∀ (i : ↑s), v ↑i ∉ span K ((fun x ↦ v ↑x) '' (univ \ {i}))) ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ 0 < Nat.card α ↔ Nonempty α

Tactic:
by
  have := Fintype.ofFinite α
  rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this : IsEmpty β
⊢ Nat.card α = 0

Tactic:
have := Function.isEmpty f

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this✝ : IsEmpty β
this : IsEmpty α
⊢ Nat.card α = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝ : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ t = f '' s

Tactic:
rw [(hs.image f).eq_of_subset_of_encard_le (image_subset_iff.mpr hf)
    (h.symm.trans hinj.encard_image.symm).le]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Infinite
⊢ (t \ s).ncard = 0 - s.ncard

Tactic:
Nat.zero_sub,

Goal state after:
case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Infinite
⊢ (t \ s).ncard = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : s.Nontrivial ∧ s.Finite
hs_nontrivial : s.Nontrivial
hs_finite : Finite ↑s
⊢ 1 < s.ncard

Tactic:
one_lt_ncard_iff_nontrivial

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : s.Nontrivial ∧ s.Finite
hs_nontrivial : s.Nontrivial
hs_finite : Finite ↑s
⊢ s.Nontrivial
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
by
  by_cases hb : IsMin b
  · rw [Icc_eq_empty, Ioo_eq_empty hb.not_lt]
    exact fun h ↦ not_isMin_succ _ <| hb.mono <| h.trans <| pred_le _
  · rw [Icc_pred_right_eq_Ico_of_not_isMin hb, Ico_succ_left_eq_Ioo]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ici a ∩ Iio b) (Ico (a + d) (b + d))

Tactic:
← Ici_inter_Iio

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ici a ∩ Iio b) (Ici (a + d) ∩ Iio (b + d))
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
← map_add_right_Ico,

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ico a b) = map (addRightEmbedding c) (Ico a b)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case succ
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
hn : succ^[n] i < j
⊢ (succ ∘ succ^[n]) i ≤ j

Tactic:
Function.comp_apply

Goal state after:
case succ
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
hn : succ^[n] i < j
⊢ succ (succ^[n] i) ≤ j
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico (a + c) (b + c), f x

Tactic:
← map_add_right_Ico,

Goal state after:
α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ map (addRightEmbedding c) (Ico a b), f x
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : ¬IsMax m
⊢ (insert (succ m) (Ioc n m)).sup (disjointed f) = f (succ m) \ f n

Tactic:
simp only [sup_insert, hf.disjointed_succ h'm, ih]

Goal state after:
case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : ¬IsMax m
⊢ f (succ m) \ f m ⊔ f m \ f n = f (succ m) \ f n
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n

Tactic:
by_cases h'm : IsMax m
    · simpa [Order.succ_eq_iff_isMax.mpr h'm] using ih
    · rw [← Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax hm h'm]
      simp only [sup_insert, hf.disjointed_succ h'm, ih]
      exact sdiff_sup_sdiff_cancel (hf (Order.le_succ m)) (hf hm)

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ {a ∈ antidiagonal n | k ≤ a.1} =
    map ({ toFun := fun x ↦ x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal (n - k))

Tactic:
by
  ext ⟨i, j⟩
  suffices i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i by simpa
  refine ⟨fun hi ↦ ⟨i - k, ?_, tsub_add_cancel_of_le hi.2⟩, ?_⟩
  · rw [← Nat.sub_add_comm hi.2, hi.1]
  · rintro ⟨l, hl, rfl⟩
    refine ⟨?_, Nat.le_add_left k l⟩
    rw [add_right_comm, hl]
    exact tsub_add_cancel_of_le h

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
x y : α
⊢ span {x, y} = span {y, x}

Tactic:
simp only [span_insert, sup_comm]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 * ∑ i ∈ range (m + 1), (2 * m + 1).choose i =
    ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)

Tactic:
two_mul,

Goal state after:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose i =
    ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
⊢ ↑(k.choose c) * (a ^ c * b ^ (k - c)) ∈ I

Tactic:
apply mul_mem_left

Goal state after:
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
⊢ a ^ c * b ^ (k - c) ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ 2 * ∑ i ∈ range (n + 1), i * n.choose i =
    ∑ i ∈ range (n + 1), (n - i) * n.choose (n - i) + ∑ i ∈ range (n + 1), i * n.choose i

Tactic:
two_mul,

Goal state after:
n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), i * n.choose i + ∑ i ∈ range (n + 1), i * n.choose i =
    ∑ i ∈ range (n + 1), (n - i) * n.choose (n - i) + ∑ i ∈ range (n + 1), i * n.choose i
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝ : Ring R
I J : Ideal R
a b x y : R
⊢ ∀ (a : R ⧸ ⊤), a = default

Tactic:
by rintro ⟨x⟩; exact Quotient.eq_zero_iff_mem.mpr Submodule.mem_top

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
z : Finset β
hz : z ∈ powersetCard y x
⊢ f #z = f y

Tactic:
(mem_powersetCard.1 hz).2

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
z : Finset β
hz : z ∈ powersetCard y x
⊢ f y = f y
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map f (((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[n]) K) ≤
    map i (((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[n]) K)

Tactic:
Function.comp_apply

Goal state after:
case succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map f (comap f (map i ((fun K ↦ comap f (map i K))^[n] K))) ≤
    map i (comap f (map i ((fun K ↦ comap f (map i K))^[n] K)))
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk.mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝ b✝¹ : R
inst✝ : I.IsTwoSided
x✝ : R ⧸ I
a : R
y✝ : R ⧸ I
b : R
b✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ (Quot.mk (⇑(Submodule.quotientRel I)) a * Quot.mk (⇑(Submodule.quotientRel I)) b) •
      Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c =
    Quot.mk (⇑(Submodule.quotientRel I)) a •
      Quot.mk (⇑(Submodule.quotientRel I)) b • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c

Tactic:
exact congr_arg _ (mul_smul _ _ _)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ ∏ i ∈ s, f i ∈ I

Tactic:
rw [Finset.prod_eq_prod_sdiff_singleton_mul hi]

Goal state after:
α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ (∏ x ∈ s \ {i}, f x) * f i ∈ I
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ (Finsupp.single x 1) y = Pi.single x 1 y

pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 • ⋯.choose = 0

Tactic:
Finsupp.single_eq_pi_single

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ Pi.single x 1 y = Pi.single x 1 y

R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 • ⋯.choose = 0
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
U : Set α
⊢ U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U

Tactic:
simp only [IsBasis.filter, FilterBasis.mem_filter_iff, mem_filterBasis_iff,
    exists_exists_and_eq_and]

Goal state after: