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 : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝ i)
n : Fin m → ℕ
nn : ℕ
f : (i : Fin m) → Fin (n i)
⊢ ∀ (fn : Fin nn), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * nn

Tactic:
fn

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝ i)
n : Fin m → ℕ
nn : ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin nn
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * nn
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
⊢ ∀ (g : ι ⊕ ι' → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Tactic:
g

Goal state after:
case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
⊢ ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
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
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 f i < g i, (if g i ≤ f i then f i - g i else g i - f i) • v i +
    (∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)

Tactic:
rw [add_left_comm, ← Finset.sum_add_distrib]

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
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, g i • v i +
    ∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : ↑m ∣ ↑(↑b - ↑a).natAbs ∧ ↑n ∣ ↑b - ↑a
⊢ a ≡ b [MOD m * n]

Tactic:
Int.natCast_dvd_natCast,

Goal state after:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ ↑n ∣ ↑b - ↑a
⊢ a ≡ b [MOD m * n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = a % c + b % c

Tactic:
← add_mod_add_ite,

Goal state after:
a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = (a + b) % c + if c ≤ a % c + b % c then c else 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hc : c ≤ a % c + b % c
⊢ (a + b) % c + c = a % c + b % c

Tactic:
← add_mod_add_ite,

Goal state after:
a b c : ℕ
hc : c ≤ a % c + b % c
⊢ (a + b) % c + c = (a + b) % c + if c ≤ a % c + b % c then c else 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case neg
iv : ℕ
ih : ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (iv + 1) → ℕ
hi : iv < iv + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last iv))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j

Tactic:
conv in Sigma.mk _ _ =>
      equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]

Goal state after:
case neg
iv : ℕ
ih : ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (iv + 1) → ℕ
hi : iv < iv + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last iv))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) ⟨Sum.inr 0, j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β

Tactic:
Fintype.card_sum

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

Goal state before:
pp: case insert
α : Type u_1
s : Set α
a✝ : α
s✝ : Set α
hat : a✝ ∉ s✝
hs✝ : s✝.Finite
ht' : s✝.encard < ⊤
⊢ (insert a✝ s✝).encard < ⊤

Tactic:
rw [encard_insert_of_notMem hat]
    exact lt_tsub_iff_right.1 ht'

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
hv : LinearIndependent R v
f : ι →₀ R
⊢ ∀ ⦃a₂ : ι →₀ R⦄, (Finsupp.linearCombination R (-v)) f = (Finsupp.linearCombination R (-v)) a₂ → f = a₂

Tactic:
g

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : LinearIndependent R v
f g : ι →₀ R
⊢ (Finsupp.linearCombination R (-v)) f = (Finsupp.linearCombination R (-v)) g → f = g
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
⊢ Nat.card α = 0

Tactic:
cases finite_or_infinite β
  · have := card_eq_zero_iff.mp h
    have := Function.isEmpty f
    exact Nat.card_of_isEmpty
  · have := Infinite.of_surjective f hf
    exact Nat.card_eq_zero_of_infinite

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

Goal state before:
pp: case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ (insert a s).ncard ≤ s.ncard + 1

Tactic:
rw [(hs.mono (subset_insert a s)).ncard]

Goal state after:
case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ 0 ≤ s.ncard + 1
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ (linearCombination S ⇑b) (b.repr m) ∈ span R (range ⇑b)

Tactic:
Finsupp.linearCombination_apply S _

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ ((b.repr m).sum fun i a ↦ a • b i) ∈ span R (range ⇑b)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
⊢ ∀ (a₁ a₂ : ↥s),
    Quotient.map' ⇑(inclusion h) ⋯ (Quotient.mk'' a₁) = Quotient.map' ⇑(inclusion h) ⋯ (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂

Tactic:
intro a b h

Goal state after:
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h✝ : s ≤ t
a b : ↥s
h : Quotient.map' ⇑(inclusion h✝) ⋯ (Quotient.mk'' a) = Quotient.map' ⇑(inclusion h✝) ⋯ (Quotient.mk'' b)
⊢ Quotient.mk'' a = Quotient.mk'' b
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ (mk' N) (g⁻¹ • x) = (mk' N) x

Tactic:
exact Quotient.sound ⟨g⁻¹, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
⊢ comap ⇑f ⋯ (conGen rel) ≤ conGen (rel on ⇑f)

Tactic:
intro a b h

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (comap ⇑f ⋯ (conGen rel)) a b
⊢ (conGen (rel on ⇑f)) a b
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)
a : (i : ι) → φ i
h : a ∈ ⨅ i, (proj i).ker
⊢ a ∈ ⊥

Tactic:
by
      simp only [mem_iInf, mem_ker, proj_apply] at h
      exact (mem_bot _).2 (funext fun i => h i)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioo (pred a) b ↔ x ∈ Ico a b

Tactic:
rw [mem_Ioo, mem_Ico, pred_lt_iff_of_not_isMin ha]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (pred a) (pred b) = Ico a b

Tactic:
by
  rw [Ioc_pred_right_eq_Ioo, Ioo_pred_left_eq_Ioc_of_not_isMin ha]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case right
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
hy : {y} ⊆ s
⊢ ⇑f ⁻¹' {y} ⊆ ↑(span R (⇑f ⁻¹' s))

Tactic:
exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α ⊕ β → M
⊢ ∀ (y : α ⊕ β → M),
    (Equiv.sumArrowEquivProdArrow α β M).toFun (f + y) =
      (Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun y

Tactic:
g

Goal state after:
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : α ⊕ β → M
⊢ (Equiv.sumArrowEquivProdArrow α β M).toFun (f + g) =
    (Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ p ((Iic i).sup' ⋯ f) ↔ ∀ j ≤ i, p (f j)

Tactic:
apply_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p,

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ (Iic i).sup' ⋯ (p ∘ f) ↔ ∀ j ≤ i, p (f j)

α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ -↑n ≤ toZ i0 (pred^[n] i0)

Tactic:
h_eq,

Goal state after:
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ -↑n ≤ toZ i0 i0
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ (∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i = ∏ i ∈ Ioc m k, f i

Tactic:
rw [← Ioc_union_Ioc_eq_Ioc hmn hnk, prod_union]
  apply disjoint_left.2 fun x hx h'x => _
  intro x hx h'x
  exact lt_irrefl _ ((mem_Ioc.1 h'x).1.trans_le (mem_Ioc.1 hx).2)

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
h_eq,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
⊢ x ^ n.succ * y ^ (n.succ - n.succ) * ↑(n.choose n.succ) = x ^ n.succ * y * y ^ (n - n.succ) * ↑(n.choose n.succ)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x : α
⊢ span {x} = ⊤ ↔ span {1} ≤ span {x}

Tactic:
span_singleton_one,

Goal state after:
α : Type u
inst✝ : CommSemiring α
x : α
⊢ span {x} = ⊤ ↔ ⊤ ≤ span {x}
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ i ∈ range (n + 2), ↑((n + 1).choose i) * f i (n + 1 - i) =
    ∑ i ∈ range (n + 1), ↑(n.choose i) * f i (n + 1 - i) + ∑ i ∈ range (n + 1), ↑(n.choose i) * f (i + 1) (n - i)

Tactic:
by
  simpa only [nsmul_eq_mul] using sum_choose_succ_nsmul f n

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

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔ ∃ a b, (⟨a, b⟩.fst ∈ dom ∧ p ⟨a, b⟩.fst ⟨a, b⟩.snd) ∧ s ⟨a, b⟩.fst ⟨a, b⟩.snd ⊆ t

Tactic:
grind +splitIndPred

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

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔ ∃ a b, ((a, b).1 ∈ dom ∧ p (a, b).1 (a, b).2) ∧ s (a, b).1 (a, b).2 ⊆ t

Tactic:
grind +splitIndPred

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

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q

Tactic:
by
  simp only [frequently_imp_distrib, frequently_const]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → Filter β
p : β → Prop
⊢ (∃ᶠ (y : β) in f.bind m, p y) ↔ ∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y

Tactic:
by
  rw [← not_iff_not]
  simp only [not_frequently, eventually_bind]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ SurjOn m s t

Tactic:
by
  rw [map_surjOn_Iic_iff_le_map, map_principal, principal_mono, SurjOn]

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

Goal state before:
pp: k b : ℕ
x✝ : 0 ≤ b
⊢ b ≤ b + k - k

Tactic:
Nat.add_sub_cancel_right

Goal state after:
k b : ℕ
x✝ : 0 ≤ b
⊢ b ≤ b
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : SemilatticeSup α
f g : β → α
F : Filter β
hf : Tendsto f F atBot
hg : Tendsto g F atBot
⊢ Tendsto (fun x ↦ f x ⊔ g x) F atBot

Tactic:
rw [Filter.tendsto_atBot] at *

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : SemilatticeSup α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, f a ≤ b
hg : ∀ (b : α), ∀ᶠ (a : β) in F, g a ≤ b
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, f a ⊔ g a ≤ b
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
hM : Module.Finite R M
⊢ Module.Finite A M

Tactic:
finite_def,

Goal state after:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
hM : ⊤.FG
⊢ ⊤.FG
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
⊢ d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a_3 : α⦄, IsLUB d a_3 → a_3 ∈ {a}

Tactic:
hdn

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a_2 : α⦄, IsLUB d a_2 → a_2 ∈ {a}
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o.pred = o ↔ IsSuccPrelimit o

Tactic:
obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o
  · simp
  · simp_rw [ho.ordinalPred_eq, ho]

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

Goal state before:
pp: s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ ¬x ∉ s

Tactic:
exact notMem_of_lt_csInf' hx

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

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
⊢ Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)

Tactic:
rw [← typein_lt_typein (Prod.Lex s r), typein_enum]

Goal state after:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : b ≤ 1
n : ℕ
⊢ (if b ≤ 1 then 0 else (log.go n b n).snd) = 0

Tactic:
if_pos hb

Goal state after:
b : ℕ
hb : b ≤ 1
n : ℕ
⊢ 0 = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case case2
b n : ℕ
hb : n < b
h✝ : ¬b ≤ 1
⊢ (log.go n b n).snd = 0

Tactic:
fun_cases log.go with

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

Goal state before:
pp: o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha ↦ succ (f a ha)
b : Ordinal.{u}
hb : b < o
hb' : (fun a ha ↦ succ (f a ha)) b hb = a
⊢ a ∈ o'.brange fun a ha ↦ succ (g a ha)

Tactic:
obtain ⟨c, hc, hc'⟩ := h ⟨b, hb, rfl⟩
    simp_rw [← hc'] at hb'
    exact ⟨c, hc, hb'⟩

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

Goal state before:
pp: b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
H : ∀ b' < b, 1 ^ b' ≤ c
⊢ 1 ≤ c

Tactic:
by simpa only [opow_zero] using H 0 l.bot_lt

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

Goal state before:
pp: case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b (n / b) + 1 - 1

Tactic:
Nat.add_sub_cancel_right

Goal state after:
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b (n / b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a c d : Ordinal.{u_4}
⊢ a % (c * d) % c = (c * (d * (a / (c * d))) + a % (c * d)) % c

Tactic:
mul_add_mod_self

Goal state after:
a c d : Ordinal.{u_4}
⊢ a % (c * d) % c = a % (c * d) % c
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω

Tactic:
· rw [← mul_one_add, one_add_omega0]

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

Goal state before:
pp: case succ
n : ℕ
IH : preOmega ↑n = ↑n
⊢ preOmega ↑(n + 1) = ↑(n + 1)

Tactic:
apply (le_preOmega_self _).antisymm'

Goal state after:
case succ
n : ℕ
IH : preOmega ↑n = ↑n
⊢ preOmega ↑(n + 1) ≤ ↑(n + 1)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ typeLT Cardinal.{u_1} ≤ (cof Cardinal.{u_1}).ord

Tactic:
simp [Order.cof_cardinal]

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

Goal state before:
pp: case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ succ b ≤ d

Tactic:
have := le_nfp (a * ·) (a ^ ω * b + c)

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ nfp (fun x ↦ a * x) (a ^ ω * b + c)
⊢ succ b ≤ d
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ StrictMono preBeth

Tactic:
intro a b h

Goal state after:
a b : Ordinal.{u_1}
h : a < b
⊢ preBeth a < preBeth b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
i : ι
⊢ f i * c ≤ (⨆ i, f i) * c

Tactic:
grw [← le_ciSup hf i]

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

Goal state before:
pp: case refine_1
o : Ordinal.{u}
⊢ ∀ b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}, o.cof ≤ b

pp: case refine_2
o : Ordinal.{u}
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
· rintro a ⟨ι, f, hf, rfl⟩
    rw [← hf]
    exact cof_iSup_add_one_le f

Goal state after:
case refine_2
o : Ordinal.{u}
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x✝ : 1 ≠ 0
⊢ StrictMono fun a ↦ ↑1 * a

Tactic:
| =>

Goal state after:
n : ℕ
hn : n ≠ 0
x✝ : 1 ≠ 0
⊢ StrictMono fun a ↦ ↑1 * a