mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case one
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
x : X
hx : x ∈ t
⊢ 1 • x ∈ t

Tactic:
simpa

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

Goal state before:
pp: ι : Type u_7
M : Type u_8
inst✝ : CommMonoid M
s t : Finset ι
f : ι → M
h : s ⊆ t
⊢ s.val ≤ t.val

Tactic:
simpa

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

Goal state before:
pp: case hbc.hab
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (f y)

pp: case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (g y)

Tactic:
· exact comm_gf hx hy h

Goal state after:
case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (g y)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
⊢ ⇑(sInf s) = sInf (@r α '' s)

Tactic:
by
  ext
  simp only [sInf_image, iInf_apply, iInf_Prop_eq]
  rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ ⇑(sInf S) = sInf (DFunLike.coe '' S)

Tactic:
by
  ext
  simp only [sInf_image, iInf_apply, iInf_Prop_eq]
  rfl

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
⊢ ¬Step [] L

Tactic:
by
  generalize h' : [] = L'
  intro h
  rcases h with - | ⟨L₁, L₂⟩
  simp at h'

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝ : CommMonoid M
f : ι → M
h : s₁ ⊆ s₂
hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1
this : DecidableEq ι
⊢ ∀ x ∈ s₂ \ s₁, f x = 1

Tactic:
simpa

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
w✝ x✝ y✝ z✝ : N
h₁ : (c.mapOfSurjective (⇑f) h hf) w✝ x✝
h₂ : (c.mapOfSurjective (⇑f) h hf) y✝ z✝
⊢ (c.mapOfSurjective (⇑f) h hf) (w✝ * y✝) (x✝ * z✝)

Tactic:
rcases h₁ with ⟨a, b, h1, rfl, rfl⟩
    rcases h₂ with ⟨p, q, h2, rfl, rfl⟩
    exact ⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩

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

Goal state before:
pp: α : Type u
a₁ : α
b₁ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: ((a₁, b₁).1, !(a₁, b₁).2) :: L₁) L₂
⊢ False

Tactic:
exact hL₁ L₁ <| .not (L₁ := [])

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

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∀ x ∈ s₁ ∩ s₂, f x = g x

Tactic:
simpa

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∀ x ∈ univ, x ∉ s.toFinset → f x = 1

Tactic:
simpa

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
ι : Type u_3
s : Set ι
hs : s.Finite
P : ι → Submonoid M
hP : ∀ i ∈ s, (P i).FG
⊢ ∀ i ∈ hs.toFinset, (P i).FG

Tactic:
simpa

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
ι : Type u_5
s : Set ι
hs : s.Finite
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ ∀ i ∈ hs.toFinset, (P i).FG

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : NonAssocSemiring α
inst✝² : Preorder α
inst✝¹ : NonAssocSemiring β
inst✝ : Preorder β
f g : α ≃+*o β
h : f.toOrderRingHom = g.toOrderRingHom
⊢ ⇑f = ⇑g

Tactic:
convert! DFunLike.ext'_iff.1 h using 0

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ n, pred^[n] b = a

Tactic:
by convert! exists_succ_iterate_of_le h.ofDual

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a✝ : α
ha : ∃ b, a✝ < b
x✝ : α
⊢ a✝ < x✝ ↔ (if h : ∃ x, a✝ < x then ⋯.min (Ioi a✝) ⋯ else a✝) ≤ x✝

Tactic:
dif_pos ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a✝ : α
ha : ∃ b, a✝ < b
x✝ : α
⊢ a✝ < x✝ ↔ ⋯.min (Ioi a✝) ⋯ ≤ x✝
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
⊢ Iio (succ b) ∩ Ici a = insert b (Iio b ∩ Ici a)

Tactic:
Iio_succ_eq_insert_of_not_isMax h₂,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
⊢ insert b (Iio b) ∩ Ici a = insert b (Iio b ∩ Ici a)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Iio (succ b) ∩ Ioi a = insert b (Iio b ∩ Ioi a)

Tactic:
Iio_succ_eq_insert_of_not_isMax h₂,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ insert b (Iio b) ∩ Ioi a = insert b (Iio b ∩ Ioi a)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
x : α
⊢ x ⩿ x + 1

Tactic:
by
  rw [← succ_eq_add_one]
  exact wcovBy_succ x

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : b ≤ succ a
x : α
this : a < x → b ≤ x
⊢ x ∈ Ioo a b ↔ x ∈ ∅

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ y + ↑0 < x

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < y - ↑0

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
x : α
inst✝³ : LinearOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x < 1 + 1 ↔ x ≤ 1

Tactic:
lt_add_one_iff

Goal state after:
α : Type u_1
x : α
inst✝³ : LinearOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x ≤ 1 ↔ x ≤ 1
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ IsMax a

Tactic:
rw [← succ_eq_iff_isMax]

Goal state after:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ succ a = a
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
hi : i < n
⊢ i < v.toList.length

Tactic:
simpa

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 : α → β
⊢ (image b univ).erase k ⊆ image (fun i ↦ b ↑i) univ

Tactic:
intro i hi

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
⊢ i ∈ image (fun i ↦ b ↑i) univ
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ ∀ x ∈ s \ {i}, f x = ?m.47 x

Tactic:
simpa

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

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b✝ : α
inst✝ : Subsingleton α
n✝ : ℕ
s s' : Sym α (n✝ + 1)
b : α
⊢ s = s'

Tactic:
eq_replicate_of_subsingleton b s',

Goal state after:
case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b✝ : α
inst✝ : Subsingleton α
n✝ : ℕ
s s' : Sym α (n✝ + 1)
b : α
⊢ s = replicate (n✝ + 1) b
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
s' : Sym α n'
⊢ (↑s + ↑s').card = n + n'

Tactic:
by rw [Multiset.card_add, s.2, s'.2]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ countP (fun x ↦ a ≠ x) ↑m + ↑⟨count a ↑m, ⋯⟩ = (↑m).card

Tactic:
add_comm

Goal state after:
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑⟨count a ↑m, ⋯⟩ + countP (fun x ↦ a ≠ x) ↑m = (↑m).card
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ < (↑v).length

Tactic:
simpa

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

Goal state before:
pp: case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ i < (↑v).length

Tactic:
simpa

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

Goal state before:
pp: α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable ↑(t i)
⊢ (⋃ i, t i).Countable

Tactic:
iUnion_eq_range_psigma

Goal state after:
α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable ↑(t i)
⊢ (range fun a ↦ ↑a.snd).Countable
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
⊢ ∀ (a b c : α ⊕ β), Lex r s a b → Lex r s b c → Lex r s a c

Tactic:
by
    rintro _ _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hbc⟩ | ⟨hbc⟩)
    exacts [.inl (_root_.trans hab hbc), .sep _ _, .inr (_root_.trans hab hbc), .sep _ _]

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

Goal state before:
pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝ ≤ ⊥

Tactic:
simp only [elim_inl, elim_inr, lex_inr_inl, false_iff]

Goal state after:
case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ ¬↑a✝ ≤ ⊥
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
h : ∀ (a : α), ¬a ∈ o
⊢ ∀ (a : α), a ∈ o ↔ a ∈ none

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
o : Part α
a : α
h : a ∈ o
f : α → Part β
⊢ o.bind f = f a

Tactic:
eq_some_iff.2 h,

Goal state after:
α : Type u_1
β : Type u_2
o : Part α
a : α
h : a ∈ o
f : α → Part β
⊢ (some a).bind f = f a
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
a : α
⊢ f a ≤ a → ⨆ n, (⇑f)^[n] ⊥ ≤ a

Tactic:
h_a

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
a : α
h_a : f a ≤ a
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ a
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ∀ x ∈ s✝, ¬x ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s✝ → False

Tactic:
intro c₃ hc₃ h₁ h₂

Goal state after:
case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
⊢ False
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ f ((iterateChain (↑f) x h) n) ≤ ωSup (iterateChain (↑f) x h)

Tactic:
← this

Goal state after:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ (iterateChain (↑f) x h) n.succ ≤ ωSup (iterateChain (↑f) x h)
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
⊢ toNat c = n ↔ c = ↑n

Tactic:
rw [← toNat_toENat, ENat.toNat_eq_iff hn, toENat_eq_natCast]

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

Goal state before:
pp: case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x + y).toENatAux = x.toENatAux + y.toENatAux
hle : ¬x ≤ y
⊢ y.toENatAux + x.toENatAux = x.toENatAux + y.toENatAux

Tactic:
add_comm

Goal state after:
case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x + y).toENatAux = x.toENatAux + y.toENatAux
hle : ¬x ≤ y
⊢ x.toENatAux + y.toENatAux = x.toENatAux + y.toENatAux
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a < ℵ₀ ∧ b < ℵ₀

Tactic:
← Ne,

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
s : Set α
a : α
h : a ∉ s
⊢ Disjoint s {a}

Tactic:
simpa

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)

Tactic:
rw [← image_preimage_eq_iff] at h

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : f '' f ⁻¹' s = s
⊢ lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : IsTorsionFree R N
f : M → N
hf : Injective f
smul : ∀ (r : R) (m : M), f (r • m) = r • f m
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ (fun x ↦ r • x) (f m₁) = (fun x ↦ r • x) (f m₂)

Tactic:
simpa [smul] using congr(f $hm)

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
simpa

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

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : NonAssocSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a b : A
h : mulLeft R a = mulLeft R b
⊢ a = b

Tactic:
by simpa using LinearMap.ext_iff.mp h 1

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

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : NonAssocSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b : A
h : mulRight R a = mulRight R b
⊢ a = b

Tactic:
by simpa using LinearMap.ext_iff.mp h 1

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

Goal state before:
pp: case e_4.e_2
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 α
⊢ (fun x_1 ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α

pp: case e_4.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 α
⊢ compHom α (MonoidHom.inr M N) = x

pp: case e_4.e_4
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 α
⊢ ⋯ ≍ snd✝

Tactic:
· funext i; congr; ext m a; clear i; (conv_rhs => rw [← one_smul N a]); rfl

Goal state after:
case e_4.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 α
⊢ compHom α (MonoidHom.inr M N) = x

case e_4.e_4
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 α
⊢ ⋯ ≍ snd✝
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
a : Rˣ
ha : (fun m ↦ m • ↑y) a = ↑x
⊢ ↑((fun m ↦ m • y) a) = ↑x

Tactic:
simpa

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
h : ∀ x ∈ p, f' x ∈ p
x : M
hx : x ∈ p
⊢ (f' ^ 0) x ∈ p

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
S : Submodule R₂ M₂
y : M
hx : f y ∈ S
⊢ ∃ y_1, f y_1 ∈ S ∧ f y_1 = f y

Tactic:
exact ⟨y, hx, rfl⟩

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * ↑u = ↑u * a

Tactic:
· exact congr_arg Units.val <| hu <| Units.mk0 a ha

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
⊢ ↑(⊥.prod ⊥) = ↑⊥

Tactic:
by simp [coe_prod]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p : M
hp : ¬IsUnit p
⊢ Irreducible p ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ p = a * b

Tactic:
by
  simpa [irreducible_iff, hp, and_rotate] using em (∀ a b, p = a * b → IsUnit a ∨ IsUnit b)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b : M
hp : Prime (a * b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
exact (hp.dvd_or_dvd dvd_rfl).symm.imp
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_right <| right_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_right · _)
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_left <| left_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_left · _)

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (List.map List.prod (hd :: tl)).sum

Tactic:
List.map_cons,

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (hd.prod :: List.map List.prod tl).sum
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mp.refine_2
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit x
⊢ Irreducible y

Tactic:
rwa [irreducible_isUnit_mul h'] at h

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inl.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
exact ⟨L, HL', Or.inr <| by rw [List.prod_cons, hhd, neg_one_mul, HP]⟩

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
u : Mˣ
⊢ ¬IsUnit (x * ↑u)

Tactic:
simpa

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
⊢ ∅ • N = ⊥

Tactic:
by
  ext
  fconstructor
  · intro hx
    rw [mem_set_smul_def, Submodule.mem_sInf] at hx
    exact hx ⊥ (fun r _ hr ↦ hr.elim)
  · rintro rfl; exact Submodule.zero_mem _

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : IsModularLattice α
a b c : α
inst✝² : BoundedOrder α
inst✝¹ : ComplementedLattice α
inst✝ : Fact (a ≤ b)
x✝ : ↑(Icc a b)
x : α
ha : a ≤ x
hb : x ≤ b
⊢ ∃ b_1, IsCompl ⟨x, ⋯⟩ b_1

Tactic:
simp_rw [Set.Icc.isCompl_iff]
    obtain ⟨y, rfl, rfl⟩ := exists_inf_eq_and_sup_eq ha hb
    exact ⟨⟨y, inf_le_right, le_sup_right⟩, rfl, rfl⟩

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
⊢ ∃ b, IsCompl ⟨x, hx⟩ b

Tactic:
simp_rw [Set.Iic.isCompl_iff]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
⊢ ∃ b, Disjoint x ↑b ∧ x ⊔ ↑b = a
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t : Set α
a✝ b : α
s : Set α
a : α
ha : a ∈ s
⊢ ↑{a} ⊆ s ∧ {a}.sup' ⋯ id = a

Tactic:
simpa

Goal state after: