mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ (∏ i, f ↑i) * ∏ i, f ↑i = ∏ i, f i

Tactic:
← Finset.prod_subtype s,

Goal state after:
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ (∏ a ∈ s, f a) * ∏ i, f ↑i = ∏ i, f i

case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
a : G
h : a ∈ Group.conjugatesOfSet base
⊢ a ∈ base

Tactic:
Group.mem_conjugatesOfSet_iff,

Goal state after:
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
a : G
h : ∃ a_1 ∈ base, IsConj a_1 a
⊢ a ∈ base
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ⁅H, K⁆ ≤ K
h : G
hh : h ∈ H
k : G
hk : k ∈ K
⊢ h * k * h⁻¹ ∈ K

Tactic:
· exact (mul_mem_cancel_right <| inv_mem hk).mp <| hH <| commutator_mem_commutator hh hk

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

Goal state before:
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 ⟨x, eq⟩ := h.surj m
      use x.1 / x.2
      rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
inst✝ : IsCancelMul M
⊢ ∀ (r : N), IsRightRegular r

Tactic:
intro n

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
inst✝ : IsCancelMul M
n : N
⊢ IsRightRegular n
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ < ↑(x * a✝)

Tactic:
bot_lt_coe

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ < ↑(a✝ * x)

Tactic:
bot_lt_coe

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
rw [mul_bot x0'] at h
      exact absurd h bot_le.not_gt

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : α
hab : ↑a ≤ ⊥
⊢ (↑a).succ ≤ ⊥.succ

Tactic:
by simp at hab

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : α
hab : ⊤ ≤ ↑a
⊢ ⊤.pred ≤ (↑a).pred

Tactic:
by simp at hab

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
⊢ IsLUB (Iio a) a

Tactic:
refine ⟨fun _ ↦ le_of_lt, fun b hb ↦ le_of_forall_lt fun c hc ↦ ?_⟩

Goal state after:
α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
⊢ c < b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
⊢ limitRecOn b isMin succ isSuccLimit = isSuccLimit b hb fun x x_1 ↦ limitRecOn x isMin succ isSuccLimit

Tactic:
by
  rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_neg hb.not_isMin]; rfl

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∀ (a_1 : ℕ), succ^[a_1] (EquivLike.inv f a) = EquivLike.inv f b → succ^[a_1] a = b

Tactic:
intro n

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ succ^[n] (EquivLike.inv f a) = EquivLike.inv f b → succ^[n] a = b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∀ (a_1 : ℕ), pred^[a_1] (EquivLike.inv f b) = EquivLike.inv f a → pred^[a_1] b = a

Tactic:
intro n

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ pred^[n] (EquivLike.inv f b) = EquivLike.inv f a → pred^[n] b = a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n + 1] (succ^[n + 1] i) = i

Tactic:
Function.iterate_succ,

Goal state after:
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ (pred^[n] ∘ pred) (succ^[n + 1] i) = i
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
h : ⊤ < ↑a✝
⊢ (match ⊤ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ (match ↑a✝ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝¹

Tactic:
· exact (not_top_lt h).elim

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ (match ↑a✝ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝¹
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst✝² : Preorder X
inst✝¹ : Preorder Y
inst✝ : SuccOrder X
f : X ≃o Y
y : Y
⊢ y ≤ f (succ (f.symm y))

Tactic:
by rw [← map_inv_le_iff f]; exact le_succ (f.symm y)

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

Goal state before:
pp: n : ℕ
⊢ ↑n < ↑(n + 1)

Tactic:
natCast_lt_natCast

Goal state after:
n : ℕ
⊢ n < n + 1
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
⊢ (if h : pred ↑⟨x, hx⟩ ∈ s then ⟨pred ↑⟨x, hx⟩, h⟩ else ⟨x, hx⟩) ≤ ⟨x, hx⟩

Tactic:
by dsimp; split <;> simp_all [Order.pred_le]

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

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
i j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
h : i ≠ j
⊢ (insert j s).piecewise f g i = s.piecewise f g i

Tactic:
simp [piecewise, h]

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

Goal state before:
pp: case bot
m : ℕ
⊢ ⊥ < ↑↑(m + 1) ↔ ⊥ ≤ ↑m

Tactic:
simp only [bot_le, WithBot.bot_lt_coe]

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ l.length - 1 = n - 1

Tactic:
p

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ n - 1 = n - 1
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ ↑i < l.length

Tactic:
p

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ ↑i < n
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : (fun {α} ↦ η.app α) = fun {α} ↦ η'.app α
⊢ η = η'

Tactic:
cases η
  cases η'
  congr

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
⊢ i ∈ image (fun i ↦ b ↑i) univ

Tactic:
rw [mem_image]

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
i : β
hi : i ∈ (image b univ).erase k
⊢ ∃ a ∈ univ, b ↑a = i
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
⊢ ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x

Tactic:
apply prod_congr rfl
  intro j hj
  have : j ≠ i := by
    rintro rfl
    exact h hj
  simp [this]

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i

Tactic:
have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))

Goal state after:
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (∏ j, if h : j = i then f j h else 1) = f i ⋯

Tactic:
by
  rw [Finset.prod_dite_eq', if_pos (mem_univ _)]

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
⊢ C v w

Tactic:
by
  induction n with
  | zero =>
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
    cases v_property
    rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
    cases w_property
    apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩
    apply ih

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

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ (count b ↑m + if a = b then count a ↑m else 0) = count b ↑m

Tactic:
if_neg h,

Goal state after:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ count b ↑m + 0 = count b ↑m
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: ι : Type u
a : Cardinal.{v}
f : ι → Cardinal.{v}
⊢ lift.{u, v} a ^ sum f = prod fun i ↦ a ^ f i

Tactic:
induction a using Cardinal.inductionOn with

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r (f.toRelEmbedding f.top) f.top
⊢ False

Tactic:
rw [show f f.top = f.top from InitialSeg.eq f (InitialSeg.refl r) f.top] at h

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r f.top f.top
⊢ False
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂

Tactic:
intro n

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
n : ℕ
⊢ ∀ (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ {a, b} ∈ Set.range fun c ↦ Set.range ⇑c

Tactic:
use pair a b hab; exact range_pair a b hab

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

Goal state before:
pp: a : Cardinal.{u}
⊢ a < 2 ^ a

Tactic:
induction a using Cardinal.inductionOn with

Goal state after:
case mk
α : Type u
⊢ #α < 2 ^ #α
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ sum f

Tactic:
rw [← Quotient.out_eq (f i)]

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} ⟦Quotient.out (f i)⟧ ≤ sum f
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ∀ (i : ℕ), ((iterateChain (↑f) x h).map ↑f) i ≤ ωSup (iterateChain (↑f) x h)

Tactic:
intro n

Goal state after:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ ((iterateChain (↑f) x h).map ↑f) n ≤ ωSup (iterateChain (↑f) x h)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
⊢ ∀ (i : ℕ), (iterateChain (↑f) x h) i ≤ a

Tactic:
intro n

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
⊢ (iterateChain (↑f) x h) n ≤ a
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ ∀ (c_1 : ℕ), c_1 ≤ toNat c ↔ c_1 ≤ toNat d

Tactic:
rw [← cast_toNat_of_lt_aleph0 (not_le.mp hc), ← cast_toNat_of_lt_aleph0 (not_le.mp hd)] at h

Goal state after:
case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ ↑(toNat c) ↔ ↑n ≤ ↑(toNat d)
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ ∀ (c_1 : ℕ), c_1 ≤ toNat c ↔ c_1 ≤ toNat d
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
κ : φ.CompTriple ψ χ
⊢ ⇑(ψ.comp φ) = ⇑χ

Tactic:
κ.comp_eq

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
κ : φ.CompTriple ψ χ
⊢ ⇑χ = ⇑χ
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (range (g ∘ f))

Tactic:
rw [range_comp]

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (g '' range f)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
⊢ lift.{max u v, max u v} (sum f) ≤ lift.{v, u} #ι * ⨆ i, lift.{u, v} (f i)

Tactic:
lift_sum,

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
⊢ (sum fun i ↦ lift.{max u v, v} (f i)) ≤ lift.{v, u} #ι * ⨆ i, lift.{u, v} (f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ lift.{u, v} #↑t ≤ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
rw [image_eq_range] at h
  convert! mk_preimage_of_subset_range_lift _ _ h using 1
  rw [mk_sep]
  rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ (x✝² • x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by ext <;> exact smul_assoc ..

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

Goal state before:
pp: G : Type u_1
R : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Monoid R
inst✝³ : AddGroup R
inst✝² : DistribMulAction G R
inst✝¹ : IsScalarTower G R R
inst✝ : SMulCommClass G R R
r : G
a : R
⊢ IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)

Tactic:
by
  rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]

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

Goal state before:
pp: R : Type u_14
M : Type u_15
M₂ : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R M₂
F : Type u_17
inst✝¹ : FunLike F M M₂
inst✝ : LinearMapClass F R M M₂
f : F
r : R
x : M
⊢ f (r • x) = r • f x

Tactic:
map_smul

Goal state after:
R : Type u_14
M : Type u_15
M₂ : Type u_16
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R M₂
F : Type u_17
inst✝¹ : FunLike F M M₂
inst✝ : LinearMapClass F R M M₂
f : F
r : R
x : M
⊢ r • f x = r • f x
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 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✝
fₗ✝ : M →ₗ[R✝] M₂
f g : M →ₛₗ[σ] M₃
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S M₂
fₗ : M →ₗ[S] M₂
c : R
x : M
⊢ fₗ ((c • 1) • x) = (c • 1) • fₗ x

Tactic:
map_smul

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
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✝
fₗ✝ : M →ₗ[R✝] M₂
f g : M →ₛₗ[σ] M₃
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S M₂
fₗ : M →ₗ[S] M₂
c : R
x : M
⊢ (c • 1) • fₗ x = (c • 1) • fₗ x
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 S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
⊢ M₂ →ₛₗ[σ'] M

Tactic:
dsimp [LeftInverse, Function.RightInverse] at h₁ h₂
  exact
    { toFun := g
      map_add' := fun x y ↦ by rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]; simp [h₂]
      map_smul' := fun a b ↦ by
        rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)]
        simp [h₂] }

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

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝¹ : (i : I) → g i
x✝ : I
⊢ (0 • x✝¹) x✝ = 0 x✝

Tactic:
rw [zero_smul]

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

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ (ψ ∘ φ) m • g (f x) = χ m • g (f x)

Tactic:
κ.comp_eq

Goal state after:
M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ χ m • g (f x) = χ m • g (f x)
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₂✝

Tactic:
exact Subsingleton.elim ..

Goal state after:
Module: Mathlib.Algebra.Ring.Pi

Goal state before:
pp: I : Type u
f : I → Type u_1
inst✝ : (i : I) → Semiring (f i)
i : I
x : f i
⊢ (i : I) → f i

Tactic:
by classical exact (if h : · = i then h ▸ x else 0)

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ p.toAddSubgroup = ⊤ ↔ p = ⊤

Tactic:
by simp [← toAddSubgroup_inj]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
h : -x ∈ p
⊢ - -x ∈ p

Tactic:
exact neg_mem _ h

Goal state after:
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:
by rw [ker, eq_bot_iff, map_le_iff_le_comap]

Goal state after: