mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ↑(filterNe a (fill a m.fst m.snd)).snd = ↑m.snd

Tactic:
rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ filter (fun x ↦ a ≠ x) (↑m.snd + ↑(replicate (↑m.fst) a)) = ↑m.snd
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:
by
        obtain ⟨b | b, h⟩ := exists_lt (inr a : α ⊕ β)
        · exact (not_inl_lt_inr h).elim
        · exact ⟨b, inr_lt_inr_iff.1 h⟩

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
hlim : ¬IsSuccPrelimit (sSup ∅)
⊢ sSup ∅ ∈ ∅

Tactic:
simp [isSuccPrelimit_bot] at hlim

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Basic

Goal state before:
pp: α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f^[n]) s

Tactic:
by
  rw [Set.preimage_iterate_eq]
  exact h.iterate n

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

Tactic:
by_cases h : o.Dom

Goal state after:
case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

Tactic:
by_cases h : o.Dom

Goal state after:
case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ o.toOption = none ↔ ¬o.Dom
Module: Mathlib.Data.Part

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

Tactic:
by_cases h : o.Dom

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

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

Goal state before:
pp: α : Type u_4
o : Option α
h₁ : (↑o).Dom
h₂ : { Dom := o.isSome = true, get := o.get }.Dom
⊢ (↑o).get h₁ = { Dom := o.isSome = true, get := o.get }.get h₂

Tactic:
cases o

Goal state after:
case none
α : Type u_4
h₁ : (↑Option.none).Dom
h₂ : { Dom := Option.none.isSome = true, get := Option.none.get }.Dom
⊢ (↑Option.none).get h₁ = { Dom := Option.none.isSome = true, get := Option.none.get }.get h₂

case some
α : Type u_4
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.Dom
⊢ (↑(Option.some val✝)).get h₁ = { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.get h₂
Module: Mathlib.Data.Part

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

Tactic:
cases o

Goal state after:
case none
α : Type u_1
⊢ (↑Option.none).toOption = Option.none

case some
α : Type u_1
val✝ : α
⊢ (↑(Option.some val✝)).toOption = Option.some val✝
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

Goal state after:
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

case neg
α : 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
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ (x.bind fun x ↦ (f x).bind fun y ↦ some (g y)) = x.bind fun y ↦ map g (f y)

Tactic:
simp [bind_some_eq_map]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ {α β : Type u_4}, Functor.mapConst = Functor.map ∘ const β

Tactic:
simp [Functor.mapConst, Functor.map]

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

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

Tactic:
· simp only [toENatAux_eq_top hy]
        rw [toENatAux_eq_top, ENat.mul_top]
        · rwa [Ne, toENatAux_eq_zero]
        · exact le_mul_of_one_le_of_le (Cardinal.one_le_iff_ne_zero.2 hx) hy

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
rw [← mul_and_mul_iff]
  exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩

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

Goal state before:
pp: α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} ↑(Iic #(Quotient.out a))

Tactic:
apply @small_of_surjective (Set a.out) (Iic #a.out) _ fun x => ⟨#x, mk_set_le x⟩

Goal state after:
α β : Type u
a : Cardinal.{u}
⊢ Surjective fun x ↦ ⟨#↑x, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
⊢ lift.{u, 0} #(Fin (n + 1)) ≤ ℵ₀

Tactic:
aleph0,

Goal state after:
n : ℕ
⊢ lift.{u, 0} #(Fin (n + 1)) ≤ lift.{u, 0} #ℕ
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ #α ≤ ℵ₀ ↔ Nonempty (α ↪ ℕ)

Tactic:
aleph0,

Goal state after:
α : Type u
⊢ #α ≤ lift.{u, 0} #ℕ ↔ Nonempty (α ↪ ℕ)
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 : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r : R
x : A
⊢ r • x = { toFun := fun r ↦ r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
simp [h₁]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
f g : M →ₛₗ[σ] M₃
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by
    cases f
    cases g
    congr
    apply DFunLike.coe_injective
    exact h

Goal state after:
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 σ₁₃ σ₃₂ σ₁₂
h : M₁ →ₛₗ[σ₁₃] M₃
f' : M₃ →ₛₗ[σ₃₂] M₂
hf' : f ∘ₛₗ f' = id
⊢ id ∘ₛₗ h = h

Tactic:
id_comp

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

Goal state before:
pp: R : Type u_14
M : Type u_15
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ IsLinearMap R fun z ↦ c • z

Tactic:
refine IsLinearMap.mk (smul_add c) ?_

Goal state after:
R : Type u_14
M : Type u_15
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ ∀ (c_1 : R) (x : M), c • c_1 • x = c_1 • c • x
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 : ℕ
⊢ f' ^ (n + 1) = (f' ^ n) ∘ₗ f'

Tactic:
rw [pow_succ, mul_eq_comp]

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

Goal state before:
pp: 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✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : R →ₗ[R] M
⊢ (smulRight 1 ((fun f ↦ f 1) f)) 1 = f 1

Tactic:
simp only [coe_smulRight, Module.End.one_apply, smul_eq_mul, ← map_smul f, mul_one]

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 α
x : α × α
s : Set (α × α)
⊢ (sSup s).1 ⊔ (sSup s).2 = sSup ((fun x ↦ x.1 ⊔ x.2) '' s)

Tactic:
by simp_rw [Prod.fst_sSup, Prod.snd_sSup, sSup_image, iSup_sup_eq]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_5
inst✝ : Mul N
f : M →ₙ* N
⊢ ↑f.srange = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_srange,

Goal state after:
M : Type u_1
inst✝¹ : Mul M
N : Type u_5
inst✝ : Mul N
f : M →ₙ* N
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ↑(srange f) = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_srange,

Goal state after:
R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.Algebra.Group.Irreducible.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ ¬Irreducible 1

Tactic:
simp [irreducible_iff]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
y : M
u : Mˣ
⊢ Prime (y * ↑u) ↔ Prime y

Tactic:
by
  rw [mul_comm, prime_units_mul]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : ↑a ∣ ↑b
c : M₀
hc : ↑b = ↑a * c
⊢ b = a * ⟨c, ⋯⟩

Tactic:
by simp_rw [Subtype.ext_iff, Submonoid.coe_mul, hc]

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

Goal state before:
pp: case mp.mk.refine_2
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ x ≠ 0

Tactic:
rwa [← Associates.mk_ne_zero, ← Associates.quot_mk_eq_mk]

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ map f s ⊔ map f (closure (⇑f ⁻¹' {0})) ≤ map f s

Tactic:
f.map_closure

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ map f s ⊔ closure (⇑f '' ⇑f ⁻¹' {0}) ≤ map f s
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₂
hf : f.range = ⊤
p p' : Submodule R₂ M₂
H : comap f p ≤ comap f p'
⊢ p ≤ p'

Tactic:
rwa [SetLike.le_def, (range_eq_top.1 hf).forall]

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

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₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst✝ : Module R₂ M₂
e : ↥p ≃ₛₗ[σ₁₂] ↥⊥
b : M
hb : b ∈ p
⊢ b = 0

Tactic:
rw [← p.mk_eq_zero hb, ← e.map_eq_zero_iff]

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring R₂
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst✝ : Module R₂ M₂
e : ↥p ≃ₛₗ[σ₁₂] ↥⊥
b : M
hb : b ∈ p
⊢ e ⟨b, hb⟩ = 0
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N : Submodule R M
r : S
m : M
mem1 : r ∈ s
mem2 : m ∈ N
⊢ ∀ p ∈ {p | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}, r • m ∈ p

Tactic:
exact fun _ h => h mem1 mem2

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
⊢ {r} • N = r • N

Tactic:
by
  apply set_smul_eq_of_le
  · rintro _ m rfl hm; exact ⟨m, hm, rfl⟩
  · rintro _ ⟨m, hm, rfl⟩
    rw [mem_set_smul_def, Submodule.mem_sInf]
    intro _ hp; exact hp rfl hm

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ max a b ∈ s

Tactic:
cases le_total a b

Goal state after:
case inl
α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h✝ : a ≤ b
⊢ max a b ∈ s

case inr
α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h✝ : b ≤ a
⊢ max a b ∈ s
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b : α
ha : IsAtom a
⊢ ¬Disjoint a b ↔ a ≤ b

Tactic:
rw [disjoint_iff, ← inf_eq_left]

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b : α
ha : IsAtom a
⊢ ¬a ⊓ b = ⊥ ↔ a ⊓ b = a
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
w x y z : M
⊢ w ∈ span R {x, y, z} ↔ ∃ a b c, a • x + b • y + c • z = w

Tactic:
rw [mem_span_insert]
  simp_rw [mem_span_pair]
  refine exists_congr fun a ↦ ⟨?_, ?_⟩
  · rintro ⟨u, ⟨b, c, rfl⟩, rfl⟩
    exact ⟨b, c, by rw [add_assoc]⟩
  · rintro ⟨b, c, rfl⟩
    exact ⟨b • y + c • z, ⟨b, c, rfl⟩, by rw [add_assoc]⟩

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ (↑↑↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
rw [algebraMap_apply R S A, algebraMap_apply R S B]

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ (↑↑↑f).toFun ((algebraMap S A) ((algebraMap R S) r)) = (algebraMap S B) ((algebraMap R S) r)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A ≃ₐ[S] B
r : R
⊢ f.toRingEquiv.toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
rw [algebraMap_apply R S A, algebraMap_apply R S B]

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A ≃ₐ[S] B
r : R
⊢ f.toRingEquiv.toFun ((algebraMap S A) ((algebraMap R S) r)) = (algebraMap S B) ((algebraMap R S) r)
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
a : List α
l : List (List α)
⊢ (↑(List.map (fun l ↦ ↑l) (a :: l))).Sections = ↑(List.map (fun l ↦ ↑l) (a :: l).sections)

Tactic:
by
    simp only [List.map_cons, List.sections]
    rw [← cons_coe, sections_cons, bind_map_comm, coe_sections l]
    simp [Function.comp_def, List.flatMap]

Goal state after:
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun s a ↦ a ∈ s) s a

Tactic:
by
  induction s using Multiset.induction_on with
  | empty => simp
  | cons _ _ ih => simp [ih, rel_cons_left, eq_comm]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ∀ i_1 ∈ Finset.image (fun x ↦ x i) s, ∀ b ∈ {c ∈ s | c i = i_1}, ⨅ i, f i (b i) ≤ f i i_1

Tactic:
Finset.mem_filter,

Goal state after:
case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ∀ i_1 ∈ Finset.image (fun x ↦ x i) s, ∀ (b : (i : ι) → κ i), b ∈ s ∧ b i = i_1 → ⨅ i, f i (b i) ≤ f i i_1
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: case h.right
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
⊢ f c = a

Tactic:
· exact hc₂

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Tactic:
simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ Pi.single k u + Pi.single l v = Pi.single m u + Pi.single n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst f.graph = f.support

Tactic:
classical
  simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β) (b₁ b₂ : M), single (g a) (b₁ + b₂) = single (g a) b₁ + single (g a) b₂

Tactic:
intro
    exact single_add _

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
have hps : ∀ x, x ∈ s → p x := fun x hx ↦ hpsa x (mem_cons_of_mem hx)

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

Tactic:
apply Set.union_subset hv₁ hv₂

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ ↑v₁.support ∪ ↑v₂.support
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #s ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})

Tactic:
by
  rw [← Finset.card_filter_add_card_filter_not fun i ↦ f i = ∅, add_comm]
  grw [card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
    nonempty_of_ne_empty (mem_filter.1 hi).2, filter_subset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
⊢ g • 0 = 0

Tactic:
by
    ext a
    simp only [comapSMul_def]
    simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Ioc i j = Ioc ↑i ↑j

Tactic:
rw [← preimage_val_Ioc_val, image_preimage_eq_inter_range, range_val, inter_eq_left]

Goal state after:
n : ℕ
i j : Fin n
⊢ Ioc ↑i ↑j ⊆ Iio n
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set α
ht : t.Finite
s : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
lift t to Finset α using ht

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i