mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
a✝ b✝ : { N // N.Normal }
h : ∀ {x y : G}, x⁻¹ * y ∈ ↑a✝ → x⁻¹ * y ∈ ↑b✝
x : G
x✝ : x ∈ ↑a✝
⊢ x ∈ ↑b✝

Tactic:
specialize @h 1 x

Goal state after:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
a✝ b✝ : { N // N.Normal }
x : G
h : 1⁻¹ * x ∈ ↑a✝ → 1⁻¹ * x ∈ ↑b✝
x✝ : x ∈ ↑a✝
⊢ x ∈ ↑b✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : ∏ x ∈ s \ {x, g x hx}, f x = 1
⊢ ∏ x ∈ s, f x = 1

Tactic:
rw [← prod_sdiff this, h, one_mul]
    cases eq_or_ne (g x hx) x with
    | inl hx' => simpa [hx'] using hg₃ x hx
    | inr hx' => grind

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
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
x : M
⊢ x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x} → x ∈ P

Tactic:
intro hx

Goal state after:
case mp
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
x : M
hx : x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
⊢ x ∈ P
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
simp_rw [neg_mul, map_neg, neg_mul]

Goal state after:
case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
ih : (lift ⇑f) (of L1 * of L2) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)
⊢ -(lift ⇑f) (of L1 * of L2) = -((lift ⇑f) (of L1) * (lift ⇑f) (of L2))
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.10
inst✝ : MulAction R X
⊢ Equivalence fun rs rs' ↦ ∃ u v, u • rs'.fst = v • rs.fst ∧ ↑u * ↑rs'.snd = v * ↑rs.snd

Tactic:
by
    refine ⟨fun _ => ⟨1, 1, by simp⟩, ?_, ?_⟩
    · rintro ⟨r, s⟩ ⟨r', s'⟩ ⟨u, v, hru, hsu⟩; dsimp only at *
      rcases oreCondition (s : R) s' with ⟨r₂, s₂, h₁⟩
      rcases oreCondition r₂ u with ⟨r₃, s₃, h₂⟩
      have : r₃ * v * s = s₃ * s₂ * s := by
        -- Porting note: the proof used `assoc_rw`
        rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
      rcases ore_right_cancel (r₃ * v) (s₃ * s₂) s this with ⟨w, hw⟩
      refine ⟨w * (s₃ * s₂), w * (r₃ * u), ?_, ?_⟩ <;>
        simp only [Submonoid.coe_mul, Submonoid.smul_def, ← hw]
      · simp only [mul_smul, hru, ← Submonoid.smul_def]
      · simp only [mul_assoc, hsu]
    · rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨r₃, s₃⟩ ⟨u, v, hur₁, hs₁u⟩ ⟨u', v', hur₂, hs₂u⟩
      rcases oreCondition v' u with ⟨r', s', h⟩; dsimp only at *
      refine ⟨s' * u', r' * v, ?_, ?_⟩ <;>
        simp only [Submonoid.smul_def, Submonoid.coe_mul, mul_smul, mul_assoc] at *
      · rw [hur₂, smul_smul, h, mul_smul, hur₁]
      · rw [hs₂u, ← mul_assoc, h, mul_assoc, hs₁u]

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
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
⊢ Injective fun a ↦ a ^ n

Tactic:
rintro ⟨a⟩ ⟨b⟩ (hab : mk a.1 a.2 ^ n = mk b.1 b.2 ^ n)
    change mk a.1 a.2 = mk b.1 b.2
    simp only [mk_pow, mk_eq_mk_iff, r_iff_exists, SubmonoidClass.coe_pow, Subtype.exists,
      exists_prop] at hab ⊢
    obtain ⟨c, hc, hab⟩ := hab
    refine ⟨c, hc, pow_left_injective hn ?_⟩
    obtain _ | n := n
    · simp
    · simp [mul_pow, pow_succ c, mul_assoc, hab]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
inst✝ : LT α
a b : WithTop α
ha : a < ⊤
hb : b < ⊤
⊢ a * b < ⊤

Tactic:
by
  rw [WithTop.lt_top_iff_ne_top] at *
  exact mul_ne_top ha hb

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * c = a * (b * c)

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * 0 = a * (b * 0)

case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a * b * c = a * (b * c)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
r✝ : X
s✝ : ↥S
⊢ (r /ₒ 1) • (r✝ /ₒ s✝) = r • (r✝ /ₒ s✝)

Tactic:
rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]

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

Goal state before:
pp: case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝¹ fun b ↦ Option.some (c * b)) + Option.bind ↑a✝ fun b ↦ Option.some (c * b)

Tactic:
exact congr_arg some (mul_add _ _ _)

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
⊢ (∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (succ i)

Tactic:
refine ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ ?_⟩
  obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)
  have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose hi; simp [hi]
  rw [← Nat.succ_pred_eq_of_pos hj]
  simp only [Function.iterate_succ', Function.comp_apply]
  apply h

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

Goal state before:
pp: case neg
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 ≤ m
hmS : m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
· exact IH hm hn hmS

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n] b ∈ s
⊢ f (pred^[n] b) ≤ f b

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)

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 = default

Tactic:
have x_top : x.val ≠ ⊤ := by
      intro h
      simp [h] at this

Goal state after:
a b c d m n : ℕ∞
x : ℕ∞ˣ
this : ↑x * x.inv = 1
x_top : ↑x ≠ ⊤
⊢ x = default
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
s : Finset ι
inst✝ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ s.piecewise f g ∈ t.pi t'

Tactic:
by
  rw [← piecewise_coe]; exact Set.piecewise_mem_pi (↑s) hf hg

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1

Tactic:
by
  rw [Finset.prod_dite, Finset.univ_eq_attach, Finset.prod_const_one, mul_one]
  congr
  · simp
  · ext; simp
  · apply Function.hfunext <;> simp +contextual [Subtype.heq_iff_coe_eq]

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

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

Tactic:
| insert a s has H =>

Goal state after:
case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hmin : IsMin (sSup s)
a : α
has : a ∈ s
⊢ sSup s ∈ s

Tactic:
← hmin.eq_of_le <| le_csSup hbdd has

Goal state after:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hmin : IsMin (sSup s)
a : α
has : a ∈ s
⊢ a ∈ s
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
⊢ ⨆ a, succ ↑a = x

Tactic:
by
  have H : BddAbove (range fun a : Iio x ↦ succ a.1) :=
    ⟨succ x, by simp +contextual [upperBounds, succ_le_succ, le_of_lt]⟩
  apply le_antisymm _ (le_of_forall_lt fun y hy ↦ ?_)
  · rw [ciSup_le_iff' H]
    exact fun a ↦ succ_le_of_lt a.2
  · rw [lt_ciSup_iff' H]
    exact ⟨⟨y, hy⟩, lt_succ_of_not_isMax hy.not_isMax⟩

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
z : α
hy : f z ∉ Set.range ⇑f
hs : s (f z) x
⊢ ∃ a, f a = x

Tactic:
cases hy (Set.mem_range_self z)

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

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

Tactic:
simp only [Lex.sep, le_top]

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
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
⊢ b ∈ Set.range ⇑(ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯)

Tactic:
by
    obtain ⟨m, hm, hm'⟩ := H.wf.has_min { a | ¬s _ b } ⟨_, asymm h⟩
    use m
    obtain lt | rfl | gt := trichotomous_of s b (collapseF f m)
    · refine (collapseF_not_lt f m (fun c h ↦ ?_) lt).elim
      by_contra hn
      exact hm' _ hn h
    · rfl
    · exact (hm gt).elim

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ (a ∈ if h : o.Dom then Option.some (o.get h) else Option.none) ↔ a ∈ o

Tactic:
simp only [h, ↓reduceDIte, Option.mem_def, reduceCtorEq, false_iff]
    exact mt Exists.fst h

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x ↔ ∀ (i : ℕ), c i ≤ x

Tactic:
by
  constructor <;> intros
  · trans ωSup c
    · exact le_ωSup _ _
    · assumption
  exact ωSup_le _ _ ‹_›

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous (f ⊓ g)

Tactic:
by
  refine ωScottContinuous.of_monotone_map_ωSup
    ⟨hf.monotone.inf hg.monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩
  simp only [Pi.inf_apply, hf.map_ωSup c, hg.map_ωSup c, inf_le_iff, ωSup_le_iff, Chain.coe_map,
    Function.comp, OrderHom.coe_mk, ← forall_or_left, ← forall_or_right]
  exact ⟨fun h _ ↦ h _ _, fun h i j ↦
    (h (max j i)).imp (le_trans <| hf.monotone <| c.mono <| le_max_left _ _)
      (le_trans <| hg.monotone <| c.mono <| le_max_right _ _)⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
⊢ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x

pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
⊢ ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x

Tactic:
· intro b hb
    apply ωSup_le _ _ _
    rintro i y hy
    simp only [Part.mem_ωSup] at hb
    rcases hb with ⟨j, hb⟩
    replace hb := hb.symm
    simp only [Part.eq_some_iff, Chain.coe_map, Function.comp_apply] at hy hb
    replace hb : b ∈ f (c (max i j)) := f.mono (c.mono (le_max_right i j)) _ hb
    replace hy : y ∈ g (c (max i j)) b := g.mono (c.mono (le_max_left i j)) _ _ hy
    apply h''' (max i j)
    simp only [Part.mem_bind_iff, Chain.coe_map,
      Function.comp_apply, OrderHom.partBind_coe]
    exact ⟨_, hb, hy⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
⊢ ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
change #(ULift.{u} _) = #(ULift.{u} _) + 1
  rw [← mk_option]
  simp

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

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
this :
  #((i : ι) × ((Quotient.out ∘ f) i ⊕ (Quotient.out ∘ g) i)) =
    #((i : ι) × (Quotient.out ∘ f) i ⊕ (i : ι) × (Quotient.out ∘ g) i)
⊢ sum (f + g) = sum f + sum g

Tactic:
simp only [comp_apply, mk_sigma, mk_sum, mk_out, lift_id] at this

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
this : (sum fun i ↦ f i + g i) = (sum fun i ↦ f i) + sum fun i ↦ g i
⊢ sum (f + g) = sum f + sum g
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_mul, toENatAux_nat]

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

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬sSup s ≤ d
⊢ False

Tactic:
csSup_le_iff' hs

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬∀ x ∈ s, x ≤ d
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
ι : Type v
f : ι → Set α
⊢ (sum fun i ↦ #↑(f i)) = lift.{v, max u v} (sum fun i ↦ #↑(f i))

Tactic:
lift_id'.{_, u}

Goal state after:
α : Type u
ι : Type v
f : ι → Set α
⊢ (sum fun i ↦ #↑(f i)) = sum fun i ↦ #↑(f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ #↑(f ⁻¹' s) ≤ #↑s

Tactic:
by
  rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
  exact mk_preimage_of_injective_lift f s h

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

Goal state before:
pp: α : Type u
β : Type v
⊢ #↑(range Sum.inr) = lift.{u, v} #β

Tactic:
rw [← lift_id'.{v, u} #_, (Equiv.Set.rangeInr α β).lift_cardinal_eq, lift_umax.{v, u}]

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

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

Tactic:
← power_zero

Goal state after:
a : Cardinal.{u_1}
h : a ≠ 0
⊢ ?m.23 ^ 0 ≤ 0 ^< a

a : Cardinal.{u_1}
h : a ≠ 0
⊢ Cardinal.{u_1}
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
h : f ∘ₛₗ ↑e₁₂ = g ∘ₛₗ ↑e₁₂
⊢ f = (f ∘ₛₗ ↑e₁₂) ∘ₛₗ ↑e₁₂.symm

Tactic:
eq_comp_toLinearMap_symm

Goal state after:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
h : f ∘ₛₗ ↑e₁₂ = g ∘ₛₗ ↑e₁₂
⊢ f ∘ₛₗ ↑e₁₂ = f ∘ₛₗ ↑e₁₂
Module: Mathlib.Algebra.Module.Submodule.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
N : Submodule R M
ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ x ∉ N

Tactic:
intro hx

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
N : Submodule R M
ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
hx : x ∈ N
⊢ False
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
⊢ map f p ≤ map f q ∧ map f p ≠ map f q ↔ p ≤ q ∧ p ≠ q

Tactic:
map_le_map_iff_of_injective hf,

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
⊢ p ≤ q ∧ map f p ≠ map f q ↔ p ≤ q ∧ p ≠ q
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ e.symm x ∈ p → ∃ y ∈ p, ↑e y = x

Tactic:
intro hx

Goal state after:
case mpr
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
hx : e.symm x ∈ p
⊢ ∃ y ∈ p, ↑e y = x
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ x ∈ map (↑e) p ↔ e.symm x ∈ p

Tactic:
by
  rw [Submodule.mem_map]; constructor
  · rintro ⟨y, hy, hx⟩
    simp [← hx, hy]
  · intro hx
    exact ⟨e.symm x, hx, by simp⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -↑n * (x✝¹ * x✝) = -x✝¹ * x✝ + -↑n * x✝¹ * x✝

Tactic:
← neg_mul,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -x✝¹ * x✝ + -↑n * (x✝¹ * x✝) = -x✝¹ * x✝ + -↑n * x✝¹ * x✝
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
a : R
⊢ a ∈ Set.center R ↔
    AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
      AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
        AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)

Tactic:
by
  rw [Set.mem_center_iff, isMulCentral_iff]
  simp [DFunLike.ext_iff, commute_iff_eq]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ x ∈ closure s → ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
intro hx

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ closure s
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s t : Subsemiring R
g : S → R
f : R →+* S
h : Function.LeftInverse g ⇑f
x : ↥f.rangeS
x' : R
hx' : f x' = ↑x
⊢ ↑((fun x ↦ f.rangeSRestrict x) ((fun x ↦ (g ∘ ⇑f.rangeS.subtype) x) x)) = ↑x

Tactic:
simp [← hx', h x']

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

Goal state before:
pp: case succ
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a ^ (n + 1)
⊢ p ∣ a

Tactic:
rw [pow_succ'] at h
    rcases dvd_or_dvd hp h with dvd_a | dvd_pow
    · assumption
    · exact ih dvd_pow

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

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
← u⁻¹.isUnit_mul_units B

Goal state after:
case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ IsUnit A ∨ IsUnit (B * ↑u⁻¹)