mathlib-initiative/mathlib-tactics huggingface dataset:
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
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'

Goal state after:
α : 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
s' : Finset α := s.toFinset
hfst' : Finset.image f s' ⊆ t
hfs' : InjOn f ↑s'
g : α ≃ ↥t
hg : ∀ i ∈ s', ↑(g i) = f i
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (0 + 1)
i : Fin (0 + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
have i0 : i = 0 := Fin.eq_zero _

Goal state after:
case succ.zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (0 + 1)
i : Fin (0 + 1)
i0 : i = 0
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
s : (i : ι) → Finset (α i)
⊢ #(piFinset s) = ∏ i, #(s i)

Tactic:
simp [piFinset, card_map]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList.prod = (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod

Tactic:
refine (List.prod_set v.toList i a).trans ?_

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ ((List.take (↑i) v.toList).prod * if ↑i < v.toList.length then a else 1) * (List.drop (↑i + 1) v.toList).prod =
    (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod
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 : α
⊢ (match f.principalSumRelIso with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

Tactic:
obtain f' | f' := f.principalSumRelIso

Goal state after:
case inl
α : 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' : r ≺i s
⊢ (match Sum.inl f' with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

case inr
α : 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' : r ≃r s
⊢ (match Sum.inr f' with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ⇑(⨅ i, f i) = ⨅ i, ⇑(f i)

Tactic:
funext x; simp [iInf_apply]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ScottContinuousOn univ (g ∘ f)

Tactic:
exact ScottContinuousOn.comp (by simp) (by simp [MapsTo]) hg hf

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case inl
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y ∨ y ≤ none

Tactic:
left

Goal state after:
case inl
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy✝ : z ≤ y
hzy : z < y
⊢ f z ≤ y ∨ f y ≤ f z

Tactic:
left

Goal state after:
case image_self_subset_self.inl.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy✝ : z ≤ y
hzy : z < y
⊢ f z ≤ y
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 ∨ f y ≤ cSup c

Tactic:
left

Goal state after:
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
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
⊢ c₃ ∈ s✝ → ¬c₃ ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s✝ → False

Tactic:
hc₃

Goal state after:
case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
⊢ ¬c₃ ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s✝ → False
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
⊢ ∃ m, x ≤ m ∧ IsMax m

Tactic:
let ⟨m, hxm, ham, hm⟩ := zorn_le_nonempty₀ (Ici a) (fun c hca hc y hy ↦ ?_) x hax

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
m : α
hxm : x ≤ m
ham : (fun x ↦ x ∈ Ici a) m
hm : ∀ ⦃y : α⦄, (fun x ↦ x ∈ Ici a) y → m ≤ y → y ≤ m
⊢ ∃ m, x ≤ m ∧ IsMax m

case refine_1
α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
c : Set α
hca : c ⊆ Ici a
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union.inr.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False

Tactic:
exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsAdmissible x f {y | IsExtremePt x f y}

Tactic:
by
  apply IsAdmissible.mk
  · constructor
    · refine ⟨(bot_isAdmissible le_map).base_isLeast.1, ?_⟩
      intro y hy hyx
      exfalso
      exact lt_irrefl x (lt_of_le_of_lt ((bot_isAdmissible le_map).base_isLeast.2 hy) hyx)
    · exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1
  · rintro _ ⟨y, hy, rfl⟩
    refine ⟨map_mem_bot le_map hy.mem_bot, ?_⟩
    intro z hz hzy
    have hz' := hz
    rw [← bot_eq_of_le_or_map_le le_map hy] at hz'
    rcases hz' with ⟨_, (hz' | hz')⟩
    · rcases le_iff_lt_or_eq.1 hz' with (hz' | rfl)
      · exact le_trans (hy.map_le_of_mem_of_lt hz hz') (le_map y)
      · exact le_refl (f z)
    · exfalso
      exact lt_irrefl z (lt_of_lt_of_le hzy hz')
  · intro c hc
    refine ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (fun _ h ↦ h.mem_bot)), ?_⟩
    intro y hy hy'
    obtain ⟨z, hz, hzy⟩ : ∃ z ∈ c, ¬ (f z ≤ y) := by
      by_contra! h
      apply lt_irrefl y (lt_of_lt_of_le hy' ?_)
      apply cSup_le
      intro z hz
      exact le_trans (le_map z) (h z hz)
    have h : y ≤ z := by
      rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hy
      exact Or.resolve_right hy.2 hzy
    obtain hyz | rfl := le_iff_lt_or_eq.1 h
    · exact le_trans ((hc hz).map_le_of_mem_of_lt hy hyz) (le_cSup _ _ hz)
    · have hc' := (bot_isAdmissible le_map).cSup_mem _ (subset_trans hc fun _ h ↦ h.mem_bot)
      rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hc'
      apply hc'.2.resolve_left
      intro hc'
      exact lt_irrefl y (lt_of_lt_of_le hy' hc')

Goal state after:
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
left

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

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

Tactic:
· apply le_trans _ (h (max i j))
    trans c₀ i (c₁ (max i j))
    · apply (c₀ i).monotone
      apply c₁.monotone
      apply le_max_right
    · apply c₀.monotone
      apply le_max_left

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

Goal state before:
pp: case inl
c : Cardinal.{u}
ha : c ≤ ℵ₀
⊢ toENat (lift.{v, u} c) = toENat c

Tactic:
| inl ha =>

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

Goal state before:
pp: α : Type u
⊢ 1 < #α ↔ Nontrivial α

Tactic:
rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not]

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

Goal state before:
pp: ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ lift.{w', w} (iSup f) ≤ lift.{w, w'} (iSup f')

Tactic:
rw [lift_iSup hf, lift_iSup hf']
  exact ciSup_mono_of_forall_exists' (bddAbove_range_comp.{_, _, w} hf' _) fun i => ⟨_, h i⟩

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • 1 * x = r • x

Tactic:
rw [h₁, one_mul]

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 : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
⊢ map f p ⋖ map f q

Tactic:
refine ⟨lt_of_le_of_ne (map_mono h.1.le) ((map_injective_of_injective hf).ne h.1.ne), ?_⟩
  intro P h₁ h₂
  refine h.2 ?_ (Submodule.comap_lt_of_lt_map_of_injective hf h₂)
  rw [← Submodule.map_lt_map_iff_of_injective hf]
  refine h₁.trans_le ?_
  exact (Set.image_preimage_eq_of_subset (.trans h₂.le (Set.image_subset_range _ _))).superset

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

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
⊢ comap (a • f) p = comap f p

Tactic:
ext b; simp only [Submodule.mem_comap, p.smul_mem_iff h, LinearMap.smul_apply]

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

Goal state before:
pp: case inl
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False

Tactic:
exact zero_ne_one h.symm

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

Goal state before:
pp: case inr
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False

Tactic:
exact zero_ne_one h.symm

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
⊢ ∀ {a b : N}, a ∈ ⇑f '' ↑S → b ∈ ⇑f '' ↑S → a * b ∈ ⇑f '' ↑S

Tactic:
rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
    exact ⟨x * y, @mul_mem (Subsemigroup M) M _ _ _ _ _ _ hx hy, by rw [map_mul]⟩

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
x : M₀
⊢ x ∉ nonZeroDivisorsLeft M₀ ↔ {y | x * y = 0 ∧ y ≠ 0}.Nonempty

Tactic:
by
  simpa [mem_nonZeroDivisorsLeft_iff] using! Set.nonempty_def.symm

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

Goal state before:
pp: M₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
S : Submonoid M₀
hS : 0 ∉ S
x✝ : M₀
hx : x✝ ∈ S
⊢ x✝ ≠ 0

Tactic:
by rintro rfl; exact hS hx

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₂
p : Submodule R₂ M₂
⊢ f.range ≤ p ↔ comap f p = ⊤

Tactic:
by rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm (e 1 * x)) = (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1)

Tactic:
e.apply_symm_apply,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm (e 1 * x)) = (algebraMap R A) (e.symm (e 1 * x)) * 1
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm 1) * e (e.symm (e 1 * x)) = x

Tactic:
e.apply_symm_apply,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm 1) * (e 1 * x) = x
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ e (e.symm 1) * x = x

Tactic:
e.apply_symm_apply,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ 1 * x = x
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ ⋯.closureOperator = c

Tactic:
ext x
  rfl

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t

Tactic:
simpa only [coe_product] using Set.prod_mono hus hvt

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 : Type u_9
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ {r • x} ⊆ ↑(R ∙ x)

Tactic:
Set.singleton_subset_iff,

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_9
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ r • x ∈ ↑(R ∙ x)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup

Tactic:
ext x
  rw [mem_toAddSubgroup, mem_sup, AddSubgroup.mem_sup]
  rfl

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hs : s.Nonempty
hs' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
h_le : k ≤ sSup s
⊢ ∃ x ∈ s, k ≤ x

Tactic:
exact hk s (sSup s) hs hs' (isLUB_sSup s) h_le

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inl
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
i : ι
hi : i ≠ k
⊢ t i = t j

Tactic:
rw [(huniv i).resolve_left hi]

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
⊢ ∏ j ∈ s, f j = 0

Tactic:
classical rw [← prod_erase_mul _ _ hi, h, mul_zero]

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

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
⊢ (fun φ i ↦ φ.comp (MonoidHom.mulSingle M i)) ((fun φ ↦ ∏ i, (φ i).comp (evalMonoidHom M i)) φ) = φ

Tactic:
ext i m

Goal state after:
ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
⊢ ((fun φ i ↦ φ.comp (MonoidHom.mulSingle M i)) ((fun φ ↦ ∏ i, (φ i).comp (evalMonoidHom M i)) φ) i) m = (φ i) m
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ⟨b, hbk⟩ = ⊤ ∨ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Tactic:
left

Goal state after:
case inl
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ⟨b, hbk⟩ = ⊤
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
a : R
s✝ : Multiset ι
f : ι → R
i : ι
s : Multiset ι
ih : (map (fun i ↦ a * f i) s).sum = a * (map f s).sum
⊢ (map (fun i ↦ a * f i) (i ::ₘ s)).sum = a * (map f (i ::ₘ s)).sum

Tactic:
by simp [ih, mul_add]

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 = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
left

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} ⊆ {⊥}
⊢ b = ⊥
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R✝¹ : Type u_1
R₂ : Type u_2
K : Type u_3
M✝¹ : Type u_4
M₂ : Type u_5
V : Type u_6
S : Type u_7
R✝ : Type u_8
M✝ : Type u_9
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u_10
M : Type u_11
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : Submodule R M
hxy : x✝⁴ ≤ x✝²
x✝¹ : M
x✝ : x✝¹ ∈ (x✝⁴ ⊔ x✝³) ⊓ x✝²
⊢ x✝¹ ∈ x✝⁴ ⊔ x✝³ ⊓ x✝²

Tactic:
rwa [← sup_inf_assoc_of_le_of_neg_le _ hxy (by simpa)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_6
inst✝ : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
by_cases hs : x ∈ s <;> by_cases ht : x ∈ t <;> simp [mem_symmDiff, *]

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

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s : Submodule K V
⊢ s ⩿ K ∙ x ⊔ s

Tactic:
by
  refine ⟨le_sup_right, fun q hpq hqp ↦ hqp.not_ge ?_⟩
  rcases SetLike.exists_of_lt hpq with ⟨y, hyq, hyp⟩
  obtain ⟨c, z, hz, rfl⟩ : ∃ c : K, ∃ z ∈ s, c • x + z = y := by
    simpa [mem_sup, mem_span_singleton] using hqp.le hyq
  rcases eq_or_ne c 0 with rfl | hc
  · simp [hz] at hyp
  · have : x ∈ q := by
      rwa [q.add_mem_iff_left (hpq.le hz), q.smul_mem_iff hc] at hyq
    simp [hpq.le, this]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case inl
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hkn : k ≤ n
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
exact prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm

Goal state after:
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ (indicator s f) i = if hi : i ∈ s then f i hi else 0

Tactic:
simp only [indicator, ne_eq, coe_mk]
  congr

Goal state after:
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ Pi.single a b a' = if a' = a then b else 0

Tactic:
Pi.single_apply

Goal state after:
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Unique α
b' : M
⊢ (single a b) default = (single a' b') default ↔ b = b'

Tactic:
Unique.eq_default a,

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Unique α
b' : M
⊢ (single default b) default = (single a' b') default ↔ b = b'
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

Tactic:
by_cases hx : x ∈ ⋃ i, s i

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

case neg
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ -u • x = -(u • x)

Tactic:
Units.smul_def,

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ ↑(-u) • x = -(u • x)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
⊢ ∑ i, (∑ a, single a (f a)) i = ∑ a, f a

Tactic:
coe_univ_sum_single

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
⊢ ∑ i, f i = ∑ a, f a