mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
⊢ (quotientQuotientEquivQuotientAux N M h).comp (map M (Subgroup.map (mk' N) M) (mk' N) ⋯) = MonoidHom.id (G ⧸ M)

Tactic:
by ext; simp

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

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H✝ : Type v
inst✝³ : Group H✝
M : Type x
inst✝² : Monoid M
φ : G →* H✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝ : G ⧸ H →* A
⊢ (fun x ↦
        match x with
        | ⟨f, hf⟩ => lift H f ⋯)
      ((fun f ↦ ⟨f.comp (mk' H), ⋯⟩) x✝) =
    x✝

Tactic:
by ext; simp

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

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H✝ : Type v
inst✝³ : Group H✝
M : Type x
inst✝² : Monoid M
φ : G →* H✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝¹ x✝ : ↥(domRestrictHom H A).ker
⊢ (match x✝¹ * x✝ with
    | ⟨f, hf⟩ => lift H f ⋯) =
    (match x✝¹ with
      | ⟨f, hf⟩ => lift H f ⋯) *
      match x✝ with
      | ⟨f, hf⟩ => lift H f ⋯

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: H : Type u_2
I : Type u_3
inst✝¹ : Monoid H
inst✝ : Monoid I
G : Submonoid (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
hG₂ : Bijective (Prod.snd ∘ ⇑G.subtype)
⊢ ∃ e, G = e.toMonoidHom.mgraph

Tactic:
simpa using MonoidHom.exists_mulEquiv_mrange_eq_mgraph hG₁.surjective hG₂.surjective
    fun _ _ ↦ hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm

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

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
⊢ p.mkQ.ker = p

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: ι : Type x
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : (i : ι) → φ i
⊢ ∑ i, Pi.single i (v i) = v

Tactic:
by ext; simp

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₂ = id.coprod 0

Tactic:
by ext; simp

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₂
⊢ snd R M M₂ = coprod 0 id

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_3
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
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ i ∈ J, (proj i).ker
⊢ ↑((codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ ∘ₗ
          pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype)
        ⟨b, hb⟩) =
    ↑(id ⟨b, hb⟩)

Tactic:
ext j

Goal state after:
case refine_3
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
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
⊢ ↑((codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ ∘ₗ
            pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype)
          ⟨b, hb⟩)
      j =
    ↑(id ⟨b, hb⟩) j
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₂
s : Set M
t : Set M₂
⊢ span R (⇑(inl R M M₂) '' s ∪ ⇑(inr R M M₂) '' t) = (span R s).prod (span R t)

Tactic:
rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]

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)
e : (i : ι) → φ i ≃ₗ[R] ψ i
c : R
f : (i : ι) → φ i
⊢ (fun i ↦ (e i) ((c • f) i)) = (RingHom.id R) c • fun i ↦ (e i) (f i)

Tactic:
by ext; simp

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₂
p : Submodule R M
q : Submodule R M₂
⊢ comap (inl R M M₂) (p.prod q) = p

Tactic:
by ext; simp

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₂
p : Submodule R M
q : Submodule R M₂
⊢ comap (inr R M M₂) (p.prod q) = q

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝³ : Finite ι
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : ι → α
⊢ BddAbove (Set.range f)

Tactic:
obtain ⟨M, hM⟩ := Finite.exists_le f

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝³ : Finite ι
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : ι → α
M : α
hM : ∀ (i : ι), f i ≤ M
⊢ BddAbove (Set.range f)
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
by
  by_cases hι : Nonempty ι
  · refine (ciSup_le fun i ↦ ?_).antisymm (ciSup_mono ?_ <| le_partialSups f)
    · simpa only [partialSups_eq_ciSup_Iic] using ciSup_le fun i ↦ le_ciSup h _
    · rwa [bddAbove_range_partialSups]
  · exact congr_arg _ (funext (not_nonempty_iff.mp hι).elim)

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
· rw [iSup, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,
      ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _
        (bddAbove_range_partialSups.not.mpr h)]

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]
  exact Set.image_add_const_Ioo _ _ _

Goal state after:
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 ↦ c + x) (Icc a b) = map (addLeftEmbedding c) (Icc a b)

Tactic:
map_eq_image,

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Icc a b) = image (⇑(addLeftEmbedding c)) (Icc a b)
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 ↦ c + x) (Ico a b) = map (addLeftEmbedding c) (Ico a b)

Tactic:
map_eq_image,

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ico a b) = image (⇑(addLeftEmbedding c)) (Ico a b)
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 ↦ c + x) (Ioc a b) = map (addLeftEmbedding c) (Ioc a b)

Tactic:
map_eq_image,

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioc a b) = image (⇑(addLeftEmbedding c)) (Ioc a b)
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 ↦ c + x) (Ioo a b) = map (addLeftEmbedding c) (Ioo a b)

Tactic:
map_eq_image,

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioo a b) = image (⇑(addLeftEmbedding c)) (Ioo a b)
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) (Icc a b) = map (addRightEmbedding c) (Icc a b)

Tactic:
map_eq_image,

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) (Icc a b) = image (⇑(addRightEmbedding c)) (Icc a b)
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) = map (addRightEmbedding c) (Ico a b)

Tactic:
map_eq_image,

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) = image (⇑(addRightEmbedding c)) (Ico a b)
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) (Ioc a b) = map (addRightEmbedding c) (Ioc a b)

Tactic:
map_eq_image,

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) (Ioc a b) = image (⇑(addRightEmbedding c)) (Ioc a b)
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) (Ioo a b) = map (addRightEmbedding c) (Ioo a b)

Tactic:
map_eq_image,

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) (Ioo a b) = image (⇑(addRightEmbedding c)) (Ioo a b)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

Tactic:
← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)

Goal state after:
case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ image (fun x ↦ n - x) (Ico k m), f j
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (antidiagonal n).card = n + 1

Tactic:
by
  rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : { a // IsIdempotentElem a }
⊢ aᶜᶜ = a

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ 0ᶜ = 1

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ 1ᶜ = 0

Tactic:
by ext; simp

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

Goal state before:
pp: case e_a
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
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
· rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
      by_cases h_eq : i = n
      · rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
      · rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
        rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) ^ (n + 1) = ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))

Tactic:
pow_succ' (x + y),

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
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
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) * (x + y) ^ n = ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
by
  rw [span_pair_comm, span_insert_zero]

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

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

Tactic:
span_pair_neg

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, y} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

Tactic:
refine ⟨a ^ (c - (n + 1)) * s.sum ^ ((Multiset.card s + 1) * n + 1 - c) *
      ((Multiset.card s + 1) * n + 1).choose c, 0, Submodule.zero_mem _, ?_⟩
    rw [mul_comm _ (a ^ (n + 1))]
    simp_rw [← mul_assoc]
    rw [← pow_add, add_zero, add_tsub_cancel_of_le h]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m ∈ x.powerset, (-1) ^ #m = if x = ∅ then 1 else 0

Tactic:
rw [sum_powerset_apply_card]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m ∈ range (#x + 1), (#x).choose m • (-1) ^ m = if x = ∅ then 1 else 0
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
s : Set α
hf : Injective m
h : m '' s ∈ map m f
⊢ s ∈ f

Tactic:
rwa [← preimage_image_eq s hf]

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

Goal state before:
pp: case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ l ≤ l'

Tactic:
rw [hl.le_basis_iff hl']
    simpa using h'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : IsEmpty α
f : α → β
la : Filter α
lb : Filter β
⊢ Tendsto f la lb

Tactic:
by simp only [filter_eq_bot_of_isEmpty la, tendsto_bot]

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

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s

Tactic:
rw [inter_comm, inter_eventuallyEq_left]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val
⊢ IsDirectedOrder ↑s

Tactic:
IsDirectedOrder,

Goal state after:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val
⊢ IsDirected ↑s fun x1 x2 ↦ x1 ≤ x2
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝² : Zero M₀
inst✝¹ : Zero B
inst✝ : SMulWithZero M₀ B
this : Zero A := e.zero
⊢ SMulWithZero M₀ A

Tactic:
exact {
    e.smulZeroClass M₀ with
    zero_smul := by simp [smul_def, zero_def]
  }

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

Goal state before:
pp: case mpr
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ (∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N) → N.FG

Tactic:
· rintro ⟨G, _, g, hg⟩
    have := Fintype.ofFinite (range g)
    exact ⟨(range g).toFinset, by simpa⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulStrictMono α β
ha : 0 < a
hb : 0 < b
⊢ 0 < a • b

Tactic:
simpa only [smul_zero] using smul_lt_smul_of_pos_left hb ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulStrictMono α β
ha : 0 < a
hb : b < 0
⊢ a • b < 0

Tactic:
simpa only [smul_zero] using smul_lt_smul_of_pos_left hb ha

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s

Tactic:
rw [not_isCofinal_iff] at h
  obtain ⟨x, h⟩ := h
  exact ⟨x, fun y hy ↦ (h y hy).le⟩

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), (p i).FG
⊢ (pi univ p).FG

Tactic:
simp_rw [fg_def] at hsb ⊢
    choose t htf hts using hsb
    refine
      ⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `span_image` into `span_image _`
    simp_rw [span_iUnion, span_image _, hts, iSup_map_single]

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
H : ∀ (x : ↑s), ∃ y, ↑x ≤ f y
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #↑s

Tactic:
choose g hg using H

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : ↑s → α
hg : ∀ (x : ↑s), ↑x ≤ f (g x)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #↑s
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ DirSupClosed {a}

Tactic:
intro d hda hdn _ b hb
  rw [hdn.subset_singleton_iff] at hda
  subst hda
  exact mem_singleton_of_eq (hb.unique isLUB_singleton)

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

Goal state before:
pp: 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}

Tactic:
simpa using Submodule.smul_mem (M := R) (.span R≥0 {1, -1}) ⟨-x, neg_nonneg.mpr hx⟩ (x := -1)
      (Submodule.subset_span <| by simp)

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

Goal state before:
pp: c : Cardinal.{u}
this : lift.{max (u + 1) v, u} c < univ.{u, max (u + 1) v}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
univ_umax.{u, v}

Goal state after:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u} c < univ.{u, v}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ (typein r).toRelEmbedding x < succ ((typein r).toRelEmbedding x)

Tactic:
apply lt_succ

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

Goal state before:
pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨o, h⟩ ≤ a

Tactic:
apply ha

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

Goal state before:
pp: o : Ordinal.{u}
ho : IsSuccLimit o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
⊢ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f

Tactic:
exact fun i hi => (hf i hi).trans_le (le_bsup f _ _)

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

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ c < b * (c / b) + b

Tactic:
apply lt_mul_div_add _ b0

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

Goal state before:
pp: case inr
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
hy : y ≠ 0
⊢ log b y < x

Tactic:
exact log_lt_of_lt_pow hy hlt

Goal state after: