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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
⊢ ∀ (snd : ↥t ⧸ s.subgroupOf t),
    (fun a ↦ (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a))
        ((fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) (Quotient.mk'' a, snd)) =
      (Quotient.mk'' a, snd)

Tactic:
refine Quotient.ind' fun b => ?_

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
⊢ (fun a ↦ (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a))
      ((fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) (Quotient.mk'' a, Quotient.mk'' b)) =
    (Quotient.mk'' a, Quotient.mk'' b)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ Odd sᶜ.ncard ↔ Odd s.ncard

Tactic:
rw [← Nat.not_even_iff_odd, even_ncard_compl_iff heven, Nat.not_even_iff_odd]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type u_5
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
r : R
⊢ (↑↑(f.prodMap g.toRingHom)).toFun ((algebraMap R (A × C)) r) = (algebraMap R (B × D)) r

Tactic:
by simp [commutes]

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
hs : s.Finite
⊢ s.ncard = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
refine ⟨eq_insert_of_ncard_eq_succ, ?_⟩
  rintro ⟨a, t, hat, h, rfl⟩
  rw [← h, ncard_insert_of_notMem hat (hs.subset ((subset_insert a t).trans_eq h))]

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

Goal state before:
pp: case of
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x y : N
h : rel x y
a b : M
fa : f a = x
fb : f b = y
⊢ rel x (f b)

Tactic:
fb

Goal state after:
case of
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x y : N
h : rel x y
a b : M
fa : f a = x
fb : f b = y
⊢ rel x y
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y ↦ rel (f x) (f y)) (f.symm w * f.symm y) b

Tactic:
fb

Goal state after:
case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y ↦ rel (f x) (f y)) (f.symm w * f.symm y) (f.symm x * f.symm z)
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
⊢ x ∈ MonoidHom.mrange (c.lift f H) → x ∈ MonoidHom.mrange f

Tactic:
by rintro ⟨⟨y⟩, hy⟩; exact ⟨y, hy⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case fst
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (((inl R M M₂).coprod (inr R M M₂)) x✝).1 = (id x✝).1

Tactic:
simp only [Prod.mk_add_mk, add_zero, id_apply, coprod_apply, inl_apply, inr_apply, zero_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case snd
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (((inl R M M₂).coprod (inr R M M₂)) x✝).2 = (id x✝).2

Tactic:
simp only [Prod.mk_add_mk, add_zero, id_apply, coprod_apply, inl_apply, inr_apply, zero_add]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (pred a) b = Ico a b

Tactic:
by
  ext x; rw [mem_Ioo, mem_Ico, pred_lt_iff_of_not_isMin ha]

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
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x

Tactic:
by
  rw [Ioc_eq_cons_Ioo h, prod_cons]

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

Goal state before:
pp: n : ℕ
xy : ℕ × ℕ
⊢ xy ∈ { val := Multiset.Nat.antidiagonal n, nodup := ⋯ } ↔ xy.1 + xy.2 = n

Tactic:
by
    rw [mem_def, Multiset.Nat.mem_antidiagonal]

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
⊢ (1 + 1) • (a * b * a) = 0

Tactic:
have : a * (a * b + b * a) * a = 0 := by rw [hab, mul_zero, zero_mul]

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
this : a * (a * b + b * a) * a = 0
⊢ (1 + 1) • (a * b * a) = 0
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ∃ x_1, (∃ y ∈ I, ∃ z, x ∣ z ∧ y + z = x_1) ∧ x_1 ∈ S
hy : ∃ x, (∃ y_1 ∈ I, ∃ z, y ∣ z ∧ y_1 + z = x) ∧ x ∈ S
⊢ False

Tactic:
obtain ⟨s₁, ⟨i₁, hi₁, ⟨_, ⟨r₁, rfl⟩, hr₁⟩⟩, hs₁⟩ := hx

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hy : ∃ x, (∃ y_1 ∈ I, ∃ z, y ∣ z ∧ y_1 + z = x) ∧ x ∈ S
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
⊢ False
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ span ((fun x ↦ x ^ 0) '' ∅)

pp: case zero.inr
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
x : α
hx : x ∈ s
⊢ 1 ∈ span ((fun x ↦ x ^ 0) '' s)

Tactic:
· rw [Set.image_empty, hs]
      trivial

Goal state after:
case zero.inr
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
x : α
hx : x ∈ s
⊢ 1 ∈ span ((fun x ↦ x ^ 0) '' s)
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
⊢ ⋯.filter = l

Tactic:
by
  ext U
  simp [h.mem_iff, IsBasis.mem_filter_iff]

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
⊢ p s

Tactic:
let q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ t', t ⊆ t' → p t'

Goal state after:
α : 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'
⊢ p s
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
⊢ ⋂ i, Iic (f i) = ∅ ↔ ¬BddBelow (range f)

Tactic:
simp [not_bddBelow_iff, Set.eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap (ψ ∘ φ) f ≤ f

Tactic:
eq,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap id f ≤ f
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ g ≤ map (φ ∘ ψ) g

Tactic:
eq,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ g ≤ map id g
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
⊢ (fun g ↦ g a) '' s ∈ f.seq (pure a)

pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ s.seq t ∈ map (fun g ↦ g a) f

Tactic:
· rw [← seq_singleton]
    exact seq_mem_seq hs singleton_mem_pure

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ s.seq t ∈ map (fun g ↦ g a) f
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ b ≤ (k * b + (k - 1)) / k

Tactic:
rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, Nat.add_zero]

Goal state after:
k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ k - 1 < k
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case mp
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

Tactic:
rintro ⟨S, Sfin, hS⟩

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
S : Set M
Sfin : S.Finite
hS : span R S = N
⊢ ∃ n s, span R (range s) = N
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ Module.Finite R≥0 R

Tactic:
simp_rw [Module.finite_def, Submodule.fg_def, Submodule.eq_top_iff']

Goal state after:
R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ ∃ S, S.Finite ∧ ∀ (x : R), x ∈ Submodule.span R≥0 S
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ ¬succ (sSup (f ⁻¹' Iic x)) ≤ sSup (f ⁻¹' Iic x)

Tactic:
not_le,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ sSup (f ⁻¹' Iic x) < succ (sSup (f ⁻¹' Iic x))
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
h0 : 0 < o
a : o.ToType
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨0, ⋯⟩ ≤ a

Tactic:
rw [← not_lt]

Goal state after:
o : Ordinal.{u_1}
h0 : 0 < o
a : o.ToType
⊢ ¬a < (enum fun x1 x2 ↦ x1 < x2) ⟨0, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub f ↔ ∀ a < lsub f, succ a < lsub f

Tactic:
by
  refine ⟨fun h => ?_, fun hf => le_antisymm (iSup_le_lsub f) (lsub_le fun i => ?_)⟩
  · rw [← h]
    exact fun a => succ_lt_iSup_of_ne_iSup fun i => (lsub_le_iff.1 (le_of_eq h.symm) i).ne
  by_contra! hle
  have heq := (succ_iSup_eq_lsub_iff f).2 ⟨i, le_antisymm (Ordinal.le_iSup _ _) hle⟩
  have :=
    hf _
      (by
        rw [← heq]
        exact lt_succ (iSup f))
  rw [heq] at this
  exact this.false

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

Goal state before:
pp: o : Ordinal.{u_3}
⊢ iSup ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding = o

Tactic:
by
  rw [← csSup_Iic (a := o), iSup, PrincipalSeg.range_eq]
  congr
  simp

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

Goal state before:
pp: case cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
m : List α
o : Ordinal.{u}
hm : m.SortedGT
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
hmltl : Lex (fun x1 x2 ↦ x1 < x2) m (a :: as)
⊢ ∀ i ∈ m, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
cases m with

Goal state after:
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)

Goal state after:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : log b n < log b (n + 1)
⊢ b ^ log b (n + 1) ≤ n + 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ u * b ≤ b ^ x

Tactic:
rw [← opow_succ]

Goal state after:
b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ succ u ≤ b ^ x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ 0 ∈ (fun x ↦ b ^ x) ⁻¹' Iic x

Tactic:
by simpa [one_le_iff_ne_zero]

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

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ f i (derivFamily f o) = derivFamily f o

Tactic:
derivFamily_limit _ l,

Goal state after:
case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ f i (⨆ b, derivFamily f ↑b) = ⨆ b, derivFamily f ↑b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case add_one.inl
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : a ≤ derivFamily f o
⊢ ∃ o, derivFamily f o = a

Tactic:
exact IH h

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

Goal state before:
pp: case limit.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a < derivFamily f o
⊢ ∃ o, derivFamily f o = a

Tactic:
derivFamily_limit _ l,

Goal state after:
case limit.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
h : a < ⨆ b, derivFamily f ↑b
⊢ ∃ o, derivFamily f o = a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ i, fixedPoints f

Tactic:
exact (Set.iInter_const _).symm

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∃ o, deriv f o = a

Tactic:
by
  unfold deriv
  rw [← le_iff_derivFamily fun _ : Unit => H]
  exact ⟨fun h _ => h, fun h => h Unit.unit⟩

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

Goal state before:
pp: case e'_3
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ i, fixedPoints f

Tactic:
exact (Set.iInter_const _).symm

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

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

Tactic:
exact (isNormal_mul_right ha).strictMono hbo

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

Goal state before:
pp: case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
⊢ a * b < ω ^ c

Tactic:
rcases ((isNormal_opow one_lt_omega0).lt_iff_exists_lt l).1 ha with ⟨x, hx, ax⟩
    refine (mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt ?_
    rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega0]
    exact l.succ_lt hx

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

Goal state before:
pp: case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ 0
⊢ a * ω ^ ω ^ 0 = ω ^ ω ^ 0

Tactic:
rw [opow_zero, opow_one] at h ⊢
    exact mul_omega0 a0 h

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

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

Tactic:
rw [← not_lt]

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

Goal state before:
pp: n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m ≤ 1

Tactic:
rw [← not_lt]

Goal state after:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ¬1 < m
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
rw [← not_lt]

Goal state after:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ ¬b < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ b ≤ a

Tactic:
rw [← not_lt]

Goal state after:
case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ¬a < b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ c + ⨆ i, f i = ⨆ i, c + f i

Tactic:
by
  rw [add_comm, Cardinal.ciSup_add f hf]; simp_rw [add_comm]

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

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : ¬α ≤ β
⊢ ¬α + γ ≤ β + γ

Tactic:
not_le,

Goal state after:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β < α
⊢ β + γ < α + γ
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card

Tactic:
exact cof_blsub_le_lift f

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

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

Tactic:
by
  rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨c, rfl⟩ | hb)
  · contradiction
  · rw [succ_eq_add_one, ← add_assoc, cof_add_one, cof_add_one]
  · exact cof_map_of_isNormal (isNormal_add_right a) hb

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

Goal state before:
pp: case h1
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ lift.{u, u} #α = lift.{u, u} #β

Tactic:
lift_inj

Goal state after:
case h1
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ #α = #β
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case h2
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ lift.{u, u} #↑s = lift.{u, u} #↑t

Tactic:
lift_inj

Goal state after:
case h2
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ #↑s = #↑t
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
⊢ (⟨i, a⟩ ∈ (↑s).toFinset.attach.val.bind fun i ↦ Multiset.map (Sigma.mk ↑i) ↑(fs i)) ∨ (f ⟨i, a⟩.fst) ⟨i, a⟩.snd = 0

Tactic:
cases s.prop i with
          | inl hi =>
            cases (fs ⟨i, Multiset.mem_toFinset.mpr hi⟩).prop a with
            | inl ha =>
              left; rw [Multiset.mem_bind]
              use ⟨i, Multiset.mem_toFinset.mpr hi⟩
              constructor
              case right => simp [ha]
              case left => apply Multiset.mem_attach
            | inr ha => right; simp [toFun_eq_coe (f i) ▸ ha]
          | inr hi => right; simp [toFun_eq_coe f ▸ hi]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ↑(span R s).dualAnnihilator = {f | s ⊆ ↑f.ker}

Tactic:
ext f
  simp only [SetLike.mem_coe, mem_dualAnnihilator, Set.mem_ofPred_eq, ← LinearMap.mem_ker]
  exact span_le

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep p
⊢ Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)

Tactic:
by
  rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)] at h
  exact h.dfinsupp_lsum_injective

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
r₁ r₂ : R
m₁ m₂ : M
inst✝ : Mul M
hm : Commute m₁ m₂
hr : Commute r₁ r₂
⊢ Commute (single m₁ r₁) (single m₂ r₂)

Tactic:
by simp [Commute, SemiconjBy, hm.eq, hr.eq]

Goal state after: