mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
⊢ ∀ (a : α), a ∈ m → ((Option.map singleton (f a)).getD 0).bind g = (Option.map g (f a)).getD 0

Tactic:
intro a ham

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
⊢ ((Option.map singleton (f a)).getD 0).bind g = (Option.map g (f a)).getD 0
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * (n + 1).choose (k + 1) + (n + 1).choose (k + 1)

Tactic:
← add_one_mul

Goal state after:
n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1) * (n + 1).choose (k + 1)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!

Tactic:
by
    rwa [Nat.add_sub_cancel_left i j] at this

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

Goal state before:
pp: α : Type u_1
s : Finset α
x : α × α
⊢ x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2

Tactic:
aesop (add simp diag)

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero.zero
⊢ 1 = 1 * 1

Tactic:
Nat.mul_one

Goal state after:
case zero.zero
⊢ 1 = 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).multichoose (k + 1) = n.multichoose (k + 1) + (n + 1).multichoose k

Tactic:
by
  simp [multichoose]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ
k : ℕ
IH : multichoose 1 k = 1
⊢ multichoose 1 (k + 1) = 1

Tactic:
simp [multichoose_succ_succ 0 k, IH]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m → β a
⊢ f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a

Tactic:
induction m using Multiset.induction_on with

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ f ∈ (a ::ₘ m).pi t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
⊢ ⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x

Tactic:
ext ⟨z, w⟩; simp only [mem_prod, mem_iUnion, exists_imp, and_imp, iff_def]; constructor
  · intro x hz hw
    exact ⟨⟨x, hz⟩, x, hw⟩
  · intro x hz x' hw
    exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ univ ^ (n + 2) = univ

Tactic:
pow_succ,

Goal state after:
α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ univ ^ (n + 1) * univ = univ
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
⊢ ⇑m ⁻¹' s * ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s * t)

Tactic:
rintro _ ⟨_, _, _, _, rfl⟩
  exact ⟨_, ‹_›, _, ‹_›, (map_mul m ..).symm⟩

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ submonoid M ↔ IsUnit a

Tactic:
change a ∈ Set.ofPred IsUnit ↔ IsUnit a

Goal state after:
M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ Set.ofPred IsUnit ↔ IsUnit a
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
A : Type u_4
inst✝² : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type u_5
inst✝¹ : Group N
P : Type u_6
inst✝ : Group P
f : G →* N
H : Subgroup G
x : G
hx : x ∈ ↑H
⊢ (f x)⁻¹ ∈ ⇑f '' ↑H

Tactic:
exact ⟨x⁻¹, H.inv_mem hx, f.map_inv x⟩

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1.refine_3
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
⊢ ∀ (x y : G),
    x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) →
      y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → (∃ i, p i ∧ x ∈ K i) → (∃ i, p i ∧ y ∈ K i) → ∃ i, p i ∧ x * y ∈ K i

pp: case refine_1.refine_4
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
⊢ ∀ x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)), (∃ i, p i ∧ x ∈ K i) → ∃ i, p i ∧ x⁻¹ ∈ K i

Tactic:
· rintro x y _ _ ⟨i, hip, hi⟩ ⟨j, hjp, hj⟩
      rcases hK i hip j hjp with ⟨k, hk, hki, hkj⟩
      exact ⟨k, hk, mul_mem (hki hi) (hkj hj)⟩

Goal state after:
case refine_1.refine_4
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
⊢ ∀ x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)), (∃ i, p i ∧ x ∈ K i) → ∃ i, p i ∧ x⁻¹ ∈ K i
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
f : G →* N
⊢ ∀ (x : N), (∃ x_1, (f.domRestrict K) x_1 = x) ↔ ∃ x_1 ∈ K, f x_1 = x

Tactic:
domRestrict_apply,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
f : G →* N
⊢ ∀ (x : N), (∃ x_1, f ↑x_1 = x) ↔ ∃ x_1 ∈ K, f x_1 = x
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ H ≤ f.ker ↔ H = ⊥

Tactic:
f.ker_eq_bot hf,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ H ≤ ⊥ ↔ H = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ≤ K

Tactic:
rw [map_le_iff_le_comap, comap_map_eq_self_of_injective hf]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: M : Type u_6
inst✝ : CommGroup M
S : Subgroup M
n : ℕ
⊢ (map (powMonoidHom n) S).subgroupOf S = (powMonoidHom n).range

Tactic:
ext : 1
  simp [mem_subgroupOf]
  grind

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit
b : Bool
n : ℕ
⊢ bit b n % 2 = (bit b n).bodd.toNat

Tactic:
| bit b n =>

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit
b : Bool
n : ℕ
⊢ (bit b n + 1).div2 = bif (bit b n).bodd then (bit b n).div2.succ else (bit b n).div2

Tactic:
| bit b n =>

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit
b : Bool
n : ℕ
⊢ (bit b n).bodd.toNat + 2 * (bit b n).div2 = bit b n

Tactic:
| bit b n =>

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (decode (encode x)).getD d = x

Tactic:
Encodable.encodek

Goal state after:
α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (some x).getD d = x
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
simp_rw [closure, op_sInf, Set.preimage_ofPred_eq, Subgroup.coe_unop]

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.unop.Normal ↔ H.Normal

Tactic:
← normal_op,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.unop.op.Normal ↔ H.Normal
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
Hs : Set (Subgroup G)
h : ∀ H ∈ Hs, H.Characteristic
⊢ (sInf Hs).Characteristic

Tactic:
by
  simp [sInf_eq_iInf', characteristic_iInf, h]

Goal state after:
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
⊢ a ^ (n.succ + 1) = a

Tactic:
pow_succ,

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
⊢ a ^ (n + 1) * a = a
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ g i✝ ≤ max (f i✝) (g i✝)

Tactic:
· apply le_max_right

Goal state after:
Module: Mathlib.Order.RelIso.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm '' t

Tactic:
rw [e.symm.image_eq_preimage_symm]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm.symm ⁻¹' t
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : Lex (α × β)
h : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
by
    cases x with | h x
    cases y with | h y
    simp only [Prod.Lex.toLex_lt_toLex] at h
    rcases h with (h | h)
    · obtain ⟨v, hv⟩ := exists_gt x.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h, hv]
    · obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense x.2 y.2 h.2
      use toLex (x.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]

Goal state after:
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 * (Int.negSucc m % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))

Tactic:
rw [Int.negSucc_eq, ← Int.natCast_succ, ← Int.add_mul_emod_self_right (b := (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.succ + ↑(m + 1) * ↑n) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange s.subtype ⊔ mrange ((s.subtype.coprod t.subtype).comp (inr ↥s ↥t))

Tactic:
coprod_comp_inr,

Goal state after:
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange s.subtype ⊔ mrange t.subtype
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ c ∈ closure ({a} ∪ {b}) ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
Submonoid.closure_union,

Goal state after:
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ c ∈ closure {a} ⊔ closure {b} ↔ ∃ m n, a ^ m * b ^ n = c
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset (Multiset α)
⊢ m.sup.Nodup ↔ ∀ (a : Multiset α), a ∈ m → a.Nodup

Tactic:
induction m using Multiset.induction_on with

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
this : i = s.min' hs
⊢ IsLeast (↑s) (s.min' hs)

Tactic:
exact isLeast_min' s hs

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

Goal state before:
pp: α : Type u_1
⊢ Function.Injective powerset

Tactic:
intro a₁

Goal state after:
α : Type u_1
a₁ : Multiset α
⊢ ∀ ⦃a₂ : Multiset α⦄, a₁.powerset = a₂.powerset → a₁ = a₂
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset α
⊢ IsLUB (↑s) (s.sup id)

Tactic:
simpa using isLUB_sup (f := id)

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
H : Set.InjOn f ↑s
z : Finset α
a : α
x✝¹ : z ⊆ s
x✝ : a ∈ s
⊢ a ∈ z ↔ f a ∈ image f z

Tactic:
grind [H.eq_iff]

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

Goal state before:
pp: α : Type u_1
a : α
o : Option α
⊢ a ∈ o.toFinset ↔ a ∈ o

Tactic:
cases o <;> simp [eq_comm]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
hf : BddBelow (range f)
⊢ ↑(sInf (range fun i ↦ f i)) = sInf (range fun i ↦ ↑(f i))

Tactic:
WithTop.coe_sInf' (range_nonempty f) hf,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
hf : BddBelow (range f)
⊢ sInf ((fun a ↦ ↑a) '' range f) = sInf (range fun i ↦ ↑(f i))
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ (f ⁻¹' s).Finite

Tactic:
rw [← Set.biUnion_preimage_singleton]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ (⋃ y ∈ s, f ⁻¹' {y}).Finite
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ (⋃ a, ↑(f a)).Finite

Tactic:
by
  rw [← biUnion_range]
  exact h.biUnion fun y _ => y.finite_toSet

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 ∅
⊢ ⨅ i ∈ s, f i ∈ image f s

Tactic:
ciInf_eq_min'_image _ h

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ (image f s).min' ⋯ ∈ image f s
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Icc a b \ {b} ⊆ {a}

Tactic:
h.Icc_eq,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ {a, b} \ {b} ⊆ {a}
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Icc a b \ {a} ⊆ {b}

Tactic:
h.Icc_eq,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ {a, b} \ {a} ⊆ {b}
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ i, b < ↑(f i)
r : α
⊢ ∃ y ∈ range f, r < y

pp: case refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
⊢ ∃ i, a < ↑(f i)

Tactic:
· rcases hf r (WithTop.coe_lt_top r) with ⟨i, hi⟩
    exact ⟨f i, ⟨i, rfl⟩, WithTop.coe_lt_coe.mp hi⟩

Goal state after:
case refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
⊢ ∃ i, a < ↑(f i)
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Set ι
h : (f '' s).Finite
hs : s.Nonempty
a : ι
ha : a ∈ s
hmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ f '' s) j → id (f a) ≤ id j → id j ≤ id (f a)
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ s) f i

Tactic:
exact ⟨a, ha, fun a' ha' hf ↦ hmax (mem_image_of_mem f ha') hf⟩

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictAntiOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
⊢ MaximalFor Q f i

Tactic:
refine ⟨h.prop, fun j hj hle ↦ ?_⟩
  by_contra
  exact h.not_lt hj <| hg ⟨i, h.prop, rfl⟩ ⟨j, hj, rfl⟩ <| lt_of_le_not_ge hle this

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ ⇑f '' s
⊢ x ∈ s ∧ Minimal (fun x ↦ f x ∈ t) x ↔ Minimal (fun x ↦ x ∈ s ∧ f x ∈ t) x

Tactic:
minimal_and_iff_left_of_imp (fun _ hx ↦ f.injective.mem_set_image.1 <| hts hx)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ (insert b (Finset.Ico a b)).val = Icc a b

Tactic:
Finset.Ico_insert_right h

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ (Finset.Icc a b).val = Icc a b
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf ∅ + n = sInf {m | p m}

Tactic:
Nat.sInf_empty,

Goal state after:
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ 0 + n = sInf {m | p m}
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl.refine_1
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)

pp: case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

pp: case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
· rw [add_comm (n / a), Nat.mul_add, mul_one, ← add_assoc]
      refine hn.symm.le.trans (Nat.add_le_add_right ?_ _)
      simpa only [zero_add] using add_le_add (zero_le i) (Nat.mod_lt n ha.bot_lt).le

Goal state after:
case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
⊢ (range f).WellFoundedOn r ↔ WellFounded (r on f)

Tactic:
by
  let f' : β → range f := fun c => ⟨f c, c, rfl⟩
  refine ⟨fun h => (InvImage.wf f' h).mono fun c c' => id, fun h => ⟨?_⟩⟩
  rintro ⟨_, c, rfl⟩
  refine Acc.of_downward_closed f' ?_ _ ?_
  · rintro _ ⟨_, c', rfl⟩ -
    exact ⟨c', rfl⟩
  · exact h.apply _

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

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

Tactic:
simpa [← coe_subset] using Set.Ioc_subset_Iic_self

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α

Tactic:
wellQuasiOrderedLE_iff,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
⊢ (WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite) ↔ WellFoundedLT α
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
n : ℕ
x✝ : n + 2 ≠ 0
H : S
⊢ ↑H ^ (n + 2) = ↑H

Tactic:
pow_succ,

Goal state after:
M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
n : ℕ
x✝ : n + 2 ≠ 0
H : S
⊢ ↑H ^ (n + 1) * ↑H = ↑H
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
n : ℕ
x✝ : n + 2 ≠ 0
H : S
⊢ ↑H ^ (n + 1) * ↑H = ↑H

Tactic:
coe_set_pow n.succ_ne_zero,

Goal state after:
M : Type u_3
S : Type u_6
inst✝² : Monoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
n : ℕ
x✝ : n + 2 ≠ 0
H : S
⊢ ↑H * ↑H = ↑H
Module: Mathlib.Order.WellFoundedSet

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

Tactic:
let t : Set s := {x | x ≤ a}

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
t : Set ↑s := {x | ↑x ≤ a}
⊢ ∃ b ≤ a, Minimal (fun x ↦ x ∈ s) b
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ↑(closure s) * s = ↑(closure s)

Tactic:
rw [← Set.iUnion_op_smul_set]

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ⋃ a ∈ s, ↑(closure s) <• a = ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ s ^ (n + 1) * ↑(closure s) = ↑(closure s)

Tactic:
pow_succ,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ s ^ n * s * ↑(closure s) = ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
⊢ Submonoid.closure ({g} ∪ {g}⁻¹) = Submonoid.powers g ⊔ Submonoid.powers g⁻¹

Tactic:
Submonoid.closure_union,

Goal state after:
G : Type u_2
inst✝ : Group G
g : G
⊢ Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹ = Submonoid.powers g ⊔ Submonoid.powers g⁻¹
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ {x | x ∈ map (⇑f) s}.Pairwise Commute

Tactic:
by
  simp only [Multiset.mem_map]
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ _
  exact (comm.of_refl hx hy).map f

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
y : α
h : ∀ x ∈ s, Commute y x
⊢ Commute y (s.noncommProd comm)

Tactic:
by
  induction s using Quotient.inductionOn
  simp only [quot_mk_to_coe, noncommProd_coe]
  exact Commute.list_prod_right _ _ h

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ (prod.comp (map f)) x = prod ((map f) x)

Tactic:
MonoidHom.coe_comp,

Goal state after:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ (⇑prod ∘ ⇑(map f)) x = prod ((map f) x)
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
⊢ ∏ i, f i = ∏ i, g i

Tactic:
by
  rw [← prod_subset s.toFinset.subset_univ (by simpa), prod_subtype (p := (· ∈ s)) _ (by simp)]
  congr! with ⟨x, h⟩
  exact w x h

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ mk ⁻¹' mk '' s → a ∈ ↑N * s

Tactic:
rintro ⟨b, hb, h⟩

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a b : G
hb : b ∈ s
h : ↑b = ↑a
⊢ a ∈ ↑N * s
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_5
inst✝³ : DecidableEq ι
inst✝² : CommMonoid κ
inst✝¹ : LT κ
inst✝ : MulLeftStrictMono κ
s : Finset ι
d : ι
hd : d ∈ s
f : ι → κ
hdf : 1 < f d
⊢ ∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m

Tactic:
conv in ∏ m ∈ s, f m => rw [← Finset.insert_erase hd]

Goal state after:
ι : Type u_1
κ : Type u_5
inst✝³ : DecidableEq ι
inst✝² : CommMonoid κ
inst✝¹ : LT κ
inst✝ : MulLeftStrictMono κ
s : Finset ι
d : ι
hd : d ∈ s
f : ι → κ
hdf : 1 < f d
⊢ ∏ m ∈ s.erase d, f m < ∏ m ∈ insert d (s.erase d), f m