mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n.succ
⊢ ∃ a s', s = a ::ₛ s'

Tactic:
by
  obtain ⟨a, ha⟩ := exists_mem s
  classical exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
⊢ C v w

Tactic:
induction n with
  | zero =>
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  | succ n ih =>
    rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
    cases v_property
    rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
    cases w_property
    apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩
    apply ih

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

Goal state before:
pp: ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
⊢ #s ^ (#univ - 1) = #s ^ (card ι - 1)

Tactic:
card_univ

Goal state after:
ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
⊢ #s ^ (card ι - 1) = #s ^ (card ι - 1)
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
⊢ ∏ j ∈ univ.erase i, #s = #s ^ (card ι - 1)

Tactic:
rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ filter (fun x ↦ a ≠ x) ↑(replicate (↑m.fst) a) = 0

pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1

Tactic:
eq_zero_iff_forall_notMem

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ (a_1 : α), a_1 ∉ filter (fun x ↦ a ≠ x) ↑(replicate (↑m.fst) a)

α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
j : κ
⊢ (if j ∈ s then #s ^ (#univ - 1) else 0) = if j ∈ s then #s ^ (card ι - 1) else 0

Tactic:
card_univ

Goal state after:
ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
j : κ
⊢ (if j ∈ s then #s ^ (card ι - 1) else 0) = if j ∈ s then #s ^ (card ι - 1) else 0
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
j : κ
⊢ (if j ∈ s then ∏ b ∈ univ.erase i, #s else 0) = if j ∈ s then #s ^ (card ι - 1) else 0

Tactic:
rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

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

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j

Tactic:
get_set_of_ne

Goal state after:
case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ v.get j = v.get j

case neg.h
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ i ≠ j
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
⊢ ∀ (a : α ⊕ β), ¬LiftRel r s a a

Tactic:
rintro _ (⟨h⟩ | ⟨h⟩)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
a✝ : α
h : r a✝ a✝
⊢ False

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
b✝ : β
h : s b✝ b✝
⊢ False
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
⊢ ∀ (a : α ⊕ β), ¬Lex r s a a

Tactic:
rintro _ (⟨h⟩ | ⟨h⟩)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
a₁✝ : α
h : r a₁✝ a₁✝
⊢ False

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
b₁✝ : β
h : s b₁✝ b₁✝
⊢ False
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit (sSup ∅)

Tactic:
csSup_empty

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit ⊥
Module: Mathlib.Data.Sum.Order

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

Tactic:
· simp only [elim_inl, lex_inr_inr, coe_le_coe]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case 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
⊢ (fun x ↦ (f x, g x)) a ∈ lowerBounds {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x}

Tactic:
intro ⟨p₁, p₂⟩ hp

Goal state after:
case 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 : (p₁, p₂) ∈ {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x}
⊢ (fun x ↦ (f x, g x)) a ≤ (p₁, p₂)
Module: Mathlib.Data.Part

Goal state before:
pp: case mpr
α : Type u_1
x : α
⊢ some x ≠ none

Tactic:
apply some_ne_none

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
a b : Part α
ha : a.Dom
hb : a.get ha ∈ b
⊢ a = b

Tactic:
by
  have hb' : b.Dom := Part.dom_iff_mem.mpr ⟨a.get ha, hb⟩
  rwa [← eq_get_iff_mem hb', eq_iff_of_dom ha hb'] at hb

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Option α
⊢ (↑o).toOption = o

Tactic:
cases o <;> rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : 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
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption

Tactic:
by_cases h : o.Dom
  · simp_rw [h.toOption, h.bind]
    rfl
  · rw [Part.toOption_eq_none_iff.2 h]
    exact Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind

Goal state after:
Module: Mathlib.Data.Part

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

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

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
h : ∀ z ∈ c, z ≤ y
⊢ cSup c ≤ y

Tactic:
apply cSup_le c y h

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:
exact h.succ

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : a ≤ b
⊢ ∃ s, a ∈ s ∧ b ∈ s

Tactic:
by
  simpa [Set.insert_subset_iff] using (IsChain.pair hab).exists_subset_flag

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

Goal state before:
pp: α : 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 β
s t : Set α
hst : s ⊆ t
⊢ (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ

Tactic:
gcongr

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

Goal state before:
pp: m : ℕ∞
⊢ 0 = m ↔ m = 0

Tactic:
apply eq_comm

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

Goal state before:
pp: m : ℕ∞
⊢ 1 = m ↔ m = 1

Tactic:
apply eq_comm

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

Goal state before:
pp: α : Type u
s : Set α
⊢ #↑(ULift.down ⁻¹' s) = lift.{v, u} #↑s

Tactic:
rw [← mk_uLift, Cardinal.eq]

Goal state after:
α : Type u
s : Set α
⊢ Nonempty (↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s)
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M α
inst✝¹ : MulAction N α
inst✝ : SMulCommClass M N α
x y : M × N
a : α
⊢ (x * y) • a = x • y • a

Tactic:
change (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
    rw [mul_smul, mul_smul, smul_comm y.1 x.2]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x y : M
hxy : (fun x ↦ s • x) x = (fun x ↦ s • x) y
⊢ IsRegular (s • 1)

Tactic:
exact ⟨fun x y hxy ↦ hs.isSMulRegular <| by simpa using hxy,
      fun x y hxy ↦ hs.isSMulRegular <| by simpa using hxy⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Injective ⇑(f' ^ n)
⊢ Injective ⇑f'

Tactic:
rw [← Nat.succ_pred_eq_of_pos (show 0 < n by lia), iterate_succ, coe_comp] at h
  exact h.of_comp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
⊢ g ^ k = 0

Tactic:
ext m
  have hg : N.subtype.comp (g ^ k) m = 0 := by
    rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]
  simpa using hg

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 : (f ^ n) x = 0
c : ℕ
w : n ≤ n + c
⊢ (f ^ c * f ^ n) x = 0

Tactic:
Module.End.mul_apply,

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
⊢ (f ^ c) ((f ^ n) x) = 0
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 m : ℕ
w : n ≤ m
x : M
h : x ∈ (fun n ↦ (f ^ n).ker) n
⊢ x ∈ (fun n ↦ (f ^ n).ker) m

Tactic:
obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le w
    rw [LinearMap.mem_ker] at h
    rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, map_zero]

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✝⁹ : 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 σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
⊢ ∀ (m : R) (x : ↥p), (Equiv.Set.image (⇑f) (↑p) i).toFun (m • x) = σ₁₂ m • (Equiv.Set.image (⇑f) (↑p) i).toFun x

Tactic:
intros
      -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `map_smulₛₗ` into `map_smulₛₗ _`
      simp only [coe_smul_of_tower, map_smulₛₗ _, Equiv.toFun_as_coe, Equiv.Set.image_apply]
      rfl

Goal state after:
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 : Surjective ⇑f
p q : Submodule R₂ M₂
⊢ comap f p < comap f q ↔ p < q

Tactic:
by
  apply lt_iff_lt_of_le_iff_le' <;> exact comap_le_comap_iff_of_surjective hf

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✝¹⁰ : 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 σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x✝ : M
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
S : Submodule R M
x y : M
hy : y ∈ S
hxy : y = x
⊢ x ∈ S

Tactic:
rwa [← hxy]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ i, ↑(S i)
i : ι
hi : x₂ ∈ ↑(S i)
⊢ C x₂

Tactic:
exact mem _ _ hi

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

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * (x✝ * a) + x✝¹ * (x✝ * b) = x✝¹ * (x✝ * (a + b))

Tactic:
← mul_add,

Goal state after:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * (x✝ * a + x✝ * b) = x✝¹ * (x✝ * (a + b))
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type ?u.4
S : Type ?u.6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
M : Type ?u.13
N : Type ?u.15
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
h : Surjective ⇑(algebraMap R S)
f : M →ₗ[R] N
r : S
x : M
⊢ f.toFun (r • x) = (RingHom.id S) r • f.toFun x

Tactic:
by obtain ⟨r, rfl⟩ := h r; simp

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

Goal state before:
pp: R : Type ?u.4
S : Type ?u.6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
M : Type ?u.13
N : Type ?u.15
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
h : Surjective ⇑(algebraMap R S)
f : M ≃ₗ[R] N
r : S
x : M
⊢ (↑f).toFun (r • x) = (RingHom.id S) r • (↑f).toFun x

Tactic:
by obtain ⟨r, rfl⟩ := h r; simp

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
⊢ Associated = Eq

Tactic:
by
  ext
  rw [associated_iff_eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
⊢ Associates.mk a = 1 ↔ IsUnit a

Tactic:
by
  rw [← mk_one, mk_eq_mk_iff_associated, associated_one_iff_isUnit]

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

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
N : Type u_9
inst✝⁸ : CommSemiring 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₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
⊢ ∀ (m : R) (x : M₁), ↑e ∘ₗ codRestrict i.range (f (m • x)) ⋯ = (RingHom.id R) m • ↑e ∘ₗ codRestrict i.range (f x) ⋯

Tactic:
by intro t x; ext y; simp [f.map_smul, ← e.map_smul, codRestrict]

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

Goal state before:
pp: case mem
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
s : Set M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
t : Set N
p : (x : M) → (y : N) → x ∈ span R s → y ∈ span R t → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : y ∈ span R t), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : x ∈ span R s), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : x ∈ span R s) (hy : y ∈ span R s) (hz : z ∈ span R t),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : x ∈ span R s) (hy : y ∈ span R t) (hz : z ∈ span R t),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : a ∈ span R s
z : N
hz : z ∈ t
⊢ p a z ha ⋯

Tactic:
induction ha using span_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h

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
s : Set M
x : M
hx : x ∈ closure (univ • s)
⊢ univ • s ⊆ ↑(span R s).toAddSubmonoid

Tactic:
rintro - ⟨r, -, x, hx, rfl⟩

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : M
hx✝ : x✝ ∈ closure (univ • s)
r : R
x : M
hx : x ∈ s
⊢ (fun x1 x2 ↦ x1 • x2) r x ∈ ↑(span R s).toAddSubmonoid
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
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : x ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
⊢ ∀ (x : M) (h : x ∈ univ • s), p x ⋯

Tactic:
rintro - ⟨r, -, x, hx, rfl⟩

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x✝ : M
hx✝ : x✝ ∈ span R s
key : ∀ {v : M}, v ∈ span R s ↔ v ∈ closure (univ • s)
r : R
left✝ : r ∈ univ
x : M
hx : x ∈ s
⊢ p ((fun x1 x2 ↦ x1 • x2) r x) ⋯
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
s t : Set M
hst : Disjoint (span R s) (span R t)
h0s : 0 ∉ s
⊢ Disjoint s t

Tactic:
rw [← sdiff_singleton_eq_self h0s]
  exact hst.of_span

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s t : Set α
a b : α
⊢ ∀ ⦃x y : Set α⦄, x ⊆ y → SupClosed y → {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ x ∧ t.sup' ht id = a} ⊆ y

Tactic:
by rintro s₁ s₂ hs h₂ _ ⟨t, ht, hts, rfl⟩; exact h₂.finsetSup'_mem ht fun i hi ↦ hs <| hts hi

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊤

Tactic:
exact le_top

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ s
⊢ (if ⊥ ∈ s then ⊥ else ⊤) ≤ ⊤

Tactic:
exact le_top

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
rw [← sSup_image]
  exact hs.sSup_mem (ht.image _) hbot (by simpa)

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)

Tactic:
split_ifs with has

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∈ s
⊢ r (f a) (g a)

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : ¬a ∈ s
⊢ r 1 1
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
a : List α
l : List (List α)
⊢ ((↑(List.map (fun l ↦ ↑l) l.sections)).bind fun b ↦ map (fun a ↦ a ::ₘ b) ↑a) =
    ↑(List.map (fun l ↦ ↑l) (List.flatMap (fun s ↦ List.map (fun a ↦ a :: s) a) l.sections))

Tactic:
simp [Function.comp_def, List.flatMap]

Goal state after: