mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * ((-↑m.succ + ↑(m + 1) * ↑n) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))

Tactic:
← mul_one ((m + 1 : ℕ) : ℤ)

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * ((-(↑(m + 1) * 1) + ↑(m + 1) * ↑n) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ a ∈ tl

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).dedup.sup = s₁.sup ⊔ s₂.sup

Tactic:
dedup_ext.2,

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (dedup ?m.26).sup = s₁.sup ⊔ s₂.sup

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ ?m.26

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).dedup.sup = s₁.sup ⊔ s₂.sup

Tactic:
dedup_ext.2,

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (dedup ?m.26).sup = s₁.sup ⊔ s₂.sup

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ ?m.26

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).dedup.sup = a ⊔ s.sup

Tactic:
dedup_ext.2,

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (dedup ?m.23).sup = a ⊔ s.sup

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ ?m.23

α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ Multiset α
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑s
⊢ toFunAux x = #({y ∈ range ↑x | y ∈ s})

Tactic:
by
  rw [toFunAux, List.countP_eq_length_filter]
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ x ∈ l

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ a ∉ ⋃ x ∈ t, f x

Tactic:
mem_iUnion₂

Goal state after:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i, ∃ (_ : i ∈ t), a ∈ f i
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
b : β
hb : b ∉ s
⊢ (cons b s hb).sup' ⋯ f = f b ⊔ s.sup' H f

Tactic:
rw [← WithBot.coe_eq_coe]
  simp [WithBot.coe_sup]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
inst✝ : DecidableEq β
b : β
⊢ (insert b s).sup' ⋯ f = f b ⊔ s.sup' H f

Tactic:
rw [← WithBot.coe_eq_coe]
  simp [WithBot.coe_sup]

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
f g : ι → α
hdf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
hdg : Directed (fun x1 x2 ↦ x1 ≤ x2) g
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
⊢ iSup f ≤ iSup g

Tactic:
by
  cases isEmpty_or_nonempty ι
  · rw [iSup_of_empty', iSup_of_empty']
  · exact hdf.ciSup_le fun x ↦ hdg.le_ciSup_of_le B x (H x)

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h✝ : i ∈ s
⊢ i ∈ s

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
h✝ : i ∉ s
⊢ ∃ a ∈ s, sSup ∅ ≤ f a

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ ⨅ i ∈ s, f i = (image f s).min' h'

Tactic:
by
  rw [← OrderDual.toDual_inj, toDual_min', toDual_iInf]
  simp only [toDual_iInf]
  rw [ciSup_eq_max'_image _ h]
  simp only [image_image]
  congr

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ioi ↑a = some '' Ioi a ∪ {⊤}

Tactic:
by
  ext x; induction x <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ici ↑a = some '' Ici a ∪ {⊤}

Tactic:
by
  ext x; induction x <;> simp

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : ∀ ⦃c : (i : ι) → α i⦄, a ≤ c → ∀ (x : ι), a x < c x → c ≤ b → ∀ (x : ι), ¬c x < b x
hab : a ≤ b
i : ι
hi : a i < b i
j : ι
hj : j ≠ i
c : (i : ι) → α i := Function.update a i (b i)
⊢ c ≤ b

Tactic:
simpa [update_le_iff, c] using fun k hk ↦ hab k

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
⊢ (∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)) → a ⩿ b

Tactic:
rintro ⟨i, hab, h⟩

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
⊢ a ⩿ b
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: ⊢ sInf ∅ = 0

Tactic:
sInf_eq_zero

Goal state after:
⊢ 0 ∈ ∅ ∨ ∅ = ∅
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ s = ∅

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = k + 1

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
exact ⟨g, Or.intro_right _ hnr⟩

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

Goal state before:
pp: case zero
⊢ image (fun j ↦ 0 - 1 - j) (range 0) = range 0

Tactic:
rw [range_zero, image_empty]

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

Goal state before:
pp: a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

Tactic:
simp_rw [Finset.range_eq_Ico, map_eq_image]
  convert! (Ico_union_Ico_eq_Ico a.zero_le (a.le_add_right b)).symm
  ext x
  simp only [Ico_zero_eq_range, mem_image, mem_range, addLeftEmbedding_apply, mem_Ico]
  constructor
  · lia
  · rintro h
    exact ⟨x - a, by lia⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_1
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ ∅, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)

Tactic:
intro f
    exists RelEmbedding.refl (· ≤ ·)
    simp only [IsEmpty.forall_iff, imp_true_iff, Finset.notMem_empty]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r r' : α → α → Prop
s t : Set α
h : t.WellFoundedOn r'
hle : r ≤ r'
hst : s ⊆ t
⊢ s.WellFoundedOn r

Tactic:
wellFoundedOn_iff

Goal state after:
α : Type u_2
r r' : α → α → Prop
s t : Set α
h : WellFounded fun a b ↦ r' a b ∧ a ∈ t ∧ b ∈ t
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFounded fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Icc ↑a ↑b
⊢ p x

Tactic:
rw [mem_Icc] at hx

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a ≤ x ∧ x ≤ ↑b
⊢ p x
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case inr
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
hs : s.Nonempty
⊢ s.Finite ↔ BddBelow s ∧ BddAbove s

Tactic:
exact ⟨fun h ↦ ⟨⟨h.toFinset.inf' ((Finite.toFinset_nonempty h).mpr hs) id,
    fun x hx ↦ Finset.inf'_le id ((Finite.mem_toFinset h).mpr hx)⟩,
    ⟨h.toFinset.sup' ((Finite.toFinset_nonempty h).mpr hs) id, fun x hx ↦ Finset.le_sup' id
    ((Finite.mem_toFinset h).mpr hx)⟩⟩,
    fun ⟨h₀, h₁⟩ ↦ BddBelow.finite_of_bddAbove h₀ h₁⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Injective (uIcc a)

Tactic:
by
  simpa only [uIcc_comm] using uIcc_injective_right a

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f }

Tactic:
exact ⟨(minBadSeqOfBadSeq r rk s 0 f0 hf0).1, (minBadSeqOfBadSeq r rk s 0 f0 hf0).2.2⟩

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g k : G
⊢ g * k = k * g ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Tactic:
rw [eq_comm]

Goal state after:
G : Type u_3
inst✝ : Group G
g k : G
⊢ k * g = g * k ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: case h₁
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ r 1 1

Tactic:
assumption

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

Goal state before:
pp: case h₂
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)

Tactic:
assumption

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 (Set.range f)) = ⨅ i, ⇑(f i)

Tactic:
coe_sInf,

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
h₂ : Red L [(x, !b)]
⊢ Red L [(x, !b)]

Tactic:
assumption

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
H : Step L₁ L₂
⊢ Lift.aux f L₁ = Lift.aux f L₂

Tactic:
obtain @⟨_, _, _, b⟩ := H

Goal state after:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b : Bool
⊢ Lift.aux f (L₁✝ ++ (x✝, b) :: (x✝, !b) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
Q : Submonoid M
hQ : Q.FG
s : Finset M
⊢ (closure ↑s ⊔ Q).FG

Tactic:
rcases hQ with ⟨t, rfl⟩

Goal state after:
M : Type u_1
inst✝ : Monoid M
s t : Finset M
⊢ (closure ↑s ⊔ closure ↑t).FG
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
Q : Subgroup G
hQ : Q.FG
s : Finset G
⊢ (closure ↑s ⊔ Q).FG

Tactic:
rcases hQ with ⟨t, rfl⟩

Goal state after:
G : Type u_3
inst✝ : Group G
s t : Finset G
⊢ (closure ↑s ⊔ closure ↑t).FG
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : ¬#s = 0
⊢ f x = b

Tactic:
have h1 : #s = 1 := le_antisymm hc (Nat.one_le_of_lt (Nat.pos_of_ne_zero hc0))

Goal state after:
case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : ¬#s = 0
h1 : #s = 1
⊢ f x = b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
⊢ ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
let t' k := (t k).filter (fun i ↦ f i ≠ 1)

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
⊢ ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
⊢ (lift f) (of x) = f x

Tactic:
by
  convert! Abelianization.lift_apply_of (FreeGroup.lift f (β := Multiplicative β)) (FreeGroup.of x)
  exact (FreeGroup.lift_apply_of (β := Multiplicative β)).symm

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : α
⊢ of x ≠ 0

Tactic:
by
  intro h
  let f : FreeAbelianGroup α →+ ℤ := lift 1
  have hfx : f (of x) = 1 := lift_apply_of _ _
  have hf0 : f (of x) = 0 := by rw [h, map_zero]
  exact one_ne_zero <| hfx.symm.trans hf0

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x✝ : α
⊢ ((map g).comp (map f)) (of x✝) = (map (g ∘ f)) (of x✝)

Tactic:
simp [map]

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
h₀ : ↑(oreDenom r₁ s₂) * r₁ = oreNum r₁ s₂ * ↑s₂
⊢ oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * s₁)

Tactic:
set v₀ := oreNum r₁ s₂

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
h₀ : ↑(oreDenom r₁ s₂) * r₁ = v₀ * ↑s₂
⊢ v₀ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * s₁)
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 y : M × ↥S
⊢ (f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 * ↑y.2) = g (y.1 * ↑x.2)

Tactic:
by
  rw [lift_mk', lift_mk', mul_inv hg]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a : M
b c : ↥S
⊢ a * ↑(b * c) = a * ↑c * ↑b

Tactic:
Submonoid.coe_mul,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a : M
b c : ↥S
⊢ a * (↑b * ↑c) = a * ↑c * ↑b
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑(sc * sa) * r₁ = rc * ↑(sb * s₂)

Tactic:
Submonoid.coe_mul,

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * ↑sa * r₁ = rc * ↑(sb * s₂)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * ↑sa * r₁ = rc * ↑(sb * s₂)

Tactic:
Submonoid.coe_mul,

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * ↑sa * r₁ = rc * (↑sb * ↑s₂)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

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
y : ↥S
⊢ mk (↑y) y = 1

Tactic:
mk_self

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
y : ↥S
⊢ 1 = 1
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f (f^[n] x)

Tactic:
exact h _

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
hab : a < b
⊢ succ a < succ b

Tactic:
simp [hab]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ a ≤ b ↔ b = a ∨ succ a ≤ b

Tactic:
rw [eq_comm]

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
⊢ Small.{u, w} β

Tactic:
by_cases hβ : Nonempty β

Goal state after:
case pos
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
⊢ Small.{u, w} β

case neg
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : ¬Nonempty β
⊢ Small.{u, w} β
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inr.inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
h0 : a ≠ 0
⊢ c ≠ 0

Tactic:
assumption

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

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
this : ↑x * x.inv = 1
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
⊢ x = default

Tactic:
obtain ⟨y, x_y⟩ := ne_top_iff_exists.1 x_top

Goal state after:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : ↑x * x.inv = 1
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y : ℕ
x_y : ↑y = ↑x
⊢ x = default
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✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : ⟨b, hb⟩ < ⟨c, hc⟩
⊢ ⟨b, hb⟩ ≤ if h : pred ↑⟨c, hc⟩ ∈ s then ⟨pred ↑⟨c, hc⟩, h⟩ else ⟨c, hc⟩

Tactic:
rw [Subtype.mk_lt_mk] at h
    dsimp only
    split
    · exact h.le_pred
    · exact h.le

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 : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x ∈ v.toList

Tactic:
by
      rw [← cons_head_tail v, toList_cons, List.mem_cons]; exact .inr hx

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Nonempty α
inst✝ : ∀ (a : α), Uncountable (π a)
inhabited_h : Inhabited α
⊢ Uncountable (Sigma π)

Tactic:
exact Sigma.uncountable default

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
l : List α
⊢ decodeList (encodeList l) = some l

Tactic:
by
  induction l <;> simp [encodeList, decodeList, unpair_pair, encodek, *]

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

Goal state before:
pp: case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑i ≤ ↑j

Tactic:
assumption

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
⊢ ⨆ a, ↑a = x

Tactic:
by
  rw [← sSup_eq_iSup', h.sSup_Iio]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet (⇑(↑f).symm ⁻¹' s)

Tactic:
exact hs.preimage f.symm.monotone

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
x✝ : α
⊢ f.toRelEmbedding x✝ = g.toRelEmbedding x✝

Tactic:
exact h _

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : Sum.Lex r s f.top g.top
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
exact ⟨Sum.inl <| (f.codRestrict {x | Sum.Lex r s x g.top}
          (fun a => _root_.trans (f.lt_top a) h) h).transRelIso g.subrelIso⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨆ i, f i) x = (⨆ i, ⇑(f i)) x

Tactic:
simp [iSup_apply]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ScottContinuousOn univ Prod.snd

Tactic:
ScottContinuousOn.snd

Goal state after: