mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
h : g i • i y = g i • a y
⊢ g i = 0

Tactic:
rw [← sub_eq_zero, ← smul_sub, smul_eq_zero] at h

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
h : g i = 0 ∨ i y - a y = 0
⊢ g i = 0
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t'

Tactic:
xgcdAux

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| if _hr : r = 0 then (r', s', t')
  else
    have q := r' / r;
    have x := ⋯;
    xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ (insert a s).encard = s.encard + 1

Tactic:
by
  rw [← union_singleton, encard_union_eq (by simpa), encard_singleton]

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
i : ι
hit : i ∈ t
⊢ ∀ x ∈ t, x ∉ s → g x • v x = 0

Tactic:
exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ∞
hk : k ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = k

Tactic:
induction k using ENat.nat_induction with

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).encard = s.encard + t.encard

Tactic:
encard_union_eq h

Goal state after:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
⊢ s.encard + t.encard = s.encard + t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : s ∪ t ≠ univ
⊢ (s ∩ t).Nonempty

Tactic:
replace h := (ncard_lt_card h).trans_le h'

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard
⊢ (s ∩ t).Nonempty
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
⊢ (Set.range g)ᶜ.ncard ≤ 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : (Set.range g)ᶜ.ncard ≤ 1
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
⊢ (Set.range g)ᶜ.ncard ≤ 1
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
a b : M
n1 : N
fa : f a = n1
n2 : N
fb : f b = n2
h : (conGen rel) n1 n2
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
induction h generalizing a b with

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ f : M →* P
x✝ : ↥(MonoidHom.mrange (kerLift f))
w : P
z : (ker f).Quotient
hz : (kerLift f) z = w
⊢ (kerLift f).mrangeRestrict z = ⟨w, ⋯⟩

Tactic:
rcases hz with ⟨⟩; rfl

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
⊢ Nonempty (Unique (M ⧸ ⊤))

Tactic:
exact ⟨QuotientTop.unique⟩

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

Goal state before:
pp: case succ.hin.refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i ≤ succ^[n.succ] i

Tactic:
Function.iterate_succ_apply'

Goal state after:
case succ.hin.refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i ≤ succ (succ^[n] i)
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b c : M
⊢ (fun x ↦ a + x) '' Ico b c = Ico (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Ico]

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

Goal state before:
pp: case succ
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
hn : succ^[n] i < j
⊢ succ^[n + 1] i ≤ j

Tactic:
rw [Function.iterate_succ', Function.comp_apply]

Goal state after:
case succ
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
hn : succ^[n] i < j
⊢ succ (succ^[n] i) ≤ j
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case e_s
G : Type u_4
inst✝ : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ Ico n m = {k ∈ range m | n ≤ k}

Tactic:
apply Finset.ext

Goal state after:
case e_s
G : Type u_4
inst✝ : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ {k ∈ range m | n ≤ k}
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
hn : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ f i

Tactic:
disjointed_succ,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
hn : ¬IsMax i
⊢ f (succ i) \ (partialSups f) i = f (succ i) \ f i

case hi
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
hn : ¬IsMax i
⊢ ¬IsMax i
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case neg
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n < m
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
replace h := h.le
    rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]

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

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ range n, i = n * (n - 1) / 2

Tactic:
by
  rw [← sum_range_id_mul_two n, Nat.mul_div_cancel _ Nat.zero_lt_two]

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) =
    cons (n + 1, 0)
      (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯

Tactic:
apply eq_of_veq
  rw [cons_val, map_val]
  exact Multiset.Nat.antidiagonal_succ'

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
this : 2 • (a * b * a) = 0
⊢ (1 + 1) • (a * b * a) = 0

Tactic:
exact this

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

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} = span {y} ↔ Associated x y

Tactic:
rw [← dvd_dvd_iff_associated, le_antisymm_iff, and_comm]

Goal state after:
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {y} ≤ span {x} ∧ span {x} ≤ span {y} ↔ x ∣ y ∧ y ∣ x
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case cons
α : 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
⊢ (a ::ₘ s).sum ^ ((a ::ₘ s).card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) (a ::ₘ s)).toFinset

Tactic:
simp only [Finset.coe_insert, Multiset.map_cons, Multiset.toFinset_cons, Multiset.sum_cons,
    Multiset.card_cons, add_pow]

Goal state after:
case cons
α : 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
⊢ ∑ m ∈ Finset.range ((s.card + 1) * n + 1 + 1),
      a ^ m * s.sum ^ ((s.card + 1) * n + 1 - m) * ↑(((s.card + 1) * n + 1).choose m) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
n : ℕ
⊢ ∑ m ∈ range (n + 1 + 1), (-1) ^ m * ↑((n + 1).choose m) = if n + 1 = 0 then 1 else 0

Tactic:
simp [Int.alternating_sum_range_choose_eq_choose]

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

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : (Finsupp.linearCombination α Subtype.val) f = 1
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
simp only [Finsupp.linearCombination, Finsupp.coe_lsum, Finsupp.sum, LinearMap.coe_smulRight,
    LinearMap.id_coe, id_eq, smul_eq_mul] at hf

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
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

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

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

Goal state before:
pp: case single
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
i : ι
r : R i
⊢ Pi.single i r ∈ span (range fun i ↦ Pi.single i 1)

Tactic:
rw [show Pi.single i r = Pi.single i r * Pi.single i 1 by simp [← Pi.single_mul_left]]
      exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨i, rfl⟩)

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

Goal state before:
pp: α : Type u
f : Filter α
⊢ ¬f = ⊥ ↔ f.NeBot

Tactic:
neBot_iff

Goal state after:
α : Type u
f : Filter α
⊢ ¬f = ⊥ ↔ f ≠ ⊥
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ i, a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

Tactic:
filter_upwards with i

Goal state after:
case inr
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ i, a ∈ s i
i : ι
⊢ (s i).piecewise f g a = (⋃ i, s i).piecewise f g a
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:
neBot_iff

Goal state after:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : comap m g ≠ ⊥
⊢ g ≠ ⊥
Module: Mathlib.Order.Interval.Set.Disjoint

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

Tactic:
exact mem_iUnion₂.mpr ⟨a, a_mem, hx⟩

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

Goal state before:
pp: α : Type u_1
f g : Filter α
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x

Tactic:
simp only [inf_neBot_iff, frequently_iff, and_comm]

Goal state after:
α : Type u_1
f g : Filter α
⊢ (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → (s ∩ s').Nonempty) ↔
    ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ x, p x ∧ x ∈ U
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
⊢ (∃ᶠ (x : α) in f, True) ↔ f.NeBot

Tactic:
by
  simp [frequently_iff_neBot]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
⊢ map id f = map (⇑e) (comap (⇑e) f)

Tactic:
map_id,

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
⊢ f = map (⇑e) (comap (⇑e) f)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
g : α → β
f : Filter α
⊢ (pure g).seq f = map g f

Tactic:
refine le_antisymm (le_map fun s hs => ?_) (le_seq fun s hs t ht => ?_)
  · rw [← singleton_seq]
    apply seq_mem_seq _ hs
    exact singleton_mem_pure
  · refine sets_of_superset (map g f) (image_mem_map ht) ?_
    rintro b ⟨a, ha, rfl⟩
    exact ⟨g, hs, a, ha, rfl⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ n s, span R (range s) = N

Tactic:
fg_def

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) ↔ ∃ n s, span R (range s) = N
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:
exact le_sup_right

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:
fg_def

Goal state after:
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 : ι), ∃ S, S.Finite ∧ span R S = p i
⊢ ∃ S, S.Finite ∧ span R S = pi univ p
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
S : Type u_3
P : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid P
inst✝² : Module S P
σ : R →+* S
inst✝¹ : RingHomSurjective σ
inst✝ : Module.Finite R M
f : M →ₛₗ[σ] P
⊢ f.range.FG

Tactic:
rw [LinearMap.range_eq_map]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_3
P : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid P
inst✝² : Module S P
σ : R →+* S
inst✝¹ : RingHomSurjective σ
inst✝ : Module.Finite R M
f : M →ₛₗ[σ] P
⊢ (map f ⊤).FG
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 : ⊤.FG
⊢ ⊤.FG

Tactic:
fg_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 : ∃ S, S.Finite ∧ span R S = ⊤
⊢ ∃ S, S.Finite ∧ span A S = ⊤
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : SuccOrder α
inst✝ : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
⊢ IsNormal f

Tactic:
by
  refine ⟨fun a b ↦ ?_, fun ha ↦ (hl ha).2⟩
  induction b using SuccOrder.limitRecOn with
  | isMin b hb => exact hb.not_lt.elim
  | succ b hb IH =>
    intro hab
    obtain rfl | h := (lt_succ_iff_eq_or_lt_of_not_isMax hb).1 hab
    · exact hs a
    · exact (IH h).trans (hs b)
  | isSuccLimit b hb IH =>
    intro hab
    have hab' := hb.succ_lt hab
    exact (IH _ hab' (lt_succ_of_not_isMax hab.not_isMax)).trans_le
      ((hl hb).1 (mem_image_of_mem _ hab'))

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, v}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
exact this

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

Goal state before:
pp: case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≼i s

pp: case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≼i s)
f : r ≼i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Tactic:
· exact (RelIso.preimage Equiv.ulift r).symm.toInitialSeg.trans
      (f.trans (RelIso.preimage Equiv.ulift s).toInitialSeg)

Goal state after:
case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≼i s)
f : r ≼i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ IsNormal fun x ↦ a + x

Tactic:
rw [isNormal_iff]
  exact ⟨add_right_strictMono, fun _ l _ ↦ (add_le_iff_of_isSuccLimit l).2⟩

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

Goal state before:
pp: case mpr
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds s
⊢ BddAbove ((fun x ↦ x + 1) '' s)

Tactic:
use a + 1

Goal state after:
case h
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds s
⊢ a + 1 ∈ upperBounds ((fun x ↦ x + 1) '' s)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ ⨆ a, f ↑a ⋯ = o.bsup f

Tactic:
Iio,

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ ⨆ a, f ↑a ⋯ = o.bsup f
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

pp: case inr.inr
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
· have := hb.ne'
    by_cases c = 0 <;> simp_all

Goal state after:
case inr.inr
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
⊢ a ^ (b * c) = (a ^ b) ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr.inr
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [mul_add_one, opow_add, IH, opow_add_one]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_mul_right hb)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using (opow_le_of_isSuccLimit (opow_ne_zero _ ha) l).symm

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

Goal state before:
pp: case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o = 0

Tactic:
· rwa [← nonpos_iff_eq_zero, ← lt_add_one_iff, zero_add, ← lt_opow_iff_log_lt hb ho, opow_one]

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
⊢ IsPrincipal op (sSup s)

Tactic:
have : IsPrincipal op (sSup ∅) := by simp

Goal state after:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
⊢ IsPrincipal op (sSup s)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a * ↑⟨c, hcb⟩ ≤ b ^ succ (log b a)

Tactic:
apply (mul_le_mul_left (le_of_lt (lt_mul_succ_div a hbo₀)) c).trans

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o ≤ ω_ ↑n ↔ o ≤ ω_ ↑n

Tactic:
simpa using lift_le (b := ω_ n)

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

Goal state before:
pp: β : Type v
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : Cardinal.lift.{u, v} #β < (lift.{v, u} (⨆ i, f i + 1)).cof
⊢ False

Tactic:
exact (lift_iSup_add_one_lt_of_lt_cof hf <| Ordinal.lt_iSup_add_one _).false

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

Goal state before:
pp: case refine_2
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o.blsub f = a

pp: case refine_2.hg
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o'.blsub g = o

Tactic:
· exact hf.2.2

Goal state after:
case refine_2.hg
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o'.blsub g = o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.inr
a b : Ordinal.{u_1}
hb✝ : b ≠ 0
hb : IsSuccLimit b
⊢ (a + b).cof = b.cof

Tactic:
· exact cof_map_of_isNormal (isNormal_add_right a) hb

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

Goal state before:
pp: c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
⊢ #↑(⋃ i, t i) < c ↔ ∀ (i : ι), #↑(t i) < c

Tactic:
refine ⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩

Goal state after:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #↑(⋃ i, t i) < c
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
⊢ ∃ a, Uncountable ↑(f ⁻¹' {a})

Tactic:
simp_rw [← Cardinal.aleph0_lt_mk_iff, ← aleph_one_le_iff]

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
⊢ ∃ a, ℵ_ 1 ≤ #↑(f ⁻¹' {a})