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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
⊢ ∏ᶠ (i : α) (_ : i ∈ {a}), f i = f a

Tactic:
by
  rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Ioi a) = Ioo (↑a) n

Tactic:
by
  rw [← attachFin_Ioo_eq_Ioi, map_valEmbedding_attachFin]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
i : ι
⊢ (hli.repr ⟨v i, ⋯⟩) i = 1

Tactic:
simp [hli.repr_eq_single i]

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
⊢ x ^ 1 = x

Tactic:
by
  rw [← natCast_one, epow_natCast, pow_one]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 8 → M
⊢ (∏ i, f i.castSucc) * f (last 7) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Tactic:
prod_univ_seven

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : Fin 8 → M
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (castSucc 6) *
      f (last 7) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

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✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ False

Tactic:
apply LinearIndependent.ne_zero x hv

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✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ v x = 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.zero
ι : Type u_1
M : Type u_2
n : ℕ
ih : ∀ (f : Fin n → Fin 0), ∑ i, ↑(f i) * 0 ^ ↑i < 0 ^ n
f : Fin (n + 1) → Fin 0
⊢ ∑ i, ↑(f i) * 0 ^ ↑i < 0 ^ (n + 1)

pp: case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ (n + 1)

Tactic:
· exact isEmptyElim (f <| Fin.last _)

Goal state after:
case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ (n + 1)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
h : a ≤ b
⊢ a ≡ b [MOD n] ↔ ∃ t, b = a + n * t

Tactic:
modEq_iff_dvd' h,

Goal state after:
n a b : ℕ
h : a ≤ b
⊢ n ∣ b - a ↔ ∃ t, b = a + n * t
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑(n.gcd m) * ↑a + ↑n * n.gcdA m * ↑b - ↑n * n.gcdA m * ↑a) / ↑(n.gcd m)

Tactic:
add_sub_assoc,

Goal state after:
case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑(n.gcd m) * ↑a + (↑n * n.gcdA m * ↑b - ↑n * n.gcdA m * ↑a)) / ↑(n.gcd m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hca : c ∣ b
⊢ (b + a) / c = a / c + b / c

Tactic:
Nat.add_div_of_dvd_right,

Goal state after:
a b c : ℕ
hca : c ∣ b
⊢ b / c + a / c = a / c + b / c

a b c : ℕ
hca : c ∣ b
⊢ c ∣ b
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set M
hdj : Disjoint s t
⊢ LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R (id '' t)) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R t)

Tactic:
image_id

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set M
hdj : Disjoint s t
⊢ LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R t) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R t)
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
h3 : ∀ i ∈ s, g i = 0
⊢ (∑ i ∈ insert a s, g i • ⇑i) 1 = 0

Tactic:
by rw [hg]; rfl

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

Tactic:
obtain (he | he) := isEmpty_or_nonempty ι

Goal state after:
case inl
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
he : IsEmpty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

case inr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ v, LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
this : Injective (⇑(Finsupp.linearCombination R v) ∘ ⇑(Finsupp.linearEquivFunOnFinite R R (Fin n)).symm)
⊢ ∃ f, Injective ⇑f

Tactic:
exact ⟨Finsupp.linearCombination .. ∘ₗ _, this⟩

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : ¬FaithfulSMul R M
⊢ Module.rank R M = 0

Tactic:
by
  contrapose! h
  obtain ⟨f, hf⟩ := by rwa [← Cardinal.one_le_iff_ne_zero, one_le_rank_iff] at h
  exact ⟨fun {x y} hxy ↦ hf (by simpa [← map_smul] using hxy (f 1))⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀

Tactic:
contrapose! h
    rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
    exact n.zero_le

Goal state after:
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'
h : Surjective ⇑f
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Tactic:
rw [← rank_range_of_surjective f h]
  apply lift_rank_range_le

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

Goal state before:
pp: α : Type u_1
P Q : Set α
x✝¹ x✝ : ↑(P ↓∩ Q)
h :
  (fun x ↦
        match x with
        | ⟨⟨x, property⟩, hx⟩ => ⟨x, hx⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨⟨x, property⟩, hx⟩ => ⟨x, hx⟩)
      x✝
⊢ x✝¹ = x✝

Tactic:
by
    simpa [Subtype.coe_inj] using h

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

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

Tactic:
(ht.subset hst).cast_ncard_eq

Goal state after:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ s.encard ≤ t.encard
Module: Mathlib.Data.Set.Card

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

Tactic:
rw [hs.cast_ncard_eq, hs.sdiff.cast_ncard_eq, encard_sdiff_singleton_add_one h]

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Surjective ⇑(rangeKerLift φ)

Tactic:
rintro ⟨_, g, rfl⟩

Goal state after:
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ∃ a, (rangeKerLift φ) a = ⟨φ g, ⋯⟩
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ a, s = {a}

Tactic:
refine ⟨fun h ↦ Or.inr ⟨x, (singleton_subset_iff.mpr hx).antisymm' fun y hy ↦ h hy hx⟩, ?_⟩

Goal state after:
case inr
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ (s = ∅ ∨ ∃ a, s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ insert b (Ioc a (pred b)) = Ioc a b

Tactic:
by
  rw [Ioc_pred_right_of_not_isMin h.not_isMin, Ioo_insert_right h]

Goal state after:
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 d x✝ : M
h : x✝ ∈ Ici (a + d)
⊢ x✝ ∈ (fun x ↦ x + d) '' Ici a

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h)

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ici (a + d)
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ici a
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:
by
  simp only [add_comm a, image_add_const_Ico]

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) = ∑ k ∈ range (n + 1), t (n + 1) (k + 1) + t (n + 1) 0

Tactic:
h_first,

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) ^ (n + 1) = ∑ k ∈ range (n + 1), t (n + 1) (k + 1) + y ^ (n + 1)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ.e_a
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
⊢ ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)

Tactic:
h_first,

Goal state after:
case succ.e_a
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
⊢ ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R✝ : Type u
inst✝¹ : Ring R✝
I✝ J : Ideal R✝
a b : R✝
S : Type v
x y : R✝
R : Type ?u.15
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a b : R ⧸ I), a * b = b * a

Tactic:
rintro ⟨a⟩ ⟨b⟩; exact congr_arg _ (mul_comm a b)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
⊢ comap (lsingle i) (submodule p) = p i

Tactic:
by
  ext x
  refine ⟨fun hx ↦ by simpa using hx i, fun hx j ↦ ?_⟩
  rcases eq_or_ne i j with rfl|h <;> simp_all

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
⊢ q (s ∩ t)

Tactic:
use inter_mem (mem_iInf_of_mem _ hs) ht.1
    intro u hu
    have : u = (u ∪ s) ∩ (u ∪ t) := by
      rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
    rw [this]
    exact ins (mem_of_superset hs subset_union_right) (ht.2 _ subset_union_right)

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ Disjoint (𝓟 s) (𝓟 t) ↔ t ⊆ sᶜ

Tactic:
disjoint_principal_left,

Goal state after:
α : Type u_1
s t : Set α
⊢ sᶜ ∈ 𝓟 t ↔ t ⊆ sᶜ
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ 1 ≤ cof α

Tactic:
rw [Cardinal.one_le_iff_ne_zero, cof_ne_zero_iff]
      use t

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < 0 • b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

pp: case inr.inr
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
· rw [zero_smul] at hab
    exact hab.false.elim

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
S₁ S₂ : Submodule R V
h₁ : Module.Finite R ↥S₁
h₂ : Module.Finite R ↥S₂
⊢ Module.Finite R ↥(S₁ ⊔ S₂)

Tactic:
Finite.iff_fg

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
S₁ S₂ : Submodule R V
h₁ : S₁.FG
h₂ : S₂.FG
⊢ (S₁ ⊔ S₂).FG
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ (PrincipalSeg.ofElement r a).top ∈ fun x ↦ r x b

pp: case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r

pp: case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)

Tactic:
· exact ha

Goal state after:
case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r

case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ StrictMono f ∧ range f = s → Subtype.val ∘ ⇑(enum s hs) = f

Tactic:
· rintro ⟨hf, rfl⟩
    rw [← StrictMono.range_inj H hf]
    simp
    rfl

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ :
  isEquivalent
    { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
      r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
    { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α, r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r,
      wo := ⋯ }
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≃r s

Tactic:
exact (RelIso.preimage Equiv.ulift r).symm.trans <| f.trans (RelIso.preimage Equiv.ulift s)

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

Goal state before:
pp: case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ b ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨a, ⋯⟩

Tactic:
· rw [← enum_typein (α := α) (· < ·) b, ← not_lt, enum_le_enum (r := (· < ·)),
        Subtype.mk_le_mk, ← lt_succ_iff, ha]
      exact typein_lt_type ..

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

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
· rw [mul_add_one, lt_add_iff hb]

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

Goal state before:
pp: case inl
a : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit (a * 0)

pp: case inr
a b : Ordinal.{u_4}
ha : IsSuccLimit a
hb : 0 < b
⊢ IsSuccPrelimit (a * b)

Tactic:
· rw [mul_zero]
    exact isSuccPrelimit_zero

Goal state after:
case inr
a b : Ordinal.{u_4}
ha : IsSuccLimit a
hb : 0 < b
⊢ IsSuccPrelimit (a * b)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : #α ≤ (type s).card
⊢ (#α).ord ≤ type s

Tactic:
· obtain ⟨f⟩ := h
    have g := RelEmbedding.preimage f s
    have := RelEmbedding.isWellOrder g
    exact (ord_le_type _).trans g.ordinal_type_le

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

Goal state before:
pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1

Tactic:
rw [log_lt_iff_lt_pow, Nat.add_lt_add_iff_right, log_lt_iff_lt_pow,
      Nat.pow_add_one, Nat.div_lt_iff_lt_mul]

Goal state after:
case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 0 < b

case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n / b ≠ 0

case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case refine_1
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : log b n < log b (n + 1)
⊢ b ^ log b (n + 1) = n + 1

Tactic:
apply le_antisymm _ (Nat.lt_pow_of_log_lt hb H)
    exact Nat.pow_log_le_self b (Ne.symm (Nat.zero_ne_add_one n))

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

Goal state before:
pp: case zero
a : Ordinal.{u_1}
⊢ a ^ 0 = a ^ 0

Tactic:
opow_zero,

Goal state after:
case zero
a : Ordinal.{u_1}
⊢ 1 = a ^ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
rw [zero_opow hc.ne', zero_opow, mul_zero]

Goal state after:
case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ b + c ≠ 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ clog b n = clog b ((n + b - 1) / b) + 1

Tactic:
apply eq_of_forall_ge_iff
  rintro (_ | c)
  · simp [Nat.ne_of_gt <| clog_pos hb hn]
  · simp only [clog_le_iff_le_pow, Nat.pow_add_one, Nat.add_le_add_iff_right, Nat.zero_lt_of_lt hb,
      div_le_iff_le_mul, hb]
    grind

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

Goal state before:
pp: case inl
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ b ^ log b x ≤ x

pp: case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x

Tactic:
· rw [← one_le_iff_ne_zero] at hx
    obtain rfl | rfl := le_one_iff.1 hb <;> simpa

Goal state after:
case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: o : Ordinal.{u_1}
ho : 0 < o
⊢ ⨆ n, o ^ n = o ^ ω

Tactic:
rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl
  · simpa using apply_omega0_of_isNormal (isNormal_opow ho₁)
  · simp

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

Goal state before:
pp: case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a * a ^ ω ≤ a ^ ω

Tactic:
← opow_one_add,

Goal state after:
case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ (1 + ω) ≤ a ^ ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x ↦ a * x) b ≤ a ^ ω

Tactic:
apply nfp_le_fp (isNormal_mul_right ha).monotone hba
    rw [← opow_one_add, one_add_omega0]

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

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
this : succ a.card ≤ a.card
⊢ False

Tactic:
exact (lt_succ _).not_ge this

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

Goal state before:
pp: case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * a ^ ω * (b / a ^ ω) + a * (b % a ^ ω) = a ^ ω * (b / a ^ ω) + b % a ^ ω
⊢ b % a ^ ω = 0

Tactic:
← opow_one_add,

Goal state after:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a ^ (1 + ω) * (b / a ^ ω) + a * (b % a ^ ω) = a ^ ω * (b / a ^ ω) + b % a ^ ω
⊢ b % a ^ ω = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ c * c = c

Tactic:
induction c using WellFoundedLT.induction with | ind c IH
   =>  _ 

Goal state after:
case ind
c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c * c = c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ω_ 0 = ω

Tactic:
by
  rw [omega_eq_preOmega, add_zero, preOmega_omega0]

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

Goal state before:
pp: case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ 0)

Tactic:
opow_zero,

Goal state after:
case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 1
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a * a ^ ω * c = a ^ ω * c

Tactic:
← opow_one_add,

Goal state after:
case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a ^ (1 + ω) * c = a ^ ω * c