mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
⊢ ∃ m n, m < n ∧ (fun x1 x2 ↦ x1 ≤ x2) (f m) (f n)

Tactic:
contrapose! hc
    refine ⟨Set.range (f ∘ g), ?_, ?_⟩
    · rintro _ ⟨m, rfl⟩ _ ⟨n, rfl⟩ _ hf
      obtain h | rfl | h := lt_trichotomy m n
      · exact hc _ _ (g.strictMono h) hf
      · contradiction
      · exact h2 _ _ h (lt_of_le_not_ge hf (hc _ _ (g.strictMono h)))
    · refine Set.infinite_range_of_injective fun m n (hf : f (g m) = f (g n)) ↦ ?_
      obtain h | rfl | h := lt_trichotomy m n <;>
        (first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f m) (f n)

Tactic:
hmn

Goal state after:
case refine_1.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f n) (f n)
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Preorder α
p : α → Prop
inst✝⁵ : DecidablePred p
y : α
F : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : Preorder M
inst✝³ : Preorder N
inst✝² : EquivLike F M N
inst✝¹ : OrderIsoClass F M N
f : F
inst✝ : LocallyFiniteOrder N
⊢ ∀ (a b x : M), x ∈ map { toFun := EquivLike.inv f, inj' := ⋯ } (finsetIco (f a) (f b)) ↔ a ≤ x ∧ x < b

Tactic:
by
    simp [finset_mem_Ico, EquivLike.inv_apply_eq, map_lt_map_iff]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f m)

Tactic:
hmn

Goal state after:
case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f n)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Icc a b) - 2

Tactic:
rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one]

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Icc a b) - 1 - 1 = #(Icc a b) - 2
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ f a ∈ f '' U

Tactic:
Set.mem_image

Goal state after:
case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ ∃ x ∈ U, f x = f a
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ ↑(centralizer s)
h : G
hh : h ∈ s
⊢ f (h * g) = f (g * h)

Tactic:
hg h hh

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ ↑(centralizer s)
h : G
hh : h ∈ s
⊢ f (g * h) = f (g * h)
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalizerMonoidHom.ker = (centralizer ↑H).subgroupOf (normalizer ↑H)

Tactic:
by
  simp [Subgroup.ext_iff, DFunLike.ext_iff, Subtype.ext_iff,
    mem_subgroupOf, mem_centralizer_iff, eq_mul_inv_iff_mul_eq, eq_comm]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s ∈ ↑(closure S)

Tactic:
rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff]
  exact subset_closure (mem_inv.mp hs)

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
N H : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(N ⊔ H) = ↑N * ↑H

Tactic:
rw [← set_mul_normalizer_comm _ _ hLE, sup_comm, coe_mul_of_left_le_normalizer_right _ _ hLE]

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

Goal state before:
pp: case inv_mem
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' : G
hg' : g' ∈ s
x : X
hx : x ∈ t
⊢ g'⁻¹ • x ∈ t

Tactic:
| inv_mem g' hg' =>

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
h : a ∉ s
⊢ (insert a s).prod = fun f ↦ f a * ∏ x ∈ s, f x

Tactic:
funext f
  rw [Finset.prod_insert h]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : ℤ
⊢ (fun x ↦ ((map 1) x).sum) ((fun x ↦ of default ^ x) x) = x

Tactic:
by
    induction x with
    | zero => simp
    | succ x hx => simpa [zpow_add_one] using hx
    | pred x hx => simpa [zpow_sub_one, ← sub_eq_add_neg] using hx

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type u
f : FreeAbelianGroup (α → β)
⊢ FreeAbelianGroup α →+ FreeAbelianGroup β

Tactic:
refine .mk' (f <*> ·) fun x y ↦ ?_
  change lift (· <$> (x + y)) _ = lift (· <$> x) _ + lift (· <$> y) _
  simp [← Pi.add_def]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
| f n

Tactic:
Finset.eq_prod_range_div f

Goal state after:
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
| f 0 * ∏ i ∈ range n, f (i + 1) / f i
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x✝ y✝ : FreeAbelianGroup α
h₁ : (lift (g ∘ f)) x✝ = (lift g) ((map f) x✝)
h₂ : (lift (g ∘ f)) y✝ = (lift g) ((map f) y✝)
⊢ (lift (g ∘ f)) (x✝ + y✝) = (lift g) ((map f) (x✝ + y✝))

Tactic:
simp only [h₁, h₂, map_add]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅⊤, H⁆ ≤ H ↔ H.Normal

Tactic:
by
  refine ⟨fun hle ↦ ⟨fun h hh g ↦ ?_⟩, fun h ↦ commutator_le_right ⊤ H⟩
  exact (H.mul_mem_cancel_right <| H.inv_mem hh).mp <| commutator_le.mp hle g trivial h hh

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
⊢ ∀ (x : α),
    ((fun F ↦ (↑F).comp ofMulHom)
          ((fun f ↦
              let __src := lift ⇑f;
              { toFun := ⇑(lift ⇑f), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
            f))
        x =
      f x

Tactic:
by
    simp only [RingHom.coe_monoidHom_mk, MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk,
      ofMulHom_coe, Function.comp_apply, lift_apply_of, forall_const]

Goal state after:
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 : N
⊢ g (f.sec (x * y)).1 * g ↑(f.sec y).2 =
    g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹

Tactic:
mul_inv_right hg

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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 * g ↑(f.sec y).2 * g ↑(f.sec x).2 = g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).1
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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
⊢ (f.toMonoidHom.comp k.toMonoidHom) x = (f.toMonoidHom.comp k.toMonoidHom) y → ∃ c, ↑c * x = ↑c * y

Tactic:
by
      rw [MonoidHom.comp_apply, MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe,
        MonoidHom.coe_coe, toMonoidHom_apply, toMonoidHom_apply, f.eq_iff_exists]
      rintro ⟨c, hc⟩
      let ⟨d, hd⟩ := k.surjective c
      refine ⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, ?_⟩
      rw [← hd, ← map_mul k, ← map_mul k] at hc; exact k.injective hc

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b c : WithTop α
⊢ (a + b) * c = a * c + b * c

Tactic:
by
    cases c with
    | top => by_cases ha : a = 0 <;> simp [ha]
    | coe c =>
      by_cases hc : c = 0; · simp [hc]
      simp only [mul_coe_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (add_mul _ _ _)

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccLimit a
⊢ IsSuccLimit ↑a

Tactic:
refine ⟨?_, ha.isSuccPrelimit.subtypeVal hs⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccLimit a
⊢ ¬IsMin ↑a
Module: Mathlib.Data.Fintype.Sum

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

Tactic:
rw [image_subset_iff]

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ ∀ x ∈ univ, b ↑x ∈ (image b univ).erase k
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
⊢ ∏ j ∈ s, f j = ∏ j ∈ s, g j ↔ f i = g i

Tactic:
rw [prod_eq_mul_prod_sdiff_singleton_of_mem hi, prod_eq_mul_prod_sdiff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]

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

Goal state before:
pp: α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ s = range (Subtype.val ∘ f)

Tactic:
hf.range_comp,

Goal state after:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ s = range Subtype.val
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Unique α
inst✝ : LE β
a✝ b✝ : Lex (α × β)
a b : α × β
heq : a.1 = b.1
⊢ { toFun := fun x ↦ (ofLex x).2, invFun := fun x ↦ toLex (default, x), left_inv := ⋯, right_inv := ⋯ } (toLex a) ≤
      { toFun := fun x ↦ (ofLex x).2, invFun := fun x ↦ toLex (default, x), left_inv := ⋯, right_inv := ⋯ } (toLex b) ↔
    toLex a ≤ toLex b

Tactic:
simp [Prod.Lex.toLex_le_toLex, heq]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
a : α
⊢ inl ⊥ ≤ inl a

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
b : β
⊢ inl ⊥ ≤ inr b

Tactic:
· exact Lex.inl bot_le

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
b : β
⊢ inl ⊥ ≤ inr b
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : α
b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inl a ≤ inr b

Tactic:
exact iff_of_false (@not_inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _) not_inr_le_inl

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
⊢ IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ioi a ⊆ s

Tactic:
by
  simp [isUpperSet_iff_forall_lt, subset_def, @forall_comm (_ ∈ s)]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsEmpty α
b : β
H : ∀ (b' : β), ¬s b' b
⊢ ∀ (b_1 : β), b_1 ∈ Set.range ⇑(RelEmbedding.ofIsEmpty r s) ↔ s b_1 b

Tactic:
by simp [H]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LT α
f : α ≤i β
h : b ≤ f a
⊢ b ∈ Set.range ⇑f

Tactic:
obtain rfl | hb := h.eq_or_lt
  exacts [⟨a, rfl⟩, f.mem_range_of_rel hb]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: β : 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}
⊢ IsLUB ((fun b ↦ b.1 ⊔ b.2) '' d) ((fun b ↦ b.1 ⊔ b.2) (p₁, p₂))

Tactic:
simp only [IsLUB, IsLeast, upperBounds, mem_image, Prod.exists, forall_exists_index, and_imp]

Goal state after:
β : 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}
⊢ p₁ ⊔ p₂ ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} ∧
    p₁ ⊔ p₂ ∈ lowerBounds {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) → b ∈ f (o.get h)

Tactic:
rintro ⟨a, ha, hb⟩

Goal state after:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
a : α
ha : a ∈ o
hb : b ∈ f a
⊢ b ∈ f (o.get h)
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ (∃ a_1, (∃ a, a ∈ f ∧ a_1 ∈ g a) ∧ a ∈ k a_1) ↔ ∃ a_1, a_1 ∈ f ∧ ∃ a_2, a_2 ∈ g a_1 ∧ a ∈ k a_2

Tactic:
exact ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩,
           fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ map g (x.bind f) = x.bind fun y ↦ map g (f y)

Tactic:
by
  rw [← bind_some_eq_map, bind_assoc]; simp [bind_some_eq_map]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type u_4
x : Part α✝
y : Part β✝
⊢ (x *> y).Dom ↔ (const α✝ id <$> x <*> y).Dom

Tactic:
simp [SeqRight.seqRight, Part.bind, assert, Seq.seq, (· <$> ·)]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ {z : α}, z ∈ bot x f → z < x → f z ≤ x

Tactic:
intro y hy hyx

Goal state after:
case base_isLeast.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
hyx : y < x
⊢ f y ≤ x
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ⊢ ∀ {a b c d : Cardinal.{u_1}}, a ≤ b → c ≤ d → a + c ≤ b + d

Tactic:
rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩

Goal state after:
case mk.mk.mk.mk
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
d✝ : Cardinal.{u_1}
δ : Type u_1
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ Quot.mk (⇑isEquivalent) α + Quot.mk (⇑isEquivalent) γ ≤ Quot.mk (⇑isEquivalent) β + Quot.mk (⇑isEquivalent) δ
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case pos
a b c : Cardinal.{u_1}
h : b ≤ c
ha : a = 0
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
simp [ha, zero_power_le]

Goal state after:
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

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

Tactic:
← MonoidHom.coe_comp,

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
κ : φ.CompTriple ψ χ
⊢ ⇑(ψ.comp φ) = ⇑χ
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ x = y

Tactic:
convert congr_arg (g⁻¹ • ·) h <;> simp [← smul_assoc]

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

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
⊢ ∃ s, n = s.card

Tactic:
obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq α n

Goal state after:
case inr
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
s : Finset α
hs : s.card = n
⊢ ∃ s, n = s.card
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
n : ℕ
⊢ (n + 2) • a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀

Tactic:
rw [succ_nsmul, add_lt_aleph0_iff, nsmul_lt_aleph0_iff]

Goal state after:
a : Cardinal.{u_1}
n : ℕ
⊢ (n + 1 = 0 ∨ a < ℵ₀) ∧ a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
α : Type u_2
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ a • (algebraMap R A) r = (algebraMap R A) r

Tactic:
rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S : Type u_6
M : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : Semiring R₄
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : AddCommMonoid M₄
inst✝¹ : AddCommMonoid N₁
inst✝ : AddCommMonoid N₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e✝ e' e : M ≃ₛₗ[σ] M₂
r : S
x : M₂
⊢ ((↑e).inverse e.invFun ⋯ ⋯) (r • x) = σ' r • ((↑e).inverse e.invFun ⋯ ⋯) x

Tactic:
rw [map_smulₛₗ]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
c : R
x : M
⊢ f (c • x) = σ c • f x

Tactic:
rw [map_smulₛₗ]

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

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

Tactic:
rw [map_smulₛₗ]

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

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

Tactic:
rw [map_smulₛₗ]

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

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (φ (φ' m) • f (g x)) = g (f (φ' m • g x))

Tactic:
rw [map_smulₛₗ]

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

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

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

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R'
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R' M'
σ₁₂ : R →+* R'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝³ x✝² : Sᵈᵐᵃ
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ ((x✝³ + x✝²) • x✝¹) x✝ = (x✝³ • x✝¹ + x✝² • x✝¹) x✝

Tactic:
simp_rw [add_apply, DomMulAct.smul_linearMap_apply, ← map_add, ← add_smul]; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i

Tactic:
rw [← SetLike.mem_coe, coe_iInf, Set.mem_iInter]; rfl

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
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 τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n : ℕ
x : M
h : x ∈ (fun n ↦ (f ^ n).ker) n
c : ℕ
w : n ≤ n + c
⊢ x ∈ (fun n ↦ (f ^ n).ker) (n + c)

Tactic:
LinearMap.mem_ker

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
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 τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n : ℕ
x : M
h : (f ^ n) x = 0
c : ℕ
w : n ≤ n + c
⊢ x ∈ (fun n ↦ (f ^ n).ker) (n + c)