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 * ∑ i, ↑a / m / m ^ ↑i % m * m ^ ↑i = ↑a

Tactic:
ih _ (Nat.div_lt_of_lt_mul (a.is_lt.trans_eq (pow_succ' _ _))),

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 % m + m * (↑a / m) = ↑a
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
a b c : Fin n
⊢ c * a + b * c = a * c + b * c

Tactic:
mul_comm

Goal state after:
n : ℕ
a b c : Fin n
⊢ a * c + b * c = a * c + b * c
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β

Tactic:
classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]

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

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Fintype α
⊢ α ≃ Fin (Nat.card α)

pp: case inr
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Infinite α
⊢ α ≃ Fin (Nat.card α)

Tactic:
· simpa only [card_eq_fintype_card] using Fintype.equivFin α

Goal state after:
case inr
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Infinite α
⊢ α ≃ Fin (Nat.card α)
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + m / k * k = m

Tactic:
mul_comm

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + k * (m / k) = m
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m / k * k + m % k = m

Tactic:
mul_comm

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ k * (m / k) + m % k = m
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬a * b ≺ b

Tactic:
mul_comm

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ⨆ i, lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
apply ciSup_le'

Goal state after:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ∀ (i : { s // LinearIndepOn R id s }), lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s \ t).encard + (s ∩ t).encard + t.encard = s.encard + t.encard

Tactic:
encard_sdiff_add_encard_inter

Goal state after:
α : Type u_1
s t : Set α
⊢ s.encard + t.encard = s.encard + t.encard
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
p : Submodule R M
⊢ Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p

Tactic:
simpa using lift_rank_map_le f p

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

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : (t \ s).encard ≤ 0
⊢ s = t

Tactic:
rw [nonpos_iff_eq_zero, encard_eq_zero, sdiff_eq_empty] at hdiff

Goal state after:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : t ⊆ s
⊢ s = t
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
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i : ι
⊢ ∑ i, g i • v i = 0

Tactic:
rw [← hs]

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
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i : ι
⊢ ∑ i, g i • v i = ∑ i ∈ s, g i • v i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ s.ncard ≤ t.ncard

Tactic:
by
  rw [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset hst).cast_ncard_eq]
  exact encard_mono hst

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
h : Cardinal.mk ↑(𝒫 s) = 2 ^ Cardinal.mk ↑s
⊢ (𝒫 s).ncard = 2 ^ s.ncard

Tactic:
rw [← cast_ncard hs.powerset, ← cast_ncard hs] at h

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
h : ↑(𝒫 s).ncard = 2 ^ ↑s.ncard
⊢ (𝒫 s).ncard = 2 ^ s.ncard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s

Tactic:
intro h
    apply (h y).mpr
    rw [mul_inv_cancel]
    exact s.one_mem

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

Goal state before:
pp: case inr
α : Type u_1
s : Set α
hs : s.Finite
x : α
ht : (insert x s).Infinite
⊢ False

Tactic:
exact ht (hs.insert x)

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 ι
inst✝ : Finite ι
⊢ ⨆ i, (single R φ i).range = ⊤

Tactic:
simpa using iInf_ker_proj_le_iSup_range_single R φ Set.finite_univ isCompl_top_bot.codisjoint

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
⊢ ↑(Ico (succ a) b) = ↑(Ioo a b)

Tactic:
simpa using Set.Ico_succ_left_eq_Ioo _ _

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
by
    convert! (Finset.sup_inf_distrib_left s.toFinset id a).le using 1
    rw [Finset.sup_eq_iSup]
    simp_rw [Set.mem_toFinset]
    rfl

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✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
n : ℕ
f : M →ₗ[R] M₂ →ₗ[R] M₃
g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃
r : R
x : M
z : M₂
⊢ ((f (r • x)).vecCons (g (r • x))) z = ((RingHom.id R) r • (f x).vecCons (g x)) z

Tactic:
by simp [Matrix.smul_cons r (f x z)]

Goal state after:
Module: Mathlib.Order.PartialSups

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

pp: case pos.refine_2
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range fun i ↦ (partialSups f) i)

Tactic:
· simpa only [partialSups_eq_ciSup_Iic] using ciSup_le fun i ↦ le_ciSup h _

Goal state after:
case pos.refine_2
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range fun i ↦ (partialSups f) i)
Module: Mathlib.LinearAlgebra.Prod

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
M₅ : Type u_1
M₆ : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Unique M₂
⊢ ∀ (c : R) (x : M₂ × M), AddEquiv.uniqueProd (c • x) = c • AddEquiv.uniqueProd x

Tactic:
simp [AddEquiv.uniqueProd]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
a b : α
inst✝⁴ : LinearOrder α
inst✝³ : LocallyFiniteOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
hab : a ≤ b
f : α → M
⊢ (∏ x ∈ Ico a b, f x) * f b = f b * ∏ x ∈ Ico a b, f x

Tactic:
mul_comm

Goal state after:
α : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
a b : α
inst✝⁴ : LinearOrder α
inst✝³ : LocallyFiniteOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
hab : a ≤ b
f : α → M
⊢ f b * ∏ x ∈ Ico a b, f x = f b * ∏ x ∈ Ico a b, f x
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ f a * ∏ i < a, f i = (∏ i < a, f i) * f a

Tactic:
mul_comm

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ f (a + 1) * ∏ i ≤ a, f i = (∏ i ≤ a, f i) * f (a + 1)

Tactic:
mul_comm

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
| (∏ k ∈ range n, ∏ x ∈ disjointed s (k + 1), g x) * ∏ x ∈ disjointed s 0, g x

Tactic:
mul_comm

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
| (∏ x ∈ disjointed s 0, g x) * ∏ k ∈ range n, ∏ x ∈ disjointed s (k + 1), g x
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ f b * ∏ x ∈ Ico a b, f x = (∏ k ∈ Ico a b, f k) * f b

Tactic:
mul_comm

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ (∏ x ∈ Ico a b, f x) * f b = (∏ k ∈ Ico a b, f k) * f b
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: δ : Type u_4
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ Ico m n, f k) * ∏ k ∈ range m, f k = ∏ k ∈ range n, f k

Tactic:
mul_comm

Goal state after:
δ : Type u_4
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k = ∏ k ∈ range n, f k
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: case h
A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : n = kl.1 * kl.2
⊢ n = kl.2 * kl.1

Tactic:
mul_comm

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 : n = kl.2 * kl.1
⊢ n = kl.2 * kl.1
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b).1 + (a, b).2 = n ∧ (a, b).1 = m ↔ if m ≤ n then a = m ∧ b = n - m else (a, b) ∈ ∅

Tactic:
ite_prop_iff_or

Goal state after:
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b).1 + (a, b).2 = n ∧ (a, b).1 = m ↔ m ≤ n ∧ a = m ∧ b = n - m ∨ ¬m ≤ n ∧ (a, b) ∈ ∅
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
h✝ : IsEmpty ι
⊢ Countable ι

Tactic:
infer_instance

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

Goal state before:
pp: A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : A
p : Multiplicative A × Multiplicative A
⊢ p.1 * p.2 = ofAdd a ↔ toAdd p.1 + toAdd p.2 = a

Tactic:
Multiplicative.ext_iff,

Goal state after:
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : A
p : Multiplicative A × Multiplicative A
⊢ toAdd (p.1 * p.2) = toAdd (ofAdd a) ↔ toAdd p.1 + toAdd p.2 = a
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Goal state after:
case inl
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : IsEmpty ι
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)

case inr
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ n ! * (n + 1) = (n + 1) * n !

Tactic:
mul_comm

Goal state after:
n : ℕ
⊢ (n + 1) * n ! = (n + 1) * n !
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ n ∈ I

Tactic:
by
  rw [← Nat.add_sub_of_le h, add_comm, pow_add]
  exact I.mul_mem_left _ ha

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

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

Tactic:
rw [span_pair_comm, span_insert_zero]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x y x✝ : α
⊢ x = x✝ * y ↔ x = y * x✝

Tactic:
mul_comm

Goal state after:
α : Type u
inst✝ : CommSemiring α
x y x✝ : α
⊢ x = y * x✝ ↔ x = y * x✝
Module: Mathlib.Data.Nat.Choose.Sum

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

Tactic:
mul_comm

Goal state after:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 * (2 ^ 2) ^ m = 2 * 4 ^ m
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ n * 2 ^ n = 2 * (n * 2 ^ (n - 1))

Tactic:
by
      rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]

Goal state after:
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 ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (n + 1) * (a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c)) + 0

Tactic:
simp_rw [← mul_assoc]

Goal state after:
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 ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (n + 1) * a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) + 0
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsPrincipalIdealRing α
p : α
hp : Prime p
hP : span {p} ≠ ⊥
⊢ p ≠ 0

Tactic:
by simp [hp.ne_zero]

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

Goal state before:
pp: α : Type u_1
B : FilterBasis α
⊢ generate B.sets = B.filter

Tactic:
apply le_antisymm
  · intro U U_in
    rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩
    exact GenerateSets.superset (GenerateSets.basic V_in) h
  · rw [le_generate_iff]
    apply mem_filter_of_mem

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
⊢ (mapRange.linearMap f) { support := x.support, toFun := y, mem_support_toFun := ⋯ } = x

Tactic:
ext; simp_all

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

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
⊢ (⨅ i, l i).HasBasis (fun ii' ↦ p ii'.fst ii'.snd) fun ii' ↦ s ii'.fst ii'.snd

Tactic:
refine ⟨fun t => ?_⟩
  rw [mem_iInf_of_directed h, Sigma.exists]
  exact exists_congr fun i => (hl i).mem_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : (comap m g).NeBot
⊢ g.NeBot

Tactic:
rw [neBot_iff] at *
  contrapose h
  rw [h]
  exact comap_bot

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

Goal state before:
pp: α : Type u
f : Filter α
p q : α → Prop
h : ∀ᶠ (x : α) in f, p x ↔ q x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∀ᶠ (x : α) in f, q x ↔ p x

Tactic:
by simpa only [Iff.comm] using h

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

Goal state before:

Tactic:
map f (F ⊓ comap f G) ≤ map f F ⊓ (map f <| comap f G) := map_inf_le
      _ ≤ map f F ⊓ G := inf_le_inf_left (map f F) map_comap_le

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

Goal state before:
pp: α : Type u_6
inst✝ : Preorder α
h : atTop.NeBot
x y : α
⊢ ∃ c, x ≤ c ∧ y ≤ c

Tactic:
exact ((eventually_ge_atTop x).and (eventually_ge_atTop y)).exists

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e✝ : G ≃ Fin n
f : Fin n ≃ ULift.{?u.25, 0} (Fin n) := Equiv.ulift.symm
e : G ≃ ULift.{?u.25, 0} (Fin n) := e✝.trans f
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
let groupH : Group (ULift (Fin n)) := e.symm.group

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e✝ : G ≃ Fin n
f : Fin n ≃ ULift.{?u.25, 0} (Fin n) := Equiv.ulift.symm
e : G ≃ ULift.{?u.25, 0} (Fin n) := e✝.trans f
groupH : Group (ULift.{?u.25, 0} (Fin n)) := e.symm.group
⊢ ∃ G' x x_1, Nonempty (G ≃* G')
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring R
e✝ e : α ≃ β
inst✝¹ : AddCommMonoid β
inst✝ : Module R β
this : AddCommMonoid α := e.addCommMonoid
⊢ ∀ (x : α), 0 • x = 0

Tactic:
by simp [smul_def, zero_smul, zero_def]

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

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
l : ℕ
h : l < m
⊢ (f ^ l).ker ≤ (f ^ m).ker

Tactic:
exact f.iterateKer.monotone h.le

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
ι : Sort u_3
inst✝ : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), (N i).FG
⊢ (iSup N).FG

Tactic:
cases nonempty_fintype (PLift ι)

Goal state after:
case intro
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Sort u_3
inst✝ : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), (N i).FG
val✝ : Fintype (PLift ι)
⊢ (iSup N).FG
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
P Q : { P // P.FG }
⊢ Q ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
by rw [← Subtype.coe_le_coe]; exact le_sup_right

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupInaccOn D (s ∪ t)

Tactic:
rw [← dirSupClosedOn_compl, compl_union]

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (sᶜ ∩ tᶜ)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
A : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
S : Submodule A M
inst✝ : Module.Finite R A
hS : S.FG
⊢ (Submodule.restrictScalars R S).FG

Tactic:
rw [← Module.Finite.iff_fg] at *
  exact Module.Finite.trans A S

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ cof α = #α

Tactic:
rw [← card_type LT.lt, ← ord_cof_eq_type_lt, card_ord]

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

Goal state before:
pp: a : Ordinal.{u_4}
⊢ 0 - a = 0

Tactic:
by simpa using sub_le_self 0 _

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u}
⊢ Small.{u, u + 1} ↑(Iio o ∪ {o})

Tactic:
infer_instance

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

Goal state before:
pp: a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = 1 * a

Tactic:
one_mul a

Goal state after:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = a
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
obtain ⟨b, hb, hba⟩ := hs a

Goal state after:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o a : Ordinal.{u}
ha : a ∈ upperBounds (enumOrd s '' Iio o)
b : Ordinal.{u}
hb : b ∈ s
hba : a < b
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
a b : Ordinal.{u_4}
h : a ≤ b
⊢ a / 0 ≤ b / 0

Tactic:
div_zero,

Goal state after:
case inl
a b : Ordinal.{u_4}
h : a ≤ b
⊢ 0 ≤ b / 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
div_zero,

Goal state after:
case inl
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
⊢ 0 = b / 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ (a * b + c) / (a * d) < succ (b / d)

Tactic:
← lt_mul_iff_div_lt H,

Goal state after:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + c < a * d * succ (b / d)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ a * (b - c) = a * b - a * c

Tactic:
refine eq_of_forall_ge_iff fun d ↦ ?_
    rw [sub_le, mul_le_iff_le_div ha, sub_le, mul_le_iff_le_div ha, mul_add_div _ ha]

Goal state after: