mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h
α : Type u_3
inst✝ : Monoid α
a : α
s : List α
comm : {x | x ∈ a ::ₘ ⟦s⟧}.Pairwise Commute
⊢ a * s.prod = s.prod * a

Tactic:
induction s with
  | nil => simp
  | cons hd tl IH =>
    rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
    · congr 1
      apply comm.of_refl <;> simp
    · intro x hx y hy
      simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
      apply comm
      · cases hx <;> simp [*]
      · cases hy <;> simp [*]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
hHnK : normalizer ↑H ≤ normalizer ↑K
⊢ normalizer ↑H ≤ normalizer ↑(K ⊔ H)

Tactic:
by
  rw [sup_comm]
  exact normalizer_le_normalizer_sup_of_normalizer_le_left hHnK

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

Goal state before:
pp: case mul
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
y : M
hy✝ : y ∈ closure s
hy : ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = y
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
⊢ ∃ f_1 t_1, ↑t_1 ⊆ s ∧ Function.support f_1 ⊆ ↑t_1 ∧ ∏ a ∈ t_1, a ^ f_1 a = (∏ a ∈ t, a ^ f a) * y

Tactic:
obtain ⟨g, u, hus, hg, rfl⟩ := hy

Goal state after:
case mul
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∃ f_1 t_1, ↑t_1 ⊆ s ∧ Function.support f_1 ⊆ ↑t_1 ∧ ∏ a ∈ t_1, a ^ f_1 a = (∏ a ∈ t, a ^ f a) * ∏ a ∈ u, a ^ g a
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
⊢ ∏ a ∈ s₁ ∩ s₂, f a = ∏ a ∈ s₁ ∩ s₂, g a

Tactic:
exact prod_congr rfl (by simpa)

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

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

Tactic:
rw [← lift_unique (prod.comp (map f)) (by simp), MonoidHom.coe_comp, Function.comp_apply]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ FG M ↔ ∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ

Tactic:
refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeMonoid.lift Subtype.val, ?_⟩, ?_⟩
  · rwa [← MonoidHom.mrange_eq_top, ← Submonoid.closure_eq_mrange]
  · rintro ⟨S, hfin : Finite S, φ, hφ⟩
    refine fg_iff.mpr ⟨φ '' Set.range FreeMonoid.of, ?_, Set.toFinite _⟩
    simp [← MonoidHom.map_mclosure, hφ, FreeMonoid.closure_range_of, ← MonoidHom.mrange_eq_map]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Monoid M
⊢ FG M → ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

Tactic:
rw [fg_iff_exists_freeMonoid_hom_surjective]
    intro ⟨S, hS, φ, hφ⟩
    obtain ⟨n, ⟨e⟩⟩ := hS.exists_equiv_fin S
    exact ⟨Fin n, inferInstance, φ.comp (FreeMonoid.freeMonoidCongr e).symm,
      hφ.comp (FreeMonoid.freeMonoidCongr e).symm.surjective⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
⊢ P.FG

Tactic:
rw [fg_iff]

Goal state after:
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
⊢ ∃ S, closure S = P ∧ S.Finite
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
constructor <;>
      · rw [map_commutator]
        apply commutator_mono <;>
          simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
⊢ (lift ⇑f) (of L1 * of L2) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)

Tactic:
simp_rw [of_mul_of, lift_apply_of]

Goal state after:
case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
⊢ f (L1 * L2) = f L1 * f L2
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ IsMulCommutative (G ⧸ N) ↔ _root_.commutator G ≤ N

Tactic:
refine ⟨fun hcomm ↦ ?_, fun hGN ↦ ⟨⟨fun x' y' ↦ ?_⟩⟩⟩
  · rw [commutator_eq_normalClosure, ← Subgroup.normalClosure_subset_iff]
    rintro x ⟨p, q, rfl⟩
    rw [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def]
    simp only [QuotientGroup.mk_mul, QuotientGroup.mk_inv]
    rw [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm, mul_comm']
  · obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N x'
    obtain ⟨y, rfl⟩ := QuotientGroup.mk'_surjective N y'
    rw [← commutatorElement_eq_one_iff_mul_comm, ← map_commutatorElement, QuotientGroup.mk'_apply,
      QuotientGroup.eq_one_iff]
    apply hGN
    rw [commutator_eq_closure]
    exact Subgroup.subset_closure (commutator_mem_commutatorSet x y)

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g✝ f g : α →*o β
h : (fun f ↦ (↑f.toMonoidHom).toFun) f = (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f g✝ g : α →*o β
toFun✝ : α → β
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_one' := map_one'✝ }.toFun x * { toFun := toFun✝, map_one' := map_one'✝ }.toFun y
monotone'✝ : Monotone (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f ↦ (↑f.toMonoidHom).toFun)
      { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ } = g
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : Mul γ
inst✝ : Mul δ
f✝ g✝ f g : α ≃*o β
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : Mul γ
inst✝ : Mul δ
f g✝ g : α ≃*o β
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x * y) =
      { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x *
        { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
map_le_map_iff'✝ :
  ∀ {a b : α},
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝ }.toFun
          a ≤
        { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝,
              map_mul' := map_mul'✝ }.toFun
          b ↔
      a ≤ b
h₁ :
  { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_le_map_iff' := map_le_map_iff'✝ }.toFun =
    g.toFun
h₂ :
  { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_le_map_iff' := map_le_map_iff'✝ }.invFun =
    g.invFun
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
      map_le_map_iff' := map_le_map_iff'✝ } =
    g
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g✝ f g : α →*₀o β
h : (fun f ↦ (↑f.toMonoidWithZeroHom).toFun) f = (fun f ↦ (↑f.toMonoidWithZeroHom).toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g✝ g : α →*₀o β
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun x * { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun y
monotone'✝ :
  Monotone (↑{ toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f ↦ (↑f.toMonoidWithZeroHom).toFun)
      { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝,
        monotone' := monotone'✝ } =
    (fun f ↦ (↑f.toMonoidWithZeroHom).toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝, monotone' := monotone'✝ } =
    g
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mpr
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)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝¹ : M × ↥S
h✝¹ : z * f ↑w✝¹.2 = f w✝¹.1
w✝ : M × ↥S
h✝ : w * f ↑w✝.2 = f w✝.1
⊢ z = w

Tactic:
← f.mk'_sec z,

Goal state after:
case mpr
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)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝¹ : M × ↥S
h✝¹ : z * f ↑w✝¹.2 = f w✝¹.1
w✝ : M × ↥S
h✝ : w * f ↑w✝.2 = f w✝.1
⊢ f.mk' (f.sec z).1 (f.sec z).2 = w
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * ↑s ∈ S
⊢ (c • 1 /ₒ 1) • (r /ₒ s) = (c • 1 /ₒ 1) • (t • r /ₒ ⟨t * ↑s, ht⟩)

Tactic:
← OreLocalization.expand

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
c : R
r : X
t : M
s : ↥S
ht : t * ↑s ∈ S
⊢ (c • 1 /ₒ 1) • (r /ₒ s) = (c • 1 /ₒ 1) • (r /ₒ s)
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
x : WithTop α
⊢ IsSuccPrelimit x ↔ x = ⊤ ∨ ∃ y, x = ↑y ∧ IsSuccPrelimit y

Tactic:
cases x with
  | coe x => simp [IsSuccPrelimit, WithTop.forall]
  | top => simp [IsSuccPrelimit]

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsSuccPrelimit a
b : α
hb : ¬IsMax b ∧ succ b = a
⊢ a ∈ range succ

Tactic:
exact ⟨b, hb.2⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
⊢ a ≤ b → ∃ n, pred^[n] b = a

Tactic:
hab

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a ≤ b
⊢ ∃ n, pred^[n] b = a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : ¬IsMax a
⊢ f (succ a) = succ (f a)

Tactic:
exact ((apply_covBy_apply_iff f).2 <| covBy_succ_of_not_isMax h).succ_eq.symm

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

Goal state before:
pp: X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
hx : succ m ∈ S
⊢ False

Tactic:
exact hm' hx

Goal state after:
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: α : Type v
inst✝ : Small.{w, v} α
x y : Shrink.{w, v} α
w : (equivShrink α).symm x = (equivShrink α).symm y
⊢ x = y

Tactic:
by
  simpa using w

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 ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g = update (s.piecewise f g) j (f j)

Tactic:
by
  simp only [← piecewise_coe, ← Set.piecewise_insert]
  ext
  congr
  simp

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
α✝ β✝ : Type u_2
x✝¹ : Const α α✝
x✝ : Const α β✝
⊢ x✝¹ <* x✝ = Function.const β✝ <$> x✝¹ <*> x✝

Tactic:
by simp [Seq.seq, SeqLeft.seqLeft]

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ : Type u_2
x✝¹ : AddConst α α✝
x✝ : AddConst α β✝
⊢ x✝¹ <* x✝ = Function.const β✝ <$> x✝¹ <*> x✝

Tactic:
by simp [Seq.seq, SeqLeft.seqLeft]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
s : Finset α
f : α → β
hfst : image f s ⊆ t
hfs : Set.InjOn f ↑s
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
classical
    induction s using Finset.induction generalizing f with
    | empty =>
      obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
      use e
      simp
    | insert a s has H => ?_
    have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
    have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
    obtain ⟨g', hg'⟩ := H hfst' hfs'
    have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
    use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
    simp_rw [mem_insert]
    rintro i (rfl | hi)
    · simp
    rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
    · exact
        ne_of_apply_ne Subtype.val
          (ne_of_eq_of_ne (hg' _ hi) <|
            hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
    · exact g'.injective.ne (ne_of_mem_of_not_mem hi has)

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
⊢ (map f v).head = f v.head

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
  rw [h, map_cons, head_cons, head_cons]

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Nonempty α
inst✝ : Uncountable β
⊢ Uncountable (α × β)

Tactic:
by
  inhabit α
  exact (Prod.mk_right_injective default).uncountable

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ ofFn (ofFn f).tail.get = ofFn fun i ↦ f i.succ

Tactic:
congr
    funext i
    rw [get_tail, get_ofFn]
    rfl

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
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ ((↑v).insertIdx (↑i) a).length = n + 1

Tactic:
by
    rw [List.length_insertIdx, v.2]
    split <;> lia

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

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map some (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = map some s

Tactic:
refine Eq.trans ?_ (.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe ?_)

Goal state after:
case neg.refine_1
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map some (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = map Subtype.val (decode (Sum.inr s)).attach

case neg.refine_2
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∏ a ∈ {x | p x}.toFinset, f a = ∏ a, f ↑a

Tactic:
rw [← Finset.prod_subtype]
  simp_rw [Set.mem_toFinset]; intro; rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
t : β
x : α
hx : x ∈ f t
⊢ ∃ x_1, ↑x_1 ∈ f ↑⟨t, ⋯⟩

Tactic:
exact ⟨⟨x, (h'f t hx)⟩, hx⟩

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
i : α
his : i ∈ s
hi : y < i
⊢ sSup s ∈ s

Tactic:
exact eq_of_le_of_not_lt (le_csSup hbdd his) (hy.2 hi) ▸ his

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp [isSuccPrelimit_bot] at hlim
  · apply csSup_mem_of_not_isSuccLimit hs _ <| mt IsSuccLimit.isSuccPrelimit hlim
    contrapose! hlim
    rw [csSup_of_not_bddAbove hlim, csSup_empty]
    exact isSuccPrelimit_bot

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

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
y : α
hy : y < x
⊢ y < ⨆ a, succ ↑a

Tactic:
rw [lt_ciSup_iff' H]

Goal state after:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
y : α
hy : y < x
⊢ ∃ i, y < succ ↑i
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b ↑(collapseF f a)

Tactic:
rw [collapseF, IsWellFounded.fix_eq]
  dsimp only
  exact WellFounded.not_lt_min _ {b | ∀ a', r a' a → s (collapseF f a') b} h

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case refine_1
β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
⊢ a ≤ p₁ ⊔ p₂

Tactic:
rw [← hba]

Goal state after:
case refine_1
β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
⊢ b₁ ⊔ b₂ ≤ p₁ ⊔ p₂
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ maxChain r

Tactic:
rw [maxChain_spec.right this (subset_insert _ _)]

Goal state after:
α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ insert a (maxChain r)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ some (Classical.choose h')

Tactic:
have hh := Classical.choose_spec h'

Goal state after:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (Classical.choose h') ∈ c
⊢ x ∈ some (Classical.choose h')
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
⊢ toNat (lift.{?u.17, u} #α) = toNat #β

Tactic:
(lift_mk_eq.{_, _, v}).mpr ⟨e⟩,

Goal state after:
α : Type u
β : Type v
e : α ≃ β
⊢ toNat (lift.{max u v, v} #β) = toNat #β
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ ¬#α ≤ 1 ↔ Nontrivial α

Tactic:
le_one_iff_subsingleton,

Goal state after:
α : Type u
⊢ ¬Subsingleton α ↔ Nontrivial α
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) = #↑s + 1

Tactic:
by
  rw [← union_singleton, mk_union_of_disjoint, mk_singleton]
  simpa

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

Goal state before:
pp: a : Cardinal.{u_1}
h : a ≠ 0
⊢ 0 ^< a = 1

Tactic:
by
  apply (powerlt_le.2 fun c _ => zero_power_le _).antisymm
  rw [← power_zero]
  exact le_powerlt 0 (pos_iff_ne_zero.2 h)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic

Goal state before:
pp: M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : mk.symm c₁ • a ≠ mk.symm c₂ • a
⊢ x = y

Tactic:
have := Classical.decEq α

Goal state after:
M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : mk.symm c₁ • a ≠ mk.symm c₂ • a
this : DecidableEq α
⊢ x = y