mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.Finite
ha : a ∈ s
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ s) b

Tactic:
by
  lift s to Finset α using hs; exact s.exists_le_maximal ha

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ (Finset.Ico a b).val ∪ (Finset.Ico b c).val = (Finset.Ico a c).val

Tactic:
← Finset.union_val,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ (Finset.Ico a b ∪ Finset.Ico b c).val = (Finset.Ico a c).val
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : {x | P x}.Finite
⊢ False

Tactic:
obtain ⟨m, hP, hm⟩ := hf.exists_maximal ⟨seed, hs⟩

Goal state after:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : {x | P x}.Finite
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ ⦃y : ℕ⦄, (fun x ↦ x ∈ {x | P x}) y → m ≤ y → y ≤ m
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Icc a b ⊆ Iic b

Tactic:
simpa [← coe_subset] using Set.Icc_subset_Iic_self

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) ⋯

Tactic:
classical rw [cons_eq_insert, Ioo_insert_left h]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ Injective orbit

Tactic:
intro x y h

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
h : x.orbit = y.orbit
⊢ x = y
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m < g 0 + n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ False

Tactic:
· rw [← Nat.sub_lt_iff_lt_add' (le_of_not_gt hm)] at mn
      apply hf1.2 _ _ (g.lt_iff_lt.2 mn)
      rw [← List.cons_head!_tail (hnil (g (m - g 0))), ← List.cons_head!_tail (hnil (g n'))]
      exact List.SublistForall₂.cons (hg _ _ (le_of_lt mn)) hmn

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ g ∈ orbit (ConjAct G) h ↔ IsConj h g

Tactic:
isConj_iff,

Goal state after:
G : Type u_3
inst✝ : Group G
g h : G
⊢ g ∈ orbit (ConjAct G) h ↔ ∃ c, c * h * c⁻¹ = g
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
⊢ map f (centralizer s) ≤ centralizer (⇑f '' s)

Tactic:
by
  rintro - ⟨g, hg, rfl⟩ - ⟨h, hh, rfl⟩
  rw [← map_mul, ← map_mul, hg h hh]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
⊢ {y | toLex (a, y) ∈ s}.IsPWO

Tactic:
by
  let f : α ×ₗ β → β := fun x => (ofLex x).2
  have h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a}) := by
    ext x
    simp [f]
  rw [h]
  apply IsPWO.image_of_monotoneOn (hαβ.mono inter_subset_left)
  rintro b ⟨-, hb⟩ c ⟨-, hc⟩ hbc
  simp only [mem_preimage, mem_singleton_iff] at hb hc
  have : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c :=
    Prod.Lex.toLex_le_toLex.mp hbc
  simp_all only [lt_self_iff_false, true_and, false_or]

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Hom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
h : SemiconjBy a x y
f : F
⊢ SemiconjBy (f a) (f x) (f y)

Tactic:
simpa only [SemiconjBy, map_mul] using congr_arg f h

Goal state after:
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : r x y
⊢ (comap Quotient.mk' s) x y

Tactic:
rw [comap_rel, Quotient.eq'.2 h]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_4
f : ι → Con M
⊢ sInf (DFunLike.coe '' Set.range f) = ⨅ i, ⇑(f i)

Tactic:
← Set.range_comp,

Goal state after:
M : Type u_1
inst✝ : Mul M
ι : Sort u_4
f : ι → Con M
⊢ sInf (Set.range (DFunLike.coe ∘ f)) = ⨅ i, ⇑(f i)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
h : Red LL₁ LL₂
⊢ Red L₁ L₂

Tactic:
induction h using Relation.ReflTransGen.head_induction_on generalizing L₁ L₂ with

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:

Tactic:
_ = ∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i) :=
        prod_congr rfl fun y _ ↦ prod_congr rfl fun x hx ↦ by rw [(mem_filter.1 hx).2]
    _ = _ := prod_fiberwise_of_maps_to h _

Goal state after:
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, y * ↑a = x) ↔ ∃ a, x⁻¹ * y = ↑a⁻¹

Tactic:
simp only [inv_mul_eq_iff_eq_mul, Subgroup.coe_inv, eq_mul_inv_iff_mul_eq]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
ih : ∀ z ∈ {x | x ∈ P ∧ x ≠ 1}, z ≤ y ∧ ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
hy₁ : y ∈ P
hy₂ : y ≠ 1
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

Tactic:
simp only [Set.mem_ofPred_eq, and_imp] at ih

Goal state after:
case neg
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih : ∀ z ∈ P, z ≠ 1 → z ≤ y → ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ f (f.sec (f x)).1 = f (↑(f.sec (f x)).2 * x)

Tactic:
by rw [sec_spec', map_mul]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ (∃ c, ↑b₂ * a₁ = ↑a₂ * b₁) ↔ ↑b₂ * a₁ = ↑a₂ * b₁

Tactic:
exists_const

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

Goal state before:
pp: case refine_1
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
g g' : G
eq : f g = f g'
⊢ g = g'

pp: case refine_2
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
m : M
⊢ ∃ a, f a = m

Tactic:
· have ⟨c, eq⟩ := h.exists_of_eq eq
      exact mul_left_cancel eq

Goal state after:
case refine_2
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
m : M
⊢ ∃ a, f a = m
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ⊥ * ↑x ≤ b * ↑x

Tactic:
simp_rw [bot_mul x0', bot_le]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ IsMax (succ^[n] a)

Tactic:
refine max_of_succ_le (le_trans ?_ h_eq.symm.le)

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ (succ^[n] a) ≤ succ^[m] a
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : ¬IsMax x
⊢ x + 1 ≤ y ↔ x < y

Tactic:
by
  rw [← succ_eq_add_one, succ_le_iff_of_not_isMax hx]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ StrictAnti f

Tactic:
simpa using strictAntiOn_of_succ_lt Set.ordConnected_univ (by simpa using hf)

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

Goal state before:
pp: case succ.zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
ha : pred^[0 + 1] b ∈ s
⊢ f (pred^[0 + 1] b) < f b

Tactic:
simpa using hf _ hab hb ha

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∉ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
simp_all only [not_false_eq_true, forall_const, one_mul]

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : f i = 1
hs : i ∉ s
⊢ ∏ x ∈ s, f x = ∏ x ∈ s \ {i}, f x
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.succ
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
rw [← cons_head_tail v, scanl_cons, get_cons_succ]
    refine Fin.cases ?_ ?_ i
    · simp
    · intro i'
      simp only [hn, Fin.castSucc_succ, get_cons_succ]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (List.Vector α n) = Fintype.card α ^ n

Tactic:
rw [Fintype.ofEquiv_card]

Goal state after:
α : Type u_1
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (Fin n → α) = Fintype.card α ^ n
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
f : α → β
inst✝ : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ Countable α

Tactic:
simp_rw [← Set.countable_univ_iff, ← Set.preimage_univ (f := f), ← Set.iUnion_of_singleton,
    Set.preimage_iUnion, Set.countable_iUnion h]

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
⊢ ∀ {a b : { x_1 // r x_1 x } ⊕ { x_1 // ¬r x_1 x }},
    r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) a) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) b) ↔
      Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) a b

Tactic:
rintro (⟨a, ha⟩ | ⟨a, ha⟩) (⟨b, hb⟩ | ⟨b, hb⟩)
    · simp
    · simpa using trans_trichotomous_right ha hb
    · simpa using fun h ↦ ha <| trans h hb
    · simp

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inl_lt_inl_iff.2 h)
        · exact ⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩
        · exact (not_inl_lt_inr ha).elim

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ f.top = g.top

Tactic:
rw [Subsingleton.elim f (PrincipalSeg.relIsoTrans e g)]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (relIsoTrans e g).top = g.top
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
⊢ x ≤ y ∨ y ≤ x

Tactic:
rcases Part.eq_none_or_eq_some x with (h | ⟨b, h₀⟩)

Goal state after:
case inl
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ x ≤ y ∨ y ≤ x

case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ x ≤ y ∨ y ≤ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ h

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
map_ωSup'✝¹ :
  ∀ (c : Chain α),
    { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun (ωSup c) =
      ωSup (c.map { toFun := toFun✝¹, monotone' := monotone'✝¹ })
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_ωSup'✝ :
  ∀ (c : Chain α),
    { toFun := toFun✝, monotone' := monotone'✝ }.toFun (ωSup c) =
      ωSup (c.map { toFun := toFun✝, monotone' := monotone'✝ })
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, monotone' := monotone'✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_ωSup' := map_ωSup'✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, map_ωSup' := map_ωSup'✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, map_ωSup' := map_ωSup'✝ }
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: ⊢ StrictMonoOn (⇑toNat) (Iio ℵ₀)

Tactic:
by
  simp only [← range_natCast, StrictMonoOn, forall_mem_range, toNat_natCast, Nat.cast_lt]
  exact fun _ _ ↦ id

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

Goal state before:
pp: case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ lift.{max u v, v} #(Quotient.out (f none)) * lift.{v, max u v} #((a : α) → Quotient.out (f (some a))) =
    lift.{u, v} (∏ i, f i)

Tactic:
lift_umax.{v, u},

Goal state after:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ lift.{u, v} #(Quotient.out (f none)) * lift.{v, max u v} #((a : α) → Quotient.out (f (some a))) =
    lift.{u, v} (∏ i, f i)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
⊢ IsSMulRegular R g

Tactic:
intro x y h

Goal state after:
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ x = y
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ lift.{0, u} #α = lift.{u, 0} #(Fin n) ↔ Nonempty (α ≃ Fin n)

Tactic:
lift_mk_eq'

Goal state after:
α : Type u
n : ℕ
⊢ Nonempty (α ≃ Fin n) ↔ Nonempty (α ≃ Fin n)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 0 • a < ℵ₀ ↔ 0 = 0 ∨ a < ℵ₀

Tactic:
simpa using aleph0_pos

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

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m * ↑n < ℵ₀

Tactic:
rw [← Nat.cast_mul]

Goal state after:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m * n) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ Infinite α ↔ ¬Finite α

Tactic:
not_finite_iff_infinite

Goal state after:
α : Type u
⊢ Infinite α ↔ Infinite α
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
⊢ f 0 = 0

Tactic:
← zero_smul R (0 : M),

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
⊢ f (0 • 0) = 0
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₂ N₂
inst✝² : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : Subsingleton M
f : M →ₛₗ[σ₁₂] M₂
x : M
⊢ f x = default x

Tactic:
rw [Subsingleton.elim x 0, map_zero, map_zero]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Opposite

Goal state before:
pp: case inl
M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
h✝ : Subsingleton α
⊢ m₁✝ = m₂✝

pp: case inr
M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
h✝ : Nontrivial α
⊢ m₁✝ = m₂✝

Tactic:
· exact Subsingleton.elim ..

Goal state after:
case inr
M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
h✝ : Nontrivial α
⊢ m₁✝ = m₂✝
Module: Mathlib.Algebra.Regular.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : Mul R
a : R
⊢ IsRegular (op a) ↔ IsRegular a

Tactic:
by
  simp [isRegular_iff, and_comm]

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

Goal state before:
pp: case e_3
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a

Tactic:
conv_rhs => rw [← one_smul N a]

Goal state after:
case e_3
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (1 • a)
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4.e_2.e_4.e_4.e_4.e_5
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a

Tactic:
conv_rhs => rw [← one_smul N a]

Goal state after:
case e_4.e_2.e_4.e_4.e_4.e_5
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (1 • a)
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ p ≤ f.ker ↔ map f p = ⊥

Tactic:
ker,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ p ≤ comap f ⊥ ↔ map f p = ⊥
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), f c ∈ p
⊢ (codRestrict p f hf).ker = f.ker

Tactic:
ker,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), f c ∈ p
⊢ comap (codRestrict p f hf) ⊥ = f.ker
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : m → M
i : m
⊢ (funLeft R M _root_.id) x i = x i

Tactic:
LinearMap.funLeft_id

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : m → M
i : m
⊢ x i = x i
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : n → M
i : n
⊢ (funLeft R M _root_.id) x i = x i

Tactic:
LinearMap.funLeft_id

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : n → M
i : n
⊢ x i = x i