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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent R (-v)

Tactic:
intro f g h
  simp only [Finsupp.linearCombination_apply, Pi.neg_apply, smul_neg, Finsupp.sum_neg, neg_inj] at h
  ext m
  exact DFunLike.congr_fun (hv h) m

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

Goal state before:
pp: ι : 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 : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0
t : Finset ↑s
g : ↑s → R
h0 : ∑ i ∈ t, g i • v ↑i = 0
i : ↑s
hit : i ∈ t
⊢ ∀ (i : ι) (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0

Tactic:
simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

Tactic:
by_cases H : j = i

Goal state after:
case pos
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

case neg
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : ¬j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (↑s).ncard = s.card

Tactic:
rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

Tactic:
by_cases H : j = i

Goal state after:
case pos
η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

case neg
η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : ¬j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ s.ncard = univ.ncard

Tactic:
himage

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ (f' '' univ).ncard = univ.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
⊢ a₁ = a₂

Tactic:
set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩
  have hsurj : f'.Surjective := by
    rintro ⟨y, hy⟩
    obtain ⟨a, ha, rfl⟩ := hsurj y hy
    simp only [Subtype.exists]
    exact ⟨_, ha, rfl⟩
  have := hs.fintype
  have := Fintype.ofSurjective _ hsurj
  set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
  exact
    @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
      (fun a ha ↦ by { rw [mem_toFinset] at ha ⊢; exact hf a ha }) (by simpa)
      (by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }) a₁
      (by simpa) a₂ (by simpa) (by simpa)

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i

Tactic:
refine i.cases ?_ ?_

Goal state after:
case refine_1
α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) 0 = vecCons (x • y) (x • v) 0

case refine_2
α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (x • vecCons y v) i.succ = vecCons (x • y) (x • v) i.succ
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i

Tactic:
refine i.cases ?_ ?_

Goal state after:
case refine_1
α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v + w) 0 = vecCons (x + vecHead w) (v + vecTail w) 0

case refine_2
α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (vecCons x v + w) i.succ = vecCons (x + vecHead w) (v + vecTail w) i.succ
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i

Tactic:
refine i.cases ?_ ?_

Goal state after:
case refine_1
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) 0 = vecCons (vecHead v + y) (vecTail v + w) 0

case refine_2
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (v + vecCons y w) i.succ = vecCons (vecHead v + y) (vecTail v + w) i.succ
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i

Tactic:
refine i.cases ?_ ?_

Goal state after:
case refine_1
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) 0 = vecCons (x - vecHead w) (v - vecTail w) 0

case refine_2
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (vecCons x v - w) i.succ = vecCons (x - vecHead w) (v - vecTail w) i.succ
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i

Tactic:
refine i.cases ?_ ?_

Goal state after:
case refine_1
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) 0 = vecCons (vecHead v - y) (vecTail v - w) 0

case refine_2
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (v - vecCons y w) i.succ = vecCons (vecHead v - y) (vecTail v - w) i.succ
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) i = vecCons (-x) (-v) i

Tactic:
refine i.cases ?_ ?_

Goal state after:
case refine_1
α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) 0 = vecCons (-x) (-v) 0

case refine_2
α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (-vecCons x v) i.succ = vecCons (-x) (-v) i.succ
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 1 ↔ ∃ a, s = {a}

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨a, rfl⟩; rw [ncard_singleton]⟩
  have hft := (finite_of_ncard_ne_zero (ne_zero_of_eq_one h)).fintype
  simp_rw [ncard_eq_toFinset_card', @Finset.card_eq_one _ (toFinset s)] at h
  refine h.imp fun a ha ↦ ?_
  simp_rw [Set.ext_iff, mem_singleton_iff]
  simp only [Finset.ext_iff, mem_toFinset, Finset.mem_singleton] at ha
  exact ha

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
ι : Sort u_5
f : ι → RingCon R
⊢ ⇑(iInf f) = ⨅ i, ⇑(f i)

Tactic:
rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
⊢ Nontrivial c.Quotient ↔ c ≠ ⊤

Tactic:
by
  simp [← not_subsingleton_iff_nontrivial]

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
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ comap (p.liftQ f h) q ≤ map p.mkQ (comap f q)

Tactic:
rintro ⟨x⟩ hx; exact ⟨_, hx, 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
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ (p.mapQ q f h).ker = map p.mkQ (comap f q)

Tactic:
by
  simp [Submodule.mapQ, Submodule.ker_liftQ, LinearMap.ker_comp]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v
h₁ : 0 ∘ₛₗ f = 0
⊢ f.range = ⊤

Tactic:
rw [← Submodule.ker_mkQ (range f), ← h 0 (range f).mkQ (Eq.trans h₁ (range_mkQ_comp _).symm)]

Goal state after:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v
h₁ : 0 ∘ₛₗ f = 0
⊢ ker 0 = ⊤
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) (Ico a b) = Ico (a + c) (b + c)

Tactic:
by
  rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
  exact Set.image_add_const_Ico _ _ _

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ f a * ∏ x < a, f x = ∏ x ≤ a, f x

Tactic:
Iic_eq_cons_Iio,

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ f a * ∏ x < a, f x = ∏ x ∈ cons a (Iio a) ⋯, f x
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:
refine lt_of_le_of_ne ?_ (h _)

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^[n + 1] i ≤ j
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ toZ i0 (succ^[n] i0) ≤ ↑n

Tactic:
by
  rw [toZ_of_ge (le_succ_iterate _ _)]
  norm_cast
  exact Nat.find_min' _ rfl

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
have h_nonneg : 0 ≤ toZ hι.some i := toZ_nonneg hi
      simp_rw [if_pos h_nonneg]
      exact iterate_succ_toZ i hi

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

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

Tactic:
by
  rw [span_pair_comm, span_pair_add_right, span_pair_comm]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
have ⟨M, hM, le⟩ := exists_le_maximal I hI

Goal state after:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i
⊢ (∏ k ∈ range (n + 1), f (k + 1) (n + 1 - (k + 1)) ^ (n + 1).choose (k + 1)) * f 0 (n + 1 - 0) ^ (n + 1).choose 0 =
    (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i

Tactic:
simpa [choose_succ_succ, pow_add, prod_mul_distrib, A, mul_assoc] using mul_comm _ _

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

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ x ^ ((t.attach.sup fun x ↦ n ⟨↑x, ⋯⟩) - n ⟨x, ⋯⟩) * x ^ n ⟨x, ⋯⟩ ∈ ↑(span (range fun x ↦ ↑x ^ n x))

Tactic:
exact mul_mem_left _ _ (subset_span ⟨_, rfl⟩)

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

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
⊢ span (range fun x ↦ ↑x ^ n x) = ⊤

Tactic:
by
  have ⟨t, hts, mem⟩ := Submodule.mem_span_finite_of_mem_span ((eq_top_iff_one _).mp hs)
  refine top_unique ((span_pow_eq_top _ ((eq_top_iff_one _).mpr mem) <|
    t.attach.sup fun x ↦ n ⟨x, hts x.2⟩).ge.trans <| span_le.mpr ?_)
  rintro _ ⟨x, hxt, rfl⟩
  rw [← Nat.sub_add_cancel (Finset.le_sup <| t.mem_attach ⟨x, hxt⟩)]
  simp_rw [pow_add]
  exact mul_mem_left _ _ (subset_span ⟨_, rfl⟩)

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

Goal state before:
pp: α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≥ x2) ((fun s ↦ 𝓟 ↑s) ⟨U, U_in⟩) ((fun s ↦ 𝓟 ↑s) z) ∧
      (fun x1 x2 ↦ x1 ≥ x2) ((fun s ↦ 𝓟 ↑s) ⟨V, V_in⟩) ((fun s ↦ 𝓟 ↑s) z)

Tactic:
use ⟨W, W_in⟩

Goal state after:
case h
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ (fun x1 x2 ↦ x1 ≥ x2) ((fun s ↦ 𝓟 ↑s) ⟨U, U_in⟩) ((fun s ↦ 𝓟 ↑s) ⟨W, W_in⟩) ∧
    (fun x1 x2 ↦ x1 ≥ x2) ((fun s ↦ 𝓟 ↑s) ⟨V, V_in⟩) ((fun s ↦ 𝓟 ↑s) ⟨W, W_in⟩)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ generate h.filterBasis.sets = generate {U | ∃ i, p i ∧ s i = U}

Tactic:
IsBasis.filterBasis

Goal state after:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ generate { sets := {t | ∃ i, p i ∧ s i = t}, nonempty := ⋯, inter_sets := ⋯ }.sets = generate {U | ∃ i, p i ∧ s i = U}
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ s ∈ comap f l ↔ (f '' sᶜ)ᶜ ∈ l

Tactic:
by
  simp only [mem_comap'', kernImage_eq_compl]

Goal state after:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a

Tactic:
by
    simpa only [exists_prop, Finite.mem_toFinset] using
      h1.toFinset.exists_max_image f ⟨x, h1.mem_toFinset.2 hx⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
⊢ a • b₁ ≤ a • b₂

Tactic:
obtain ha | ha := ha.eq_or_lt
    · simp [← ha]
    · exact h₀ _ ha _ _ h

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulStrictMono α γ
_a : α
ha : 0 < _a
_b₁ _b₂ : β × γ
h₁ : _b₁.1 ≤ _b₂.1
h₂ : _b₁.2 < _b₂.2
⊢ (_a • _b₁).1 < (_a • _b₂).1 ∧ (_a • _b₁).2 ≤ (_a • _b₂).2 ∨ (_a • _b₁).1 ≤ (_a • _b₂).1 ∧ (_a • _b₁).2 < (_a • _b₂).2

Tactic:
· exact .inr ⟨smul_le_smul_of_nonneg_left h₁ ha.le, smul_lt_smul_of_pos_left h₂ ha⟩

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
a : α
⊢ IsNormal fun x ↦ ⟨f ↑x, ⋯⟩

Tactic:
isNormal_iff

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
a : α
⊢ (StrictMono fun x ↦ ⟨f ↑x, ⋯⟩) ∧
    ∀ (o : ↑(Iio a)), IsSuccLimit o → ∀ (a_2 : ↑(Iio (f a))), (∀ b < o, ⟨f ↑b, ⋯⟩ ≤ a_2) → ⟨f ↑o, ⋯⟩ ≤ a_2
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f ((enum r) ⟨type t, ⋯⟩) = (enum s) ⟨type t, ⋯⟩

Tactic:
rw [enum_type g, enum_type (g.transRelIso f)]

Goal state after:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f g.top = (g.transRelIso f).top
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ a < b + c ↔ ∃ d < c, a < b + d

Tactic:
lt_add_iff hc.ne_bot

Goal state after:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a ≤ b + d) ↔ ∃ d < c, a < b + d
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
isNormal_iff

Goal state after:
a : Ordinal.{u_4}
⊢ (StrictMono fun x ↦ a + x) ∧
    ∀ (o : Ordinal.{u_4}), IsSuccLimit o → ∀ (a_2 : Ordinal.{u_4}), (∀ b < o, a + b ≤ a_2) → a + o ≤ a_2
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
← not_notMem

Goal state after:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ ¬x ∉ s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub f ∨ succ (iSup f) = lsub f

Tactic:
by
  rcases eq_or_lt_of_le (iSup_le_lsub f) with h | h
  · exact Or.inl h
  · exact Or.inr ((succ_le_of_lt h).antisymm (lsub_le_succ_iSup f))

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

Goal state before:
pp: b : ℕ
hb : b ≤ 1
n : ℕ
⊢ log b n = 0

Tactic:
by
  rw [log, if_pos hb]

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

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

Tactic:
· exact (isSuccLimit_mul_left ha hb).isSuccPrelimit

Goal state after:
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) / (a * 0) = b / 0

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

Tactic:
· rw [mul_zero, div_zero, div_zero]

Goal state after:
case inr
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
⊢ (a * b + c) / (a * d) = b / d
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) ≤ b / d

Tactic:
rw [← lt_succ_iff, ← lt_mul_iff_div_lt H, mul_assoc]
      · grw [hc, ← mul_succ]
        gcongr
        rw [succ_le_iff]
        exact lt_mul_succ_div b hd

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

Goal state before:
pp: a b : Ordinal.{u_4}
H : b ∣ a
⊢ a % b = 0

Tactic:
by
  rcases H with ⟨c, rfl⟩
  rcases eq_or_ne b 0 with (rfl | hb)
  · simp
  · simp [mod_def, hb]

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

Goal state before:
pp: case inr
a b c : Ordinal.{u_1}
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c

Tactic:
exact (opow_le_opow_iff_right h₁).2 h₂

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

Goal state before:
pp: case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ sSup (if 1 ∈ Iic x then univ else ∅) = 0

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
⊢ clog b n = clog b (n + 1) ↔ b ^ clog b n ≠ n

Tactic:
by
  rw [ne_eq, ← clog_lt_clog_succ_iff hb, not_lt]
  simp only [le_antisymm_iff, and_iff_right_iff_imp]
  exact fun _ ↦ clog_monotone b (le_add_right n 1)

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

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

Tactic:
simpa using apply_omega0_of_isNormal (isNormal_opow ho₁)

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

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

pp: case inr
ho : 0 < 1
⊢ ⨆ n, 1 ^ n = 1 ^ ω

Tactic:
· simpa using apply_omega0_of_isNormal (isNormal_opow ho₁)

Goal state after:
case inr
ho : 0 < 1
⊢ ⨆ n, 1 ^ n = 1 ^ ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ IsNormal ⇑preOmega

Tactic:
isNormal_iff

Goal state after:
⊢ StrictMono ⇑preOmega ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Ordinal.{u_1}), (∀ b < o, preOmega b ≤ a) → preOmega o ≤ a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 + x2) a b < o

Tactic:
← h a hao

Goal state after:
case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 + x2) a b < a + o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preAleph (ω + (o + 1)) = ℵ_ (o + 1)

Tactic:
aleph_eq_preAleph

Goal state after:
o : Ordinal.{u_1}
⊢ preAleph (ω + (o + 1)) = preAleph (ω + (o + 1))
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ < ℵ_ o ↔ 0 < o

Tactic:
by
  rw [← aleph_zero, aleph_lt_aleph]

Goal state after: