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

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a % m + m * (↑a / m) = ↑a

Tactic:
Nat.mod_add_div

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a = ↑a
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2.specialize_2
ι : 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
h :
  ∀ (s t : Finset ι) (f : ι → R),
    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 : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∑ i ∈ s with g i ≤ f i, (if g i ≤ f i then f i - g i else g i - f i) • v i =
    ∑ i ∈ s with f i < g i, (if g i ≤ f i then f i - g i else g i - f i) • v i

Tactic:
rw [← add_right_cancel_iff
        (a := ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)]
      conv_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]
      conv_rhs => rw [add_left_comm, ← Finset.sum_add_distrib]
      convert! heq
        <;> simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]
        <;> congr! 2 with i hi
        <;> simp only [Finset.mem_filter] at hi
      · simp [hi.2, ← add_smul, tsub_add_cancel_of_le hi.2]
      · simp [hi.2.not_ge, ← add_smul, tsub_add_cancel_of_le hi.2.le]

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

Goal state before:
pp: n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ ↑(finSigmaFinEquiv ij) = ↑ij.snd

Tactic:
by
  rw [finSigmaFinEquiv_apply, add_eq_right]
  apply @Finset.sum_of_isEmpty _ _ _ _ (by simpa using Fin.isEmpty')

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite β
f : α → β
hf : Injective f
⊢ Nat.card α ≤ Nat.card β

Tactic:
simpa using! toNat_le_toNat (lift_mk_le_lift_mk_of_injective hf) (by simp)

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Subsingleton α
⊢ Nat.card α = 1

Tactic:
let := Fintype.ofSubsingleton a
  rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ Nat.card ↑((fun a ↦ (a, b)) '' s) = Nat.card ↑s

Tactic:
Nat.card_image_of_injective (Prod.mk_left_injective b)

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ Nat.card ↑s = Nat.card ↑s
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ 1 ≤ Module.rank R M ↔ ∃ f, Injective ⇑f

Tactic:
nontriviality R
  refine le_rank_iff_exists_linearMap.trans ⟨fun ⟨f, hf⟩ ↦ ?_, fun ⟨f, hf⟩ ↦ ?_⟩
  · exact ⟨f ∘ₗ _, by apply hf.comp (LinearEquiv.piUnique R ..).symm.injective⟩
  · exact ⟨f ∘ₗ _, hf.comp (LinearEquiv.piUnique R ..).injective⟩

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ LinearIndependent R v ↔ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0

Tactic:
by
  simp [linearIndependent_iff_ker, LinearMap.ker_eq_bot']

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

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a s \ {b}).encard = s.encard

Tactic:
← insert_sdiff_singleton_comm (by rintro rfl; exact ha hb),

Goal state after:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a (s \ {b})).encard = s.encard
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ ¬LinearIndependent R v ↔ ∃ l, (Finsupp.linearCombination R v) l = 0 ∧ l ≠ 0

Tactic:
by
  simp [linearIndependent_iff_ker, LinearMap.ker_eq_bot']

Goal state after:
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
⊢ LinearIndependent K v ↔ ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))

Tactic:
by
  apply linearIndependent_iff_eq_zero_of_smul_mem_span.trans
  constructor
  · intro h i h_in_span
    apply one_ne_zero (h i 1 (by simp [h_in_span]))
  · intro h i a ha
    by_contra ha'
    exact False.elim (h _ ((smul_mem_iff _ ha').1 ha))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ a₁ ∈ s, ∀ a₂ ∈ s, a₁ ≠ a₂ → f a₁ ≠ f a₂
this : Function.Injective (MapsTo.restrict f s t hf)
f' : ↑s ↪ ↑t := { toFun := MapsTo.restrict f s t hf, inj' := this }
⊢ s.encard ≤ t.encard

Tactic:
exact f'.encard_le

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.mk α

Tactic:
exact Nat.cast_card

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ (insert a s).ncard = s.ncard + 1

Tactic:
by
  rw [← Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one,
    hs.cast_ncard_eq, encard_insert_of_notMem h]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).ncard = s.ncard - 1

Tactic:
by
  rcases s.infinite_or_finite with hs | hs
  · simp_all [ncard, Infinite.sdiff hs (finite_singleton a)]
  · exact eq_tsub_of_add_eq (ncard_sdiff_singleton_add_one h hs)

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

Goal state before:
pp: case neg
α : Type u_1
s : Set α
a : α
h : a ∉ s
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
rw [sdiff_singleton_eq_self h]

Goal state after:
case neg
α : Type u_1
s : Set α
a : α
h : a ∉ s
⊢ s.ncard - 1 ≤ s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ ¬Even s.ncard ↔ Odd s.ncard

Tactic:
Nat.not_even_iff_odd

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Odd s.ncard ↔ Odd s.ncard
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)

Tactic:
by
  simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard

Tactic:
rw [← ncard_inter_add_ncard_sdiff_eq_ncard s t hs, ← ncard_inter_add_ncard_sdiff_eq_ncard t s ht,
    inter_comm, add_right_inj]

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ ¬Even s.ncard ↔ Odd s.ncard

Tactic:
Nat.not_even_iff_odd

Goal state after:
α : Type u_1
inst✝ : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ Odd s.ncard ↔ Odd s.ncard
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x : M
f : M →ₛₗ[τ₁₂] M₂
h : f x = 0
⊢ R ∙ x ≤ f.ker

Tactic:
rw [span_singleton_le_iff_mem, LinearMap.mem_ker, h]

Goal state after:
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 : ι
⊢ proj i ∘ₗ single R φ j = diag j i

Tactic:
rw [single_eq_pi_diag, proj_pi]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
| f x

Tactic:
rw [pi_eq_sum_univ x, map_sum]

Goal state after:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
| ∑ x_1, f (x x_1 • fun j ↦ if x_1 = j then 1 else 0)
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a - 1 ≤ b
⊢ insert (a - 1) (Icc a b) = Icc (a - 1) b

Tactic:
by
  simpa [← pred_eq_sub_one] using insert_Icc_left_eq_Icc_pred (pred_eq_sub_one a ▸ h)

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ⊤ ≤ fst R M M₂ ⊔ snd R M M₂

Tactic:
rintro ⟨m, n⟩ -

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (m, n) ∈ fst R M M₂ ⊔ snd R M M₂
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ upperBounds (Set.range ⇑(partialSups f)) = upperBounds (Set.range f)

Tactic:
by
  ext a
  simp only [mem_upperBounds, Set.forall_mem_range, partialSups_le_iff]
  exact ⟨fun h _ ↦ h _ _ le_rfl, fun h _ _ _ ↦ h _⟩

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨆ i_1, f ↑i_1 ≤ (Iic i).sup' ⋯ f

Tactic:
exact ciSup_le fun ⟨j, hj⟩ ↦ le_sup' f (by simpa only [mem_Iic, Set.mem_Iic] using hj)

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : j < succFn i
⊢ j ≤ i

Tactic:
by
  rw [lt_isGLB_iff (succFn_spec i)] at hij
  obtain ⟨k, hk_lb, hk⟩ := hij
  rw [mem_lowerBounds] at hk_lb
  exact not_lt.mp fun hi_lt_j ↦ not_le.mpr hk (hk_lb j hi_lt_j)

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∏ i ∈ Icc a b, f i = ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1

Tactic:
rw [← prod_ite_mem_eq, prod_fin_eq_prod_range]

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Icc a b then f ⟨i, h⟩ else 1 else 1) =
    ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∏ i ≤ a, f i.succ / f i.castSucc = f a.succ / f 0

Tactic:
rw [← prod_ite_mem_eq, prod_fin_eq_prod_range]

Goal state after:
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Iic a then f ⟨i, h⟩.succ / f ⟨i, h⟩.castSucc else 1 else 1) =
    f a.succ / f 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ IsIdempotentElem (a + b) ↔ a * b + b * a = 0

Tactic:
by
  refine ⟨fun h ↦ ?_, ha.add hb⟩
  rw [← add_right_cancel_iff (a := b), add_assoc, ← add_left_cancel_iff (a := a),
    ← add_assoc, add_add_add_comm]
  simpa [add_mul, mul_add, ha.eq, hb.eq] using h.eq

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
⊢ span 1 = ⊤

Tactic:
← Set.singleton_one,

Goal state after:
α : Type u
inst✝ : Semiring α
⊢ span {1} = ⊤
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ z ∈ I

Tactic:
← span_eq I

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ z ∈ span ↑I
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r x✝ : (i : ι) → R i
⊢ (∀ (i : ι), ∃ a, a * r i = x✝ i) ↔ ∃ a, ∀ (x : ι), (a * r) x = x✝ x

Tactic:
Classical.skolem,

Goal state after:
ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r x✝ : (i : ι) → R i
⊢ (∃ f, ∀ (x : ι), f x * r x = x✝ x) ↔ ∃ a, ∀ (x : ι), (a * r) x = x✝ x
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(lift I f H)

Tactic:
by
  intro y
  obtain ⟨x, rfl⟩ := hf y
  use Ideal.Quotient.mk I x
  simp only [Ideal.Quotient.lift_mk]

Goal state after:
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:
rw [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.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: 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 : ℕ
⊢ f.iterateMapComap i n K ≤ (fun K ↦ comap f (map i K))^[n + 1] K

Tactic:
rw [iterate_succ', Function.comp_apply, ← iterateMapComap, ← map_le_iff_le_comap]

Goal state after:
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 : ℕ
⊢ map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i = ∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x

pp: case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i = ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)

Tactic:
· refine prod_congr rfl fun i hi ↦ ?_
    rw [tsub_add_eq_add_tsub (this _ hi)]

Goal state after:
case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i = ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case inl
R : Type u_5
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

pp: case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

Tactic:
· exact
      ⟨fun h => (not_isField_of_subsingleton _ h).elim, fun h =>
        (false_of_nontrivial_of_subsingleton <| Ideal R).elim⟩

Goal state after:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := ⋯
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) x)) = f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) y))

Tactic:
simp_rw [← snd_prodOfFinsuppNat, eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
⊢ comap φ (comap ψ G) = comap θ (comap ρ G)

Tactic:
rw [Filter.comap_comap, H, ← Filter.comap_comap]

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ 𝓟 s = 𝓟 t ↔ s = t

Tactic:
simp only [le_antisymm_iff, le_principal_iff, mem_principal]

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

Goal state before:
pp: case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ s
⊢ Ioi x ⊆ Ioi a

Tactic:
exact Ioi_subset_Ioi (h.1 hx)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (s ⁻¹'o fun x1 x2 ↦ x1 ⊇ x2) Subtype.val
ne : S.Nonempty
t : Set α
⊢ Directed ((fun i ↦ 𝓟 (s i)) ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) Subtype.val

Tactic:
← directed_comp

Goal state after:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (fun x1 x2 ↦ x1 ⊇ x2) (s ∘ Subtype.val)
ne : S.Nonempty
t : Set α
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) ((fun i ↦ 𝓟 (s i)) ∘ Subtype.val)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
⊢ ∀ᶠ (x : α) in f, p x

Tactic:
by filter_upwards [h univ] with _ pa using pa (by simp)

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

Goal state before:
pp: α : Type u_6
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ atTop = pure ⊤

Tactic:
by
  rw [isTop_top.atTop_eq, Ici_top, principal_singleton]

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set α
hs : IsCofinal (⇑e '' s)
⊢ IsCofinal s

Tactic:
simpa using e.symm.map_isCofinal hs

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
b : α
hb : b ∈ s
hb' : a ≤ b
⊢ a ∈ s

Tactic:
rwa [ha.eq_of_ge hb'] at hb

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ : Submodule R M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite
span_t₁ : span R t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite
span_t₂ : span R t₂ = N₂
⊢ N₁ ⊔ span R t₂ = N₁ ⊔ N₂

Tactic:
span_t₂

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ : Submodule R M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite
span_t₁ : span R t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite
span_t₂ : span R t₂ = N₂
⊢ N₁ ⊔ N₂ = N₁ ⊔ N₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : SMulWithZero α β
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : MulOneClass β
inst✝² : PosMulMono β
inst✝¹ : MulPosMono β
inst✝ : IsScalarTower α β β
h : Monotone fun x ↦ x • 1
x✝² : α
ha : 0 ≤ x✝²
x✝¹ x✝ : β
hb : x✝¹ ≤ x✝
⊢ x✝² • x✝¹ ≤ x✝² • x✝

Tactic:
by
    have := mul_le_mul_of_nonneg_left hb (by simpa using h ha)
    simpa

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α = 1 ↔ ∃ x, IsTop x

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨t, ht⟩ ↦ ?_⟩
  · obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
    rw [h, mk_set_eq_one_iff] at hs'
    obtain ⟨t, rfl⟩ := hs'
    use t
    rwa [isCofinal_singleton_iff] at hs
  · apply le_antisymm
    · apply (cof_le (s := {t}) _).trans_eq (mk_singleton _)
      rwa [isCofinal_singleton_iff]
    · rw [Cardinal.one_le_iff_ne_zero, cof_ne_zero_iff]
      use t

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α γ : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder γ
f : α → γ
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ cof α = cof γ

Tactic:
by
  simpa using lift_cof_congr_of_strictMono hf hf'

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
⊢ DirSupInaccOn D s

Tactic:
by
  intro d hd₀ hd₁ hd₂ a hda hd₃
  obtain ⟨b, hbd, hb⟩ := h hd₀ hd₁ hd₂ hda hd₃
  exact ⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • b < a₂ • b

Tactic:
simp only [← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
    exact smul_lt_smul_of_pos_right ha hb

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
⊢ b < f a ↔ ∃ a' < a, b < f a'

Tactic:
simpa [mem_upperBounds] using lt_isLUB_iff (hf.isLUB_image_Iio_of_isSuccLimit ha)

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : Sum.Lex r emptyRelation ≼i s
h : Surjective ⇑((InitialSeg.leAdd r emptyRelation).trans f)
⊢ False

Tactic:
simpa using h (f (Sum.inr PUnit.unit))

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

Goal state before:
pp: case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i j : β
hj : i < j
⊢ f i + 1 ≤ ⨆ i, f i

Tactic:
apply (le_ciSup hf' j).trans'

Goal state after:
case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i j : β
hj : i < j
⊢ f i + 1 ≤ f j
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ ∀ b < sInf t, enumOrd s b < a

Tactic:
intro b hb
      by_contra! hb'
      exact hb.not_ge (csInf_le' hb')

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ typeLT α ∈ range succ ↔ ∃ x, IsMax x

Tactic:
simp_rw [← isTop_iff_isMax]

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ typeLT α ∈ range succ ↔ ∃ x, IsTop x