mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #{i | xs.get i = a} = List.count a xs.toList
⊢ (if x = a then 1 else 0) + List.count a xs.toList = List.count a xs.toList + if (x == a) = true then 1 else 0

Tactic:
add_comm (ite (x = a) 1 0),

Goal state after:
case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #{i | xs.get i = a} = List.count a xs.toList
⊢ (List.count a xs.toList + if x = a then 1 else 0) = List.count a xs.toList + if (x == a) = true then 1 else 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ f a ∣ finprod f

Tactic:
· rw [notMem_mulSupport.mp ha]
    exact one_dvd (finprod f)

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬(s ∩ mulSupport (f ∘ g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)

Tactic:
unfold Function.comp at hs

Goal state after:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬(s ∩ mulSupport fun x ↦ f (g x)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨i + 1, hi⟩

Tactic:
simp only [← Nat.add_assoc, Nat.add_right_comm, cons_val_succ',
      vecAlt0]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a

Tactic:
rw [Set.sUnion_eq_biUnion]
  exact finprod_mem_biUnion h ht₀ ht₁

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
⊢ ∏ᶠ (x : α), f x = 0

Tactic:
by
  nontriviality
  rw [finprod_eq_prod f hf]
  refine Finset.prod_eq_zero (hf.mem_toFinset.2 ?_) hx
  simp [hx]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
hi : i ≠ 0
⊢ ↑((Equiv.symm (finRotate n)) i) = ↑i - 1

Tactic:
finRotate_symm_apply,

Goal state after:
n : ℕ
inst✝ : NeZero n
i : Fin n
hi : i ≠ 0
⊢ ↑(i - 1) = ↑i - 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x ↦ x ∈ range f
g : α → M
a : α
⊢ (if h' : f a ∈ range f then g (Classical.choose h') else 1) = g a

Tactic:
dif_pos (Set.mem_range_self a),

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x ↦ x ∈ range f
g : α → M
a : α
⊢ g (Classical.choose ⋯) = g a
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
refine ⟨fun h ↦ ⟨?_, fun y_0 ↦ ?_⟩, fun h ↦ h.1.symm ▸ zero_epow h.2⟩
  · contrapose! h
    exact (epow_pos h).ne'
  · rw [y_0, epow_zero] at h; contradiction

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

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun x1 x2 ↦ x1 * x2) g k

Tactic:
by
  rcases lt_trichotomy (k : ℕ) j with (h | h | h)
  · rwa [succAbove_of_castSucc_lt, succAbove_of_castSucc_lt, partialProd_right_inv,
    contractNth_apply_of_lt]
    · assumption
    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
      exact le_of_lt h
  · rwa [succAbove_of_castSucc_lt, succAbove_of_le_castSucc, partialProd_succ,
    castSucc_succ, ← mul_assoc,
      partialProd_right_inv, contractNth_apply_of_eq]
    · simp [le_iff_val_le_val, ← h]
    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
      exact le_of_eq h
  · rwa [succAbove_of_le_castSucc, succAbove_of_le_castSucc, partialProd_succ, partialProd_succ,
      castSucc_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
    · exact le_iff_val_le_val.2 (le_of_lt h)
    · rw [le_iff_val_le_val, val_succ]
      exact Nat.succ_le_of_lt h

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case refine_2
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ (↑m / ↑d).gcd (↑c / ↑d) = 1

Tactic:
show Int.gcd (m / d) (c / d) = 1
    simp only [d, ← Int.natCast_div, Int.gcd_natCast_natCast (m / d) (c / d),
      gcd_div hmd hcd, Nat.div_self (gcd_pos_of_pos_left c hm)]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
⊢ (take i (ofFn f)).prod = ∏ j with ↑j < i, f j

Tactic:
induction i with
  | zero =>
    simp
  | succ i IH =>
    by_cases h : i < n
    · have : i < length (ofFn f) := by rwa [length_ofFn]
      rw [prod_take_succ _ _ this]
      have A : ({j | j.val < i + 1} : Finset (Fin n)) =
          insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) := by grind
      grind
    · have A : (ofFn f).take i = (ofFn f).take i.succ := by
        rw [← length_ofFn (f := f)] at h
        have : length (ofFn f) ≤ i := not_lt.mp h
        rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
      have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) := by
        intro j
        have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
        simp [this, lt_trans this (Nat.lt_succ_self _)]
      simp [← A, B, IH]

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

Goal state before:
pp: case inl
ι : 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
x✝ : ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ((∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0)
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ s
hfi : f i ≠ 0
⊢ ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ∃ i ∈ s, f i ≠ 0

pp: case inr
ι : 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
x✝ : ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ((∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0)
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
hgi : f i ≠ 0
⊢ ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ∃ i ∈ s, f i ≠ 0

Tactic:
· exact ⟨s, t, f, hst, heq, i, hi, hfi⟩

Goal state after:
case inr
ι : 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
x✝ : ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ((∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0)
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
hgi : f i ≠ 0
⊢ ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ∃ i ∈ s, f i ≠ 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: k : ℕ
⊢ {i | i < k}.encard = ↑k

Tactic:
by
  convert! encard_coe_eq_coe_finsetCard (Finset.range k) using 1
  · rw [Finset.coe_range, Iio_def]
  rw [Finset.card_range]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥⊥ = 1

Tactic:
exact card_bot

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

Goal state before:
pp: case inr
α : Type u_1
l : List α
h : l.Nodup
h✝ : Infinite α
⊢ ↑l.length ≤ ENat.card α

Tactic:
· grw [ENat.card_eq_top_of_infinite]
    exact le_top

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Finite

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ Finite ((G ⧸ H) × ↥H) ↔ Finite ↥H ∧ Finite (G ⧸ H)

Tactic:
Prod.finite_iff,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ Finite (G ⧸ H) ∧ Finite ↥H ↔ Finite ↥H ∧ Finite (G ⧸ H)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ x✝ ∈ ⇑f ⁻¹' {f a} ↔ x✝ ∈ a • ↑f.ker

Tactic:
mem_preimage,

Goal state after:
α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ f x✝ ∈ {f a} ↔ x✝ ∈ a • ↑f.ker
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x y : M
⊢ p.quotientRel x y ↔ -(x - y) ∈ p

Tactic:
rw [quotientRel, leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x y : M
⊢ -x + y ∈ p.toAddSubgroup ↔ -x + y ∈ p
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
⊢ b i = 0 i

Tactic:
by_cases hiI : i ∈ I
    · by_cases hiJ : i ∈ J
      · exact (h.le_bot ⟨hiI, hiJ⟩).elim
      · exact hJ i hiJ
    · exact hI i hiI

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
h : a ≤ b
⊢ ↑(insert a (Ioc a b)) = ↑(Ioc (pred a) b)

Tactic:
by simpa using Set.insert_Ioc_left_eq_Ioc_pred h

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
by
  simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc a b

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : One α
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : Add α
inst✝³ : Sub α
inst✝² : SuccAddOrder α
inst✝¹ : PredSubOrder α
inst✝ : Nontrivial α
a b : α
⊢ Icc (a + 1) (b - 1) = Ioo a b

Tactic:
by
  simpa [succ_eq_add_one, pred_eq_sub_one] using Icc_succ_pred_eq_Ioo a b

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
⊢ ∃ z, ∀ i ∈ s, r (f i) (f z)

Tactic:
convert! D.finset_le hs.toFinset using 3

Goal state after:
α : Type u_2
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
x✝ a✝ : γ
⊢ a✝ ∈ s → r (f a✝) (f x✝) ↔ a✝ ∈ hs.toFinset → r (f a✝) (f x✝)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (↑(Finset.Ioc i j)) i

Tactic:
rw [Finset.coe_Ioc]

Goal state after:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (Set.Ioc i j) i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
⊢ ∀ {a b : ι}, a ≤ b → ∃ n, succ^[n] a = b

Tactic:
intro i j hij
    rw [le_iff_lt_or_eq] at hij
    rcases hij with hij | hij
    swap
    · refine ⟨0, ?_⟩
      simpa only [Function.iterate_zero, id] using hij
    by_contra! h
    have h_lt : ∀ n, succ^[n] i < j := fun n ↦ by
      induction n with
      | zero => simpa only [Function.iterate_zero, id] using hij
      | succ n hn =>
        refine lt_of_le_of_ne ?_ (h _)
        rw [Function.iterate_succ', Function.comp_apply]
        exact succ_le_of_lt hn
    have h_mem : ∀ n, succ^[n] i ∈ Finset.Icc i j :=
      fun n ↦ Finset.mem_Icc.mpr ⟨le_succ_iterate n i, (h_lt n).le⟩
    obtain ⟨n, m, hnm, h_eq⟩ : ∃ n m, n < m ∧ succ^[n] i = succ^[m] i := by
      let f : ℕ → Finset.Icc i j := fun n ↦ ⟨succ^[n] i, h_mem n⟩
      obtain ⟨n, m, hnm_ne, hfnm⟩ : ∃ n m, n ≠ m ∧ f n = f m :=
        Finite.exists_ne_map_eq_of_infinite f
      have hnm_eq : succ^[n] i = succ^[m] i := by simpa only [f, Subtype.mk_eq_mk] using hfnm
      rcases le_total n m with h_le | h_le
      · exact ⟨n, m, lt_of_le_of_ne h_le hnm_ne, hnm_eq⟩
      · exact ⟨m, n, lt_of_le_of_ne h_le hnm_ne.symm, hnm_eq.symm⟩
    have h_max : IsMax (succ^[n] i) := isMax_iterate_succ_of_eq_of_ne h_eq hnm.ne
    exact not_le.mpr (h_lt n) (h_max (h_lt n).le)

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ ∃ c, n = kl.1 * c

Tactic:
use kl.2

Goal state after:
case h
A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ n = kl.1 * kl.2
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : ¬m = n + 1
⊢ IsMin (pred^[n.succ] i0)

Tactic:
exact isMin_iterate_pred_of_eq_of_ne h_eq.symm (Ne.symm hmn)

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case pos
α : 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
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n

Tactic:
simpa [Order.succ_eq_iff_isMax.mpr h'm] using ih

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ x ∈ range n, f (x + 1) (n - x) ^ n.choose (x + 1)) * f (n + 1) (n - n) ^ n.choose (n + 1) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i

Tactic:
prod_range_succ'

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ x ∈ range n, f (x + 1) (n - x) ^ n.choose (x + 1)) * f (n + 1) (n - n) ^ n.choose (n + 1) * f 0 (n + 1) =
    (∏ k ∈ range n, f (k + 1) (n + 1 - (k + 1)) ^ n.choose (k + 1)) * f 0 (n + 1 - 0) ^ n.choose 0
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
⊢ 1 ∈ J

Tactic:
rcases hqf.mul_inv_cancel (mt Ideal.Quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩

Goal state after:
case right.mk
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : (mk I) x * Quot.mk (⇑(Submodule.quotientRel I)) y = 1
⊢ 1 ∈ J
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i
⊢ ∏ i ∈ range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i =
    (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i

Tactic:
prod_range_succ'

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i
⊢ (∏ k ∈ range (n + 1), f (k + 1) (n + 1 - (k + 1)) ^ (n + 1).choose (k + 1)) * f 0 (n + 1 - 0) ^ (n + 1).choose 0 =
    (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
⊢ ∀ {x y : Set α},
    x ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b} →
      y ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b} → x ∩ y ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b}

Tactic:
rintro x y ⟨a, ha, b, hb, rfl⟩ ⟨c, hc, d, hd, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
c : Set α
hc : c ∈ f
d : Set α
hd : d ∈ g
⊢ a ∩ b ∩ (c ∩ d) ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b}
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ h.filterBasis.filter = generate {U | ∃ i, p i ∧ s i = U}

Tactic:
← h.filterBasis.generate,

Goal state after:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ generate h.filterBasis.sets = generate {U | ∃ i, p i ∧ s i = U}
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ioi i

Tactic:
· rcases h.exists_between hx with ⟨y, hys, _, hyx⟩
    exact mem_biUnion hys hyx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
⊢ Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g

Tactic:
by
  rw [Tendsto, ← map_compose]
  simp only [(· ∘ ·), map_comap_of_mem h, Tendsto]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
h : f ⁻¹' s i ⊆ t
y : α
hy : y ∈ s i
x : β
hx : f x = y
⊢ x ∈ f ⁻¹' s i

Tactic:
mem_preimage,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
h : f ⁻¹' s i ⊆ t
y : α
hy : y ∈ s i
x : β
hx : f x = y
⊢ f x ∈ s i
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
f g : α → β
⊢ f =ᶠ[⊤] g ↔ f = g

Tactic:
by simp [EventuallyEq, funext_iff]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Tendsto

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) = upperBounds (range f)

Tactic:
refine Subset.antisymm ?_ (upperBounds_mono_set <| range_comp_subset_range _ _)
  rintro c hc _ ⟨b, rfl⟩
  obtain ⟨a, ha⟩ : ∃ a, b ≤ g a := (hg.eventually_ge_atTop b).exists
  exact (hf ha).trans <| hc <| mem_range_self _

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s') → (span R s).FG

Tactic:
intro ⟨s', _, h⟩
    exact ⟨s', h.symm⟩

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
⊢ x ∈ Submodule.span R≥0 {1, -1}

Tactic:
obtain hx | hx := le_total 0 x

Goal state after:
case inl
R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
hx : 0 ≤ x
⊢ x ∈ Submodule.span R≥0 {1, -1}

case inr
R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
hx : x ≤ 0
⊢ x ∈ Submodule.span R≥0 {1, -1}
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
⊢ IsNormal (g ∘ f)

Tactic:
refine ⟨hg.strictMono.comp hf.strictMono, fun ha b hb ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a✝ : α
ha : IsSuccLimit a✝
b : γ
hb : b ∈ upperBounds (g ∘ f '' Iio a✝)
⊢ (g ∘ f) a✝ ≤ b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ sSup (f ⁻¹' Iic x) ∈ f ⁻¹' Iic x

Tactic:
mem_preimage,

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ f (sSup (f ⁻¹' Iic x)) ∈ Iic x
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' : Ordinal.liftPrincipalSeg.toRelEmbedding o = o✝
⊢ lift.{max (u + 1) v, u} o.card < univ.{u, v}

Tactic:
apply lift_lt_univ'

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
n : ℕ
⊢ a + ↑n = b + ↑n ↔ a = b

Tactic:
by
  simp only [le_antisymm_iff, add_le_add_iff_right]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a + b - (a + c) = b - c

Tactic:
rw [← sub_sub, add_sub_cancel]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
⊢ a - b < c

Tactic:
by
  obtain hab | hba := lt_or_ge a b
  · rwa [Ordinal.sub_eq_zero_iff_le.2 hab.le]
  · rwa [sub_lt_of_le hba]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f
a : Ordinal.{max u v}
⊢ a < o.bsup f → succ a < o.bsup f

Tactic:
← iSup_eq_bsup

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ iSup (o.familyOfBFamily f)
a : Ordinal.{max u v}
⊢ a < iSup (o.familyOfBFamily f) → succ a < iSup (o.familyOfBFamily f)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f
a : Ordinal.{max u v}
⊢ a < o.bsup f → succ a < o.bsup f

Tactic:
by
  rw [← iSup_eq_bsup] at *
  exact succ_lt_iSup_of_ne_iSup fun i => hf _

Goal state after: