mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝² : Fintype α
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
⊢ ∏ i, f i = f a * ∏ i, f ↑i

Tactic:
← (Equiv.optionSubtypeNe a).prod_comp,

Goal state after:
α : Type u_1
M : Type u_4
inst✝² : Fintype α
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
⊢ ∏ i, f ((Equiv.optionSubtypeNe a) i) = f a * ∏ i, f ↑i
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
v_property : [].length = n + 1
⊢ C ⟨[], v_property⟩

pp: case succ.cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
a : α
v : List α
v_property : (a :: v).length = n + 1
⊢ C ⟨a :: v, v_property⟩

Tactic:
cases v_property

Goal state after:
case succ.cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
a : α
v : List α
v_property : (a :: v).length = n + 1
⊢ C ⟨a :: v, v_property⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.cons
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
a : α
v : List α
v_property : (a :: v).length = n + 1
⊢ C ⟨a :: v, v_property⟩

Tactic:
exact cons (ih ⟨v, (add_left_inj 1).mp v_property⟩)

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

Goal state before:
pp: case succ.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (n + 1)
v_property : [].length = n + 1
⊢ C ⟨[], v_property⟩ w

pp: case succ.cons
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (n + 1)
a : α
v : List α
v_property : (a :: v).length = n + 1
⊢ C ⟨a :: v, v_property⟩ w

Tactic:
cases v_property

Goal state after:
case succ.cons
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (n + 1)
a : α
v : List α
v_property : (a :: v).length = n + 1
⊢ C ⟨a :: v, v_property⟩ w
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.cons.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
v_property : [].length = n + 1
⊢ C ⟨a :: u, u_property⟩ ⟨[], v_property⟩ w

pp: case succ.cons.cons
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
⊢ C ⟨a :: u, u_property⟩ ⟨b :: v, v_property⟩ w

Tactic:
cases v_property

Goal state after:
case succ.cons.cons
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (n + 1)
a : α
u : List α
u_property : (a :: u).length = n + 1
b : β
v : List β
v_property : (b :: v).length = n + 1
⊢ C ⟨a :: u, u_property⟩ ⟨b :: v, v_property⟩ w
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List β
⊢ map (⇑e ∘ ⇑e.symm) l = l

Tactic:
e.self_comp_symm,

Goal state after:
α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List β
⊢ map id l = l
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∏ i, c i = ∏ i ∈ range n, if h : i < n then c ⟨i, h⟩ else 1

Tactic:
rw [← Fin.prod_univ_eq_prod_range, Finset.prod_congr rfl]
  rintro ⟨i, hi⟩ _
  simp only [hi, dif_pos]

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

Goal state before:
pp: case cons
α : Type u
x : α
xs : List α
IH : traverseAux pure xs = pure ⟨xs, ⋯⟩
⊢ traverseAux pure (x :: xs) = pure ⟨x :: xs, ⋯⟩

Tactic:
simp! [IH]

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)
⊢ sSup s ∈ s

Tactic:
· have ⟨y, hy⟩ := not_forall_not.mp hlim
    have ⟨i, his, hi⟩ := exists_lt_of_lt_csSup hne hy.lt
    exact eq_of_le_of_not_lt (le_csSup hbdd his) (hy.2 hi) ▸ his

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

Goal state before:
pp: ι : Type u
a : Cardinal.{v}
f : ι → Cardinal.{v}
⊢ lift.{u, v} a ^ sum f = prod fun i ↦ a ^ f i

Tactic:
induction a using Cardinal.inductionOn with | _ α =>
  induction f using induction_on_pi with | _ f =>
  simp_rw [← mk_uLift, prod, sum, power_def]
  apply mk_congr
  refine (Equiv.piCurry fun _ _ => ULift α).trans ?_
  refine Equiv.piCongrRight fun b => ?_
  refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_
  exact outMkEquiv.symm

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

Goal state before:
pp: α : 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 : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ {a b : α₁ ⊕ₗ β₁},
    (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) a ≤ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) b ↔ a ≤ b

Tactic:
by simp_rw [Lex.forall]; rintro (a | a) (b | b) <;> simp

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
p : Set β
f : r ≺i s
H : ∀ (a : α), f.toRelEmbedding a ∈ p
H₂ : f.top ∈ p
x✝ : { x // x ∈ p }
val✝ : β
property✝ : val✝ ∈ p
⊢ ⟨val✝, property✝⟩ ∈ Set.range ⇑(RelEmbedding.codRestrict p f.toRelEmbedding H) ↔
    Subrel s (fun x ↦ x ∈ p) ⟨val✝, property✝⟩ ⟨f.top, H₂⟩

Tactic:
simp [← f.mem_range_iff_rel]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
h : b ≤ f a
c : α
hc : f c = b
⊢ c ≤ a

Tactic:
← hc,

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
c : α
h : f c ≤ f a
hc : f c = b
⊢ c ≤ a
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
h : b < f a
c : α
hc : f c = b
⊢ c < a

Tactic:
← hc,

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
c : α
h : f c < f a
hc : f c = b
⊢ c < a
Module: Mathlib.Order.Part

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
β γ : Type u_4
f : α → Part (β → γ)
g : α → Part β
hf : Monotone f
hg : Monotone g
⊢ Monotone fun x ↦ f x <*> g x

Tactic:
by
  simpa only [seq_eq_bind_map] using! hf.partBind <| Monotone.of_apply₂ fun _ ↦ hg.partMap

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x ↦ (f x, g x)) a).1 ≤ (p₁, p₂).1

pp: case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x ↦ (f x, g x)) a).2 ≤ (p₁, p₂).2

Tactic:
· rw [isLUB_le_iff (hf hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_ofPred_eq]
      intro _ hb
      exact (hp _ hb).1

Goal state after:
case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x ↦ (f x, g x)) a).2 ≤ (p₁, p₂).2
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ (a / b).get hab = a.get ⋯ / b.get ⋯

Tactic:
by
  simp [div_def]; aesop

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

Goal state before:
pp: case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])

Goal state after:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) → IsSMulRegular M a

Tactic:
← Nat.succ_pred_eq_of_pos n0,

Goal state after:
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n.pred.succ) → IsSMulRegular M a
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{u}
⊢ sum f ≤ #ι * ⨆ i, f i

Tactic:
by
  simpa using sum_le_lift_mk_mul_iSup_lift f

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a * b < ℵ₀ ↔ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · by_cases ha : a = 0
    · exact Or.inl ha
    right
    by_cases hb : b = 0
    · exact Or.inl hb
    right
    rw [← Ne, ← Cardinal.one_le_iff_ne_zero] at ha hb
    constructor
    · rw [← mul_one a]
      exact (mul_le_mul' le_rfl hb).trans_lt h
    · rw [← one_mul b]
      exact (mul_le_mul' ha le_rfl).trans_lt h
  rintro (rfl | rfl | ⟨ha, hb⟩) <;> simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]

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

Goal state before:
pp: α : Type u
A : Set (Set α)
⊢ #↑(⋃ i, ↑i) ≤ #↑A * ⨆ s, #↑↑s

Tactic:
apply mk_iUnion_le

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

Goal state before:
pp: ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ x, A ↑x) ≤ #↑s * ⨆ x, #↑(A ↑x)

Tactic:
apply mk_iUnion_le

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

Goal state before:
pp: α : Type u
s : Set α
⊢ Subsingleton ↑s ∧ Nonempty ↑s ↔ s.Nonempty ∧ s.Subsingleton

Tactic:
Set.nonempty_coe_sort,

Goal state after:
α : Type u
s : Set α
⊢ Subsingleton ↑s ∧ s.Nonempty ↔ s.Nonempty ∧ s.Subsingleton
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ Function.Injective fun a ↦ n • a

Tactic:
simp_rw [← Nat.cast_smul_eq_nsmul R]

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ Function.Injective fun a ↦ ↑n • a
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
carrier : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier.carrier → c • x ∈ carrier.carrier
⊢ { toAddSubmonoid := carrier, smul_mem' := smul_mem' } = ⊥ ↔ carrier = ⊥

Tactic:
simp [← toAddSubmonoid_inj]

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
carrier : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier.carrier → c • x ∈ carrier.carrier
⊢ { toAddSubmonoid := carrier, smul_mem' := smul_mem' } = ⊤ ↔ carrier = ⊤

Tactic:
simp [← toAddSubmonoid_inj]

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

Goal state before:
pp: case e'_2
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ e (c • a) = e.toAddMonoidHom (c • a)

Tactic:
exact congr(e $(int_smul_eq_zsmul ..))

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ⊔ g.ker ≤ (f ∘ₗ g).ker

Tactic:
by
  refine sup_le_iff.mpr ⟨?_, ker_le_ker_comp g f⟩
  rw [← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp]
  exact ker_le_ker_comp f g

Goal state after:
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✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ f.ker ≤ (c • f).ker

Tactic:
simpa only [ker] using Submodule.comap_le_comap_smul _ _ _

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
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 σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomSurjective σ₁₂
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomSurjective σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R M
⊢ ↑(map (g ∘ₛₗ f) p) = ↑(map g (map f p))

Tactic:
simp only [← image_comp, map_coe, LinearMap.coe_comp, comp_apply]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
S : NonUnitalSubsemiring R
⊢ S.toAddSubmonoid = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

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

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

Tactic:
(natCast_mem_center _ n).left_assoc _ _,

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
S : NonUnitalSubring R
⊢ S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
S : NonUnitalSubring R
⊢ S.toAddSubgroup = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : Subring R
⊢ S.toSubsemiring = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : Subring R
⊢ S.toAddSubgroup = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : CommMonoidWithZero M
inst✝² : CommMonoidWithZero N
p : M
E : Type u_5
inst✝¹ : EquivLike E M N
inst✝ : MulEquivClass E M N
e✝ : E
e : M ≃* N := ↑e✝
⊢ Prime (e✝ p) ↔ Prime p

Tactic:
exact ⟨comap_prime e e.symm fun a => by simp,
    fun h => (comap_prime e.symm e fun a => by simp) <| (e.symm_apply_apply p).substr h⟩

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
q : Submodule R₂ M₂
h : q ≤ f.range
⊢ map f (comap f q) = q

Tactic:
Submodule.map_comap_eq,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
q : Submodule R₂ M₂
h : q ≤ f.range
⊢ f.range ⊓ q = q
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b

Tactic:
rw [inf_comm, sup_comm]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ a → b ⊓ a ⋖ b → b ⋖ b ⊔ a
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Tactic:
by
  refine and_congr_right fun _ ↦ forall_congr' fun H ↦ ?_
  contrapose!
  rw [lt_iff_le_not_ge, lt_iff_le_and_ne, and_and_and_comm]
  simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ ∃ a, a • y = x

Tactic:
by
    refine span_induction ?_ ?_ ?_ ?_ h
    · rintro y (rfl | ⟨⟨_⟩⟩)
      exact ⟨1, by simp⟩
    · exact ⟨0, by simp⟩
    · rintro _ _ - - ⟨a, rfl⟩ ⟨b, rfl⟩
      exact ⟨a + b, by simp [add_smul]⟩
    · rintro a _ - ⟨b, rfl⟩
      exact ⟨a * b, by simp [smul_smul]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
⊢ ⨆ i, p i = span R (⋃ i, ↑(p i))

Tactic:
simp_rw [← iSup_span, span_eq]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
i : ι
x✝³ : i ∈ s
t : Finset (β i)
x✝² : t ⊆ g i
j : β i
x✝¹ : j ∈ g i
x✝ : j ∉ t
this : Disjoint (f ⟨i, j⟩) ((image (fun b ↦ ⟨i, b⟩) t).sup f)
⊢ Disjoint ((fun b ↦ f ⟨i, b⟩) j) (t.sup fun b ↦ f ⟨i, b⟩)

Tactic:
simpa only [sup_image]

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Tactic:
tfae_have 1 → 2 := @WellFoundedGT.isSupFiniteCompact α _
  tfae_have 2 → 3 := IsSupFiniteCompact.isSupClosedCompact α
  tfae_have 3 → 1 := IsSupClosedCompact.wellFoundedGT α
  tfae_have 2 ↔ 4 := isSupFiniteCompact_iff_all_elements_compact α
  tfae_finish

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

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ b = ⊥

Tactic:
← sSup_compact_le_eq b,

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ sSup {c | IsCompactElement c ∧ c ≤ b} = ⊥
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
⊢ motive f

Tactic:
suffices ∀ (s) (f : ι →₀ M), f.support = s → motive f from this _ _ rfl

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
⊢ ∀ (s : Finset ι) (f : ι →₀ M), f.support = s → motive f
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
G : Type u_6
H : Type u_7
inst✝¹ : NegZeroClass G
inst✝ : NegZeroClass H
f : G → H
hf : f 0 = 0
hf' : ∀ (x : G), f (-x) = -f x
v : ι →₀ G
x✝ : ι
⊢ (mapRange f hf (-v)) x✝ = (-mapRange f hf v) x✝

Tactic:
by simp only [hf', neg_apply, mapRange_apply]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
⊢ s.indicator (fun a ↦ r a • f a) a = s.indicator r a • f a

Tactic:
dsimp only [indicator]
  split_ifs
  exacts [rfl, (zero_smul _ (f a)).symm]

Goal state after: