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

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝ : (i : ι) → CommGroup (A i)
n : ℕ
φ : ((i : ι) → A i) →* (i : ι) → A i ⧸ (powMonoidHom n).range :=
  { toFun := fun x x_1 ↦ ↑(x x_1), map_one' := ⋯, map_mul' := ⋯ }
y : (i : ι) → A i ⧸ (powMonoidHom n).range
⊢ (φ fun i ↦ Quotient.out (y i)) = y

Tactic:
by simp [φ]

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ x * y * z = z

Tactic:
rw [hxy, one_mul]

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

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

Tactic:
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Icc a b = Set.Icc (c + a) (c + b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

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

Tactic:
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Icc a b = Set.Icc (a + c) (b + c)
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:
rw [Iic_eq_cons_Iio, prod_cons]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ partialSups (disjointed f) = partialSups f

Tactic:
suffices ∀ r i (hi : #(Iio i) ≤ r), partialSups (disjointed f) i = partialSups f i from
    OrderHom.ext _ _ (funext fun i ↦ this _ i le_rfl)
  intro r i hi
  induction r generalizing i with
  | zero =>
    -- Base case: `n` is minimal, so `partialSups f i = partialSups (disjointed f) n = f i`.
    simp only [Nat.le_zero, card_eq_zero] at hi
    simp only [partialSups_apply, Iic_eq_cons_Iio, hi, disjointed_apply, sup'_eq_sup, sup_cons,
      sup_empty, sdiff_bot]
  | succ n ih =>
    -- Induction step: first WLOG arrange that `#(Iio i) = r + 1`
    rcases lt_or_eq_of_le hi with hn | hn
    · exact ih _ <| Nat.le_of_lt_succ hn
    simp only [partialSups_apply (disjointed f), Iic_eq_cons_Iio, sup'_eq_sup, sup_cons]
    -- Key claim: we can write `Iio i` as a union of (finitely many) `Iic` intervals.
    have hun : (Iio i).biUnion Iic = Iio i := by
      ext r; simpa using ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
    -- Use claim and `sup_biUnion` to rewrite the supremum in the definition of `disjointed f`
    -- in terms of suprema over `Iic`'s. Then the RHS is a `sup` over `partialSups`, which we
    -- can rewrite via the induction hypothesis.
    rw [← hun, sup_biUnion, sup_congr rfl (g := partialSups f)]
    · simp only [funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion, hun]
      simp only [disjointed, sdiff_sup_self, Iic_eq_cons_Iio, sup_cons]
    · simp only [partialSups, sup'_eq_sup, OrderHom.coe_mk] at ih ⊢
      refine fun x hx ↦ ih x ?_
      -- Remains to show `∀ x in Iio i, #(Iio x) ≤ r`.
      rw [← Nat.lt_add_one_iff, ← hn]
      apply lt_of_lt_of_le (b := #(Iic x))
      · simpa only [Iic_eq_cons_Iio, card_cons] using Nat.lt_succ_self _
      · refine card_le_card (fun r hr ↦ ?_)
        simp only [mem_Iic, mem_Iio] at hx hr ⊢
        exact hr.trans_lt hx

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
⊢ univ.sup (disjointed f) = univ.sup f

Tactic:
have hun : univ.biUnion Iic = (univ : Finset ι) := by
    ext r; simpa only [mem_biUnion, mem_univ, mem_Iic, true_and, iff_true] using ⟨r, le_rfl⟩
  rw [← hun, sup_biUnion, sup_biUnion, sup_congr rfl (fun i _ ↦ ?_)]
  rw [← sup'_eq_sup nonempty_Iic, ← sup'_eq_sup nonempty_Iic,
    ← partialSups_apply, ← partialSups_apply, partialSups_disjointed]

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

Goal state before:
pp: n : ℕ
⊢ map (Prod.map id Nat.succ) (antidiagonal (n + 1)) ++ [(n + 1 + 1, 0)] =
    (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]

Tactic:
antidiagonal_succ

Goal state after:
n : ℕ
⊢ map (Prod.map id Nat.succ) ((0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)) ++ [(n + 1 + 1, 0)] =
    (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ (i, n - i).2 + (i, n - i).1 = n

Tactic:
Nat.sub_add_cancel

Goal state after:
n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ n = n

n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ i ≤ n
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : 1 - b * a ∈ I
abc : c = 1 - b * a
⊢ b * a - 1 ∈ I

Tactic:
← neg_mem_iff (G := R) (H := I),

Goal state after:
case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : -(1 - b * a) ∈ I
abc : c = 1 - b * a
⊢ b * a - 1 ∈ I
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
⊢ l.HasBasis (fun i ↦ p i ∧ q i) s

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i, hpi, hti⟩ => h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩
  rcases h.mem_iff.1 ht with ⟨i, hpi, hti⟩
  rcases hq i hpi with ⟨j, hpj, hqj, hji⟩
  exact ⟨j, ⟨hpj, hqj⟩, hji.trans hti⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ comap f ⊤

Tactic:
comap_top

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ ⊤
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: ι : Sort u
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
has_least_elem : ⨅ i, f i ∈ range f
⊢ ⋃ i, Ici (f i) = Ici (⨅ i, f i)

Tactic:
simp only [← IsGLB.biUnion_Ici_eq_Ici (@isGLB_iInf _ _ _ f) has_least_elem, mem_range,
    iUnion_exists, iUnion_iUnion_eq']

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

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

Tactic:
union_subset_iff,

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ ((∃ i, p i ∧ s i ⊆ t) ∧ ∃ i, p' i ∧ s' i ⊆ t) ↔ ∃ a b, (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x✝ : Set α
⊢ x✝ ∈ l ↔ ∃ i, p i ∧ x✝ ∈ 𝓟 (s i)

Tactic:
by simp only [h.mem_iff, mem_principal]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) ⊆ upperBounds (range f)

Tactic:
rintro c hc _ ⟨b, rfl⟩

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
⊢ f b ≤ c
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
⊢ C S

Tactic:
by
  have : Finite S := Finite.to_subtype h
  have : Finite {T : Set α // T ⊆ S} := Finite.of_equiv (Set S) (Equiv.Set.powerset S).symm
  rw [← Subtype.coe_mk (p := (· ⊆ S)) _ le_rfl]
  rw [← Subtype.coe_mk (p := (· ⊆ S)) _ hS0] at H0
  refine Finite.to_wellFoundedGT.wf.induction_bot' (fun s hs hs' ↦ ?_) H0
  obtain ⟨a, ⟨ha1, ha2⟩, ha'⟩ := H1 s (ssubset_of_ne_of_subset hs s.2) hs'
  exact ⟨⟨insert a s.1, insert_subset ha1 s.2⟩, Set.ssubset_insert ha2, ha'⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
⊢ _a₁ ≤ _a₂

Tactic:
by
    rcases lt_iff.mp hb with ⟨h₁, -⟩ | ⟨-, h₁⟩
    · exact le_of_smul_le_smul_right h.1 h₁
    · exact le_of_smul_le_smul_right h.2 h₁

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

Goal state before:
pp: A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
this : IsScalarTower A₁ A₂ B₁
e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Module.Finite A₂ B₂

Tactic:
have := of_restrictScalars_finite A₁ A₂ B₁

Goal state after:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝² : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝¹ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
this✝ : IsScalarTower A₁ A₂ B₁
e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : Module.Finite A₂ B₁
⊢ Module.Finite A₂ B₂
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ sSup (Iic x) ≤ x

Tactic:
rw [csSup_Iic]

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

Goal state before:
pp: b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < univ.{u, v}

Tactic:
univ,

Goal state after:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < lift.{v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
simpa using (lt_add_iff_of_isSuccLimit hb).not

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

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ IsSuccLimit (a - b)

Tactic:
rw [isSuccLimit_iff, Ordinal.sub_ne_zero_iff_lt, isSuccPrelimit_iff_succ_lt]

Goal state after:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ b < a ∧ ∀ a_1 < a - b, succ a_1 < a - b
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a b : Ordinal.{v}
⊢ lift.{u, v} a < lift.{u, v} b ↔ a < b

Tactic:
by
  simp_rw [lt_iff_le_not_ge, lift_le]

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : IsSuccLimit c
⊢ a < b * c ↔ ∃ c' < c, a < b * c'

Tactic:
simpa using (mul_le_iff_of_isSuccLimit h).not

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

Goal state before:
pp: b n fuel : ℕ
hb : 1 < b
hn : n ≠ 0
hfuel : n < b ^ fuel
⊢ (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)

Tactic:
induction fuel generalizing b with

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

Goal state before:
pp: a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ ∀ ⦃a_1 : Ordinal.{u_1}⦄, (∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x.ord ≤ a_1) → a.ord ≤ a_1

Tactic:
ord_le

Goal state after:
a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ ∀ ⦃a_1 : Ordinal.{u_1}⦄, (∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x ≤ a_1.card) → a ≤ a_1.card
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n < o.card ↔ ↑n < o

Tactic:
rw [← natCast_add_one_le_iff, ← succ_le_iff, ← Nat.cast_add_one, nat_le_card]

Goal state after:
o : Ordinal.{u_1}
n : ℕ
⊢ ↑(n + 1) ≤ o ↔ succ ↑n ≤ o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case limit
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ 1 ^ b ≤ c ↔ 1 ≤ c

Tactic:
rw [opow_le_of_isSuccLimit one_ne_zero l]

Goal state after:
case limit
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ (∀ b' < b, 1 ^ b' ≤ c) ↔ 1 ≤ c
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
this : Small.{u, u + 1} Ordinal.{u}
⊢ False

Tactic:
exact not_small_ordinal this

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

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

Tactic:
rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one]

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

Goal state before:
pp: n b fuel : ℕ
hn : 1 < n
hb : 1 < b
hfuel : n < b ^ fuel
⊢ (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧ b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)

Tactic:
induction fuel generalizing b with

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

Tactic:
← one_le_iff_ne_zero

Goal state after:
case inl
b x : Ordinal.{u_1}
hx : 1 ≤ x
hb : b ≤ 1
⊢ b ^ log b x ≤ x
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case zero
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
⊢ (op a)^[0] a < o

Tactic:
rwa [Function.iterate_zero]

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

Goal state before:
pp: case mp
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (∃ c, (∃ c_1 < b, ∃ n, c < ω ^ c_1 * ↑n) ∧ ∃ n, a < ω ^ c * ↑n) → ∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)

Tactic:
intro ⟨a, ⟨b, hb, ⟨m, hm⟩⟩, ⟨n, hn⟩⟩

Goal state after:
case mp
a✝ b✝ : Ordinal.{u_1}
hb✝ : b✝ ≠ 0
a b : Ordinal.{u_1}
hb : b < b✝
m : ℕ
hm : a < ω ^ b * ↑m
n : ℕ
hn : a✝ < ω ^ a * ↑n
⊢ ∃ c < b✝, ∃ n, a✝ < ω ^ (ω ^ c * ↑n)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ nfp 0 a = a

Tactic:
rw [← iSup_iterate_eq_nfp]
  apply (Ordinal.iSup_le ?_).antisymm (Ordinal.le_iSup _ 0)
  intro n
  cases n
  · rfl
  · rw [Function.iterate_succ']
    simp

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

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : b ≠ 0
⊢ nfp (fun x ↦ a * x) 1 ≤ b

Tactic:
← one_le_iff_ne_zero

Goal state after:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : 1 ≤ b
⊢ nfp (fun x ↦ a * x) 1 ≤ b
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
ord_le

Goal state after:
a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
this : succ a.card ≤ a.card
⊢ False
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun x1 x2 ↦ x1 + x2) c d < a * x + a * y

Tactic:
exact Left.add_lt_add hx' hy'

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
⊢ ∃ t ⊆ s, IsCofinal t ∧ typeLT ↑t = (Order.cof α).ord

Tactic:
obtain ⟨t, ht, ht'⟩ := exists_ord_cof_eq s

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
t : Set ↑s
ht : IsCofinal t
ht' : typeLT ↑t = (Order.cof ↑s).ord
⊢ ∃ t ⊆ s, IsCofinal t ∧ typeLT ↑t = (Order.cof α).ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ a = 0

Tactic:
rw [mul_zero] at h

Goal state after:
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : 0 = a
⊢ a = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ a = 0

Tactic:
rw [mul_zero] at h

Goal state after:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : 0 = a
⊢ a = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a

Tactic:
· rintro (⟨h1, h2⟩ | h3)
    · rw [add_eq_max h1, max_eq_left h2]
    · rw [h3, add_zero]

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

Goal state before:
pp: case inl
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c

Tactic:
add_eq_right hb this.le,

Goal state after:
case inl
a b c : Cardinal.{u_1}
h : b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
⊢ (⨆ i, f i + 1).cof ≤ #α

Tactic:
by
  simpa using cof_lift_iSup_add_one_le f

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
⊢ (succ c).IsRegular

Tactic:
use hc₀

Goal state after:
case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
⊢ succ c ≤ (succ c).ord.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ⊢ univ.{u, v}.cof = Cardinal.univ.{u, v}

Tactic:
univ,

Goal state after:
⊢ (lift.{v, u + 1} (typeLT Ordinal.{u})).cof = Cardinal.univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
⊢ ∃ a, #↑(f ⁻¹' {a}) = #β

Tactic:
have : ∃ a, #β ≤ #(f ⁻¹' {a}) := by
    by_contra! h
    apply mk_univ.not_lt
    rw [← preimage_univ, ← iUnion_of_singleton, preimage_iUnion]
    exact
      mk_iUnion_le_sum_mk.trans_lt <| (sum_le_mk_mul_iSup _).trans_lt <|
        mul_lt_of_lt h₁ (h₂.trans_le <| cof_ord_le _) (iSup_lt_of_lt_cof_ord h₂ h)

Goal state after:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
this : ∃ a, #β ≤ #↑(f ⁻¹' {a})
⊢ ∃ a, #↑(f ⁻¹' {a}) = #β
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
⊢ #(α ≃ β) = 0 ↔ #α ≠ #β

Tactic:
mk_equiv_eq_zero_iff_lift_ne,

Goal state after:
α β : Type u
⊢ lift.{u, u} #α ≠ lift.{u, u} #β ↔ #α ≠ #β
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
j : ι
H : i = j
⊢ (f + single i b) j = (single i b + f) j

pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
j : ι
H : ¬i = j
⊢ (f + single i b) j = (single i b + f) j

Tactic:
· subst H
        simp [h1]

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
j : ι
H : ¬i = j
⊢ (f + single i b) j = (single i b + f) j
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
j' : α i
hj : j' ≠ j
⊢ (single ⟨i, j⟩ x) ⟨i, j'⟩ = (single j x) j'

Tactic:
· rw [single_eq_of_ne, single_eq_of_ne hj]
      simpa using hj

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x ↦ ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b
⊢ finHRecOn (fun x ↦ ⟦a x⟧) f h = f a

Tactic:
refine eq_of_heq ((eqRec_heq _ _).trans ?_)

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x ↦ ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b
⊢ Quotient.hrecOn (finChoice fun x ↦ ⟦a x⟧) f h ≍ f a
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (evalEquiv R M).symm g
⊢ f m = g f

Tactic:
← (evalEquiv R M).apply_symm_apply g,

Goal state after:
R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (evalEquiv R M).symm g
⊢ f m = ((evalEquiv R M) ((evalEquiv R M).symm g)) f
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i i' : ι
h : i ≠ i'
⊢ lapply i ∘ₗ lsingle i' = 0

Tactic:
ext; simp [h.symm]

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

Goal state before:
pp: R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Multiset R
t : Multiset M
⊢ s.sum • t.sum = (map (fun p ↦ p.1 • p.2) (s ×ˢ t)).sum

Tactic:
induction s using Multiset.induction with

Goal state after: