mathlib-initiative/mathlib-tactics huggingface dataset:
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 x).2 = g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).1

Tactic:
rw [← g.map_mul]

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 * ↑(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)
x y : N
⊢ g ((f.sec (x * y)).1 * ↑(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

Tactic:
rw [← g.map_mul]

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 * ↑(f.sec y).2 * ↑(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)
x y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).1

Tactic:
rw [← g.map_mul]

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 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(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)
x y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(f.sec (x * y)).2) * g (f.sec x).1

Tactic:
rw [← g.map_mul]

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 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(f.sec (x * y)).2 * (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)
x y : N
⊢ g ((f.sec (x * y)).1 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(f.sec (x * y)).2 * (f.sec x).1)

Tactic:
rw [← g.map_mul]

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 * ↑(f.sec y).2 * ↑(f.sec x).2) = g ((f.sec y).1 * ↑(f.sec (x * y)).2 * (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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
⊢ z = w

Tactic:
have ⟨z', w', x, hxz, hxw⟩ := surj₂ f z w

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
or : Set.SurjOn ⇑g ↑S ↑T ∨ Injective ⇑k
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
⊢ z = w
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
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
r : R
x : OreLocalization S X
⊢ (r • 1 /ₒ 1) • x = r • x

Tactic:
rw [oreDiv_one_smul, smul_one_smul]

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

Goal state before:
pp: R : Type u_1
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
r : R
x : X
⊢ (r • 1 /ₒ 1) • (x /ₒ 1) = r • x /ₒ 1

Tactic:
smul_div_one,

Goal state after:
R : Type u_1
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
r : R
x : X
⊢ (r • 1) • x /ₒ 1 = r • x /ₒ 1
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
rcases lt_trichotomy (f x) (g x) with (H | H | H)

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x = g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
⊢ ¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a

Tactic:
by
  rw [isSuccLimit_iff, not_and_or, not_not]

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

Goal state before:
pp: α : Type u_2
β : α → Type u_1
inst✝¹ : Small.{w, u_2} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink.{w, u_1} (β ((equivShrink α).symm ((equivShrink α) a)))

Tactic:
simpa using equivShrink (β a)

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

Goal state before:
pp: α : Type u_2
β : α → Type u_1
inst✝¹ : Small.{w, u_2} α
inst✝ : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ β a ≃ Shrink.{w, u_1} (β ((equivShrink α).symm ((equivShrink α) a)))

Tactic:
simpa using equivShrink (β a)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → M
⊢ (∏ x ∈ s, if p x then f x else g x) = (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, g x

Tactic:
simp [prod_apply_ite _ _ fun x => x]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
⊢ (∏ x ∈ s, if p x then k (f x) else k (g x)) = ∏ x ∈ s, k (f x)

Tactic:
exact prod_ite_of_true h _ _

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ γ✝ : Type u_2
x✝² : AddConst α α✝
x✝¹ : AddConst α (α✝ → β✝)
x✝ : AddConst α (β✝ → γ✝)
⊢ x✝ <*> (x✝¹ <*> x✝²) = Function.comp <$> x✝ <*> x✝¹ <*> x✝²

Tactic:
simp [Const.map, map, Seq.seq, add_assoc]

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

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

Tactic:
classical
    let s' : Finset α := s.toFinset
    have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using! hfst
    have hfs' : Set.InjOn f s' := by simpa [s'] using! hfs
    obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
    refine ⟨g, fun i hi => ?_⟩
    apply hg
    simpa [s'] using! hi

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x ∈ v.toList

Tactic:
rw [← cons_head_tail v, toList_cons, List.mem_cons]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x = v.head ∨ x ∈ v.tail.toList
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ ((↑s).card = n ∧ ∀ b ∈ ↑s, b = a) ↔ ∀ b ∈ s, b = a

Tactic:
exact and_iff_right s.2

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

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
⊢ ∀ (a b : Sym α (n✝ + 1)), a = b

Tactic:
intro s

Goal state after:
case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
s : Sym α (n✝ + 1)
⊢ ∀ (b : Sym α (n✝ + 1)), s = b
Module: Mathlib.Data.Vector.Basic

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

Tactic:
rw [get_tail, get_ofFn]

Goal state after:
α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ f ⟨↑i + 1, ⋯⟩ = f i.succ
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤) ↔ ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤

Tactic:
by
  constructor
  · rintro ⟨s, hps, hs⟩
    refine ⟨range s, countable_range s, forall_mem_range.2 hps, ?_⟩
    rwa [sSup_range]
  · rintro ⟨S, hSc, hps, hS⟩
    rcases eq_empty_or_nonempty S with (rfl | hne)
    · rw [sSup_empty] at hS
      have := subsingleton_of_bot_eq_top hS
      rcases h with ⟨x, hx⟩
      exact ⟨fun _ => x, fun _ => hx, Subsingleton.elim _ _⟩
    · rcases (Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩
      refine ⟨fun n => s n, fun n => hps _ (s n).coe_prop, ?_⟩
      rwa [hs.iSup_comp, ← sSup_eq_iSup']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
⊢ ∃ b, b < a

Tactic:
obtain ⟨b | b, h⟩ := exists_lt (inr a : α ⊕ β)

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
b : α
h : inl b < inr a
⊢ ∃ b, b < a

case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : β
h : inr b < inr a
⊢ ∃ b, b < a
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b

Tactic:
exact Lex.sep _ _

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

Goal state before:
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.sep _ _

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✝¹ : LE β
inst✝ : OrderTop β
a : α
⊢ inl a ≤ inr ⊤

Tactic:
exact Lex.sep _ _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
⊢ s.Nonempty → ¬BddAbove s

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩
  obtain ⟨c, hc⟩ := exists_gt b
  exact hc.not_ge (hb <| hs ((hb ha).trans hc.le) ha)

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
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (f.transPrincipal g).toRelEmbedding a = g.toRelEmbedding (f a)

Tactic:
InitialSeg.transPrincipal

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (match f.principalSumRelIso with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption

Tactic:
simp_rw [h.toOption, h.bind]
    rfl

Goal state after:
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
constructor
        · exact (bot_isAdmissible le_map).base_isLeast.1
        · exact Or.inl ((bot_isAdmissible le_map).base_isLeast.2 hy.mem_bot)

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ lfp f

Tactic:
· apply le_lfp
    intro a h_a
    exact ωSup_iterate_le_prefixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le h_a bot_le

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ
α : Type u_1
r : α → α → Prop
c s✝ : Set α
a✝ : ChainClosure r s✝
h : IsChain r s✝
⊢ IsChain r (SuccChain r s✝)

Tactic:
| succ _ h =>

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
z : α
hz : z ∈ bot x f
a✝ : y ≠ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y

Tactic:
rw [mem_bot_iff_isExtremePt le_map] at hy

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
a✝ : y ≠ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
i j : ℕ
⊢ j ≤ max i j

Tactic:
apply le_max_right

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

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))

Tactic:
← Quot.out_eq (f i),

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : Quot.mk (⇑isEquivalent) (Quot.out (f i)) ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))

Tactic:
rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this

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

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ toNat a = n ↔ ↑(toNat a) = ↑n

Tactic:
exact Nat.cast_inj.symm

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

Goal state before:
pp: case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x * y).toENatAux = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
rw [mul_comm, this y x (le_of_not_ge hle), mul_comm]

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

Goal state before:
pp: case refine_2
α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

pp: case refine_3
α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
· intro f
    rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]

Goal state after:
case refine_3
α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ 0)

Tactic:
rw [pow_zero]; simp only [one]

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

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

Tactic:
let hα := Fintype.ofFinite α

Goal state after:
case inl
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ ∃ s, n = s.card
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
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₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
σ₃₂ : R₃ →+* R₂
inst✝¹ : RingHomInvPair σ₂₃ σ₃₂
inst✝ : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
hf : ∃ f', f ∘ₛₗ f' = id
⊢ Surjective fun g ↦ f ∘ₛₗ g

Tactic:
by
  intro h
  obtain ⟨f', hf'⟩ := hf
  refine ⟨f'.comp h, ?_⟩
  simp_rw [← comp_assoc, hf', id_comp]

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'
S' : Type u_6
T' : Type u_7
inst✝⁵ : Monoid S'
inst✝⁴ : DistribMulAction S' M
inst✝³ : SMulCommClass R S' M
inst✝² : Monoid T'
inst✝¹ : DistribMulAction T' M
inst✝ : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
c : R
x : M
⊢ (a • ⇑f) (c • x) = σ₁₂ c • (a • ⇑f) x

Tactic:
DomMulAct.smul_apply,

Goal state after:
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'
S' : Type u_6
T' : Type u_7
inst✝⁵ : Monoid S'
inst✝⁴ : DistribMulAction S' M
inst✝³ : SMulCommClass R S' M
inst✝² : Monoid T'
inst✝¹ : DistribMulAction T' M
inst✝ : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
c : R
x : M
⊢ f (DomMulAct.mk.symm a • c • x) = σ₁₂ c • f (DomMulAct.mk.symm a • x)
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
r : R
c : M
⊢ Exists.choose ⋯ = σ₁₂ r • Exists.choose ⋯

Tactic:
by apply hp; simp_rw [map_smul, (h _).choose_spec, map_smulₛₗ]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
⊢ f ⊥ = ⊥

Tactic:
← sSup_empty,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
⊢ f (sSup ∅) = ⊥
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
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₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ N ≤ f.ker ↔ f ∘ₛₗ N.subtype = 0

Tactic:
rw [SetLike.le_def, LinearMap.ext_iff, Subtype.forall]; rfl

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝³ : Semiring R
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y : ↥(Submodule.map (↑e) p)
⊢ (LinearMap.codRestrict (Submodule.map (↑e) p) ((↑e).domRestrict p) ⋯).toFun ((fun y ↦ ⟨↑e.symm ↑y, ⋯⟩) y) = y

Tactic:
by
      apply SetCoe.ext
      simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe,
        LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))
⊢ y ∈ ↑H.toAddSubmonoid

Tactic:
refine (Subsemigroup.mem_closure.mp hy) H.toSubsemigroup fun z hz => ?_

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubsemigroup
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
x✝ : IsUnit q
v : Mˣ
hv : ↑v = q
⊢ ↑(v * u⁻¹) = p

Tactic:
by simp [hv, hu.symm]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : a ~ᵤ b
u : Mˣ
hu : a * ↑u = b
x✝ : IsUnit a
v : Mˣ
hv : ↑v = a
⊢ ↑(v * u) = b

Tactic:
by simp [hv, hu.symm]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
u : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ q = p * x
⊢ q * ↑u = p * x * ↑u

Tactic:
← hx.right

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
u : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ q = p * x
⊢ q * ↑u = q * ↑u