mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝²⁴ : Monoid M
N : Type u_2
inst✝²³ : Monoid N
P : Type u_3
inst✝²² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝²¹ : Monoid A
inst✝²⁰ : MulDistribMulAction M A
B : Type u_5
inst✝¹⁹ : Monoid B
inst✝¹⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝¹⁷ : Monoid B₁
inst✝¹⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝¹⁵ : Monoid C
inst✝¹⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝¹³ : Group A'
inst✝¹² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹¹ : Group B'
inst✝¹⁰ : MulDistribMulAction N B'
R : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_11
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_12
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction N S
S' : Type u_13
inst✝³ : Ring S'
inst✝² : MulSemiringAction N S'
T : Type u_14
inst✝¹ : Semiring T
inst✝ : MulSemiringAction P T
f g : R →ₑ+*[φ] S
h : (fun m ↦ m.toFun) f = (fun m ↦ m.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨⟨tF, _, _⟩, _, _⟩

Goal state after:
M : Type u_1
inst✝²⁴ : Monoid M
N : Type u_2
inst✝²³ : Monoid N
P : Type u_3
inst✝²² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝²¹ : Monoid A
inst✝²⁰ : MulDistribMulAction M A
B : Type u_5
inst✝¹⁹ : Monoid B
inst✝¹⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝¹⁷ : Monoid B₁
inst✝¹⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝¹⁵ : Monoid C
inst✝¹⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝¹³ : Group A'
inst✝¹² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹¹ : Group B'
inst✝¹⁰ : MulDistribMulAction N B'
R : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type u_11
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_12
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction N S
S' : Type u_13
inst✝³ : Ring S'
inst✝² : MulSemiringAction N S'
T : Type u_14
inst✝¹ : Semiring T
inst✝ : MulSemiringAction P T
g : R →ₑ+*[φ] S
tF : R →ₑ[⇑φ] S
map_zero'✝ : tF.toFun 0 = 0
map_add'✝ : ∀ (x y : R), tF.toFun (x + y) = tF.toFun x + tF.toFun y
map_one'✝ : { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : R),
    { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (x * y) =
      { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun x *
        { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun y
h :
  (fun m ↦ m.toFun)
      { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝, map_one' := map_one'✝,
        map_mul' := map_mul'✝ } =
    (fun m ↦ m.toFun) g
⊢ { toMulActionHom := tF, map_zero' := map_zero'✝, map_add' := map_add'✝, map_one' := map_one'✝,
      map_mul' := map_mul'✝ } =
    g
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R'
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁵ : Monoid S'
inst✝⁴ : DistribMulAction S' M
inst✝³ : SMulCommClass R S' M
inst✝² : Monoid T'
inst✝¹ : DistribMulAction T' M
inst✝ : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
c : R
x : M
⊢ (a • ⇑f) (c • x) = σ₁₂ c • (a • ⇑f) x

Tactic:
by simp_rw [DomMulAct.smul_apply, ← smul_comm, f.map_smulₛₗ]

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

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R M
inst✝⁶ : Module R M₁
inst✝⁵ : Semiring S
inst✝⁴ : Module R S
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : IsDomain S
f : M₁ →ₗ[R] S
x : M
inst✝ : Module.IsTorsionFree S M
⊢ f.smulRight x = 0 ↔ f = 0 ∨ x = 0

Tactic:
simp [DFunLike.ext_iff, forall_or_right]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ ∀ (g : G₀), g * ↑u = ↑u * g

Tactic:
a

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
⊢ a * ↑u = ↑u * a
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
⊢ a⁻¹ ∈ s.centralizer

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0⁻¹ ∈ s.centralizer

case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
⊢ a⁻¹ ∈ s.centralizer
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
⊢ ↑(n + 1) * (x✝¹ * x✝) = ↑(n + 1) * x✝¹ * x✝

Tactic:
rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s

Tactic:
ext x
  refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
  rintro - ⟨H, rfl⟩
  rintro - ⟨J, rfl⟩
  refine (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => ?_
  refine (Subsemigroup.mem_closure.mp hy) H.toSubsemigroup fun z hz => ?_
  exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
hf : f 1 = 1
r : R
h : Invertible ((algebraMap R A) r)
⊢ f ⅟((algebraMap R A) r) * (algebraMap R B) r = 1

Tactic:
rw [← Algebra.commutes, ← Algebra.smul_def, ← map_smul, Algebra.smul_def,
    mul_invOf_self, hf]

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

Goal state before:
pp: case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
⊢ C (List.map List.prod (hd :: tl)).sum

Tactic:
suffices C (List.prod hd) by
    rw [List.map_cons, List.sum_cons]
    exact ha this (ih HL.2)

Goal state after:
case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
⊢ C hd.prod
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inr.cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ x ∈ tl, x ∈ s) → C (-tl.prod)
HL' : ∀ x ∈ hd :: tl, x ∈ s
⊢ C (-(hd :: tl).prod)

Tactic:
rw [List.prod_cons, neg_mul_eq_mul_neg]
      rw [List.forall_mem_cons] at HL'
      exact hs _ HL'.1 _ (ih HL'.2)

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

Goal state before:
pp: case mp.mk.refine_1
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
⊢ Associates.mk x * Associates.mk a = 0

Tactic:
← Associates.quot_mk_eq_mk

Goal state after:
case mp.mk.refine_1
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
⊢ Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
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
⊢ Associates.mk x ≠ 0

Tactic:
← Associates.quot_mk_eq_mk

Goal state after:
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
⊢ Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
⊢ f - f = 0

Tactic:
sub_self

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
⊢ 0 = 0
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 : Surjective ⇑f
p q : Submodule R M
hpq : Codisjoint p q
⊢ Codisjoint (map f p) (map f q)

Tactic:
codisjoint_iff,

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₂
hf : Surjective ⇑f
p q : Submodule R M
hpq : Codisjoint p q
⊢ map f p ⊔ map f q = ⊤
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
p p' : Submodule R M
⊢ Codisjoint p p' ↔ ∀ (z : M), ∃ x y, x ∈ p ∧ y ∈ p' ∧ x + y = z

Tactic:
codisjoint_iff,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ p ⊔ p' = ⊤ ↔ ∀ (z : M), ∃ x y, x ∈ p ∧ y ∈ p' ∧ x + y = z
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderTop α
a b : α
ha : IsCoatom a
⊢ ¬Codisjoint a b ↔ b ≤ a

Tactic:
codisjoint_iff,

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderTop α
a b : α
ha : IsCoatom a
⊢ ¬a ⊔ b = ⊤ ↔ b ≤ a
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
obtain ⟨⟨a', ha'b : a' ≤ b⟩, ha'⟩ := exists_isCompl (α := Set.Iic b) ⟨a, hab.le⟩

Goal state after:
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩
⊢ ∃ x, a ⋖ x ∧ x ≤ b
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ (iSupIndep fun i ↦ t ↑i) ↔ iSupIndep t

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.comp Subtype.val_injective⟩
  simp only [iSupIndep_def] at h ⊢
  intro i
  cases eq_or_ne (t i) ⊥ with
  | inl hi => simp [hi]
  | inr hi => ?_
  convert! h ⟨i, hi⟩
  have : ∀ j, ⨆ (_ : t j = ⊥), t j = ⊥ := fun j ↦ by simp only [iSup_eq_bot, imp_self]
  rw [iSup_split _ (fun j ↦ t j = ⊥), iSup_subtype]
  simp only [iSup_comm (ι' := _ ≠ i), this, ne_eq, sup_of_le_right, Subtype.mk.injEq, iSup_bot,
    bot_le]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f g : ι → α
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ j, ⨆ (_ : j ≠ i), f j) (g i)
⊢ Codisjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)

Tactic:
codisjoint_iff,

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f g : ι → α
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ j, ⨆ (_ : j ≠ i), f j) (g i)
⊢ f i ⊔ ⨆ j, ⨆ (_ : j ≠ i), f j = ⊤
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ t.sup id ≤ sSup s

Tactic:
simp only [id, Finset.sup_le_iff]

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ ∀ b ∈ t, b ≤ sSup s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : ↑u ⊆ range fun x ↦ f ↑x
⊢ ↑u ⊆ f '' s

Tactic:
by rwa [Set.image_eq_range f s]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
x✝ : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).1 + (x₁, x₂).2 = ↑l
⊢ (x₁, (x₁, x₂).1 + (x₁, x₂).2 - x₁) = (x₁, x₂)

Tactic:
by rw [add_tsub_cancel_left x₁ x₂]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
f₂ : N ≃ O
hf₂ : f₂ 0 = 0
⊢ (e.trans f₂) 0 = 0

Tactic:
Equiv.trans_apply,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
e : M ≃ N
hf : e 0 = 0
f₂ : N ≃ O
hf₂ : f₂ 0 = 0
⊢ f₂ (e 0) = 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

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

Tactic:
by
  simp_rw [single, coe_mk]
  classical rw [Finset.sum_pi_single]
  simp

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

Goal state before:
pp: R : Type u_5
inst✝⁶ : Semiring R
S : Type u_6
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
inst✝³ : IsOrderedRing S
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : v ≠ AbsoluteValue.trivial
⊢ ∃ x, x ≠ 0 ∧ v x ≠ 1

Tactic:
contrapose! H

Goal state after:
R : Type u_5
inst✝⁶ : Semiring R
S : Type u_6
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
inst✝³ : IsOrderedRing S
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R), x ≠ 0 → v x = 1
⊢ v = AbsoluteValue.trivial
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_4
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s : Multiset α
⊢ ∀ (a : List α), (∀ (x : α), x ∈ a → 1 ≤ x) → a.prod = 1 → ∀ (x : α), x ∈ a → x = 1

Tactic:
exact fun l => List.all_one_of_le_one_le_of_prod_eq_one

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), f a ∉ l.support
⊢ ∀ (a : β), a ∉ l.support

Tactic:
a

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), f a ∉ l.support
a : β
⊢ a ∉ l.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p f + filter (fun x ↦ ¬p x) f = f

Tactic:
by ext; simp [filter_apply]; split <;> simp

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i

Tactic:
rw [right_distrib]
    gcongr with j hj <;> aesop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ g (∏ x ∈ s, f x) ≤ ∑ x ∈ s, g (f x)

Tactic:
by
  refine (Multiset.apply_prod_le_sum_map _ _ h_one h_mul).trans_eq ?_
  rw [Multiset.map_map, Function.comp_def, Finset.sum_map_val]

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

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
refine le_of_mul_le_mul_of_pos_left
      (le_of_add_le_add_left (a := (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2) ?_) h

Goal state after:
case inr
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 ≤
    (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * ((∑ i ∈ s, f i) * ∑ i ∈ s, g i)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝¹ : Zero γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
f : α ⊕ β →₀ γ
ab : α ⊕ β
⊢ ((fun fg ↦ fg.1.sumElim fg.2) ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f)) ab = f ab

Tactic:
rcases ab with a | b <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M✝ : Type u_5
N : Type u_6
P✝ : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ ∀ ⦃a : α⦄ (x : Subtype P), x ∈ f.support ∧ ↑x = a → ¬∃ a_1 ∈ g.support, ↑a_1 = a

Tactic:
Subtype.forall,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M✝ : Type u_5
N : Type u_6
P✝ : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ ∀ ⦃a : α⦄ (a_1 : α) (b : P a_1), ⟨a_1, b⟩ ∈ f.support ∧ a_1 = a → ¬∃ a_2 ∈ g.support, ↑a_2 = a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
⊢ ¬(mapDomain f x) t = 0 → ∃ a ∈ x.support, f a = t

Tactic:
simpa [mapDomain, sum, single_apply] using fun i h h' _ ↦ ⟨i, h, h'⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_3
R : Type u_6
p : α → Prop
inst✝² : DecidablePred p
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
b : R
v : α →₀ M
⊢ {x | p x}.indicator (b • ⇑v) = b • {x | p x}.indicator ⇑v

Tactic:
exact Set.indicator_const_smul { x | p x } b v

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
M✝ : Type u_2
N✝ : Type u_3
P : Type u_4
R✝ : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S✝ : Type u_8
inst✝¹⁷ : Semiring R✝
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring S✝
inst✝¹³ : AddCommMonoid M✝
inst✝¹² : Module R✝ M✝
inst✝¹¹ : AddCommMonoid N✝
inst✝¹⁰ : Module R₂ N✝
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R₃ P
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMul R M
inst✝¹ : SMulZeroClass R N
inst✝ : CompatibleSMul M N R S
f : M →ₗ[S] ι →₀ N
r : R
m : M
⊢ f (r • m) = r • f m

Tactic:
by ext i; apply ((lapply i).comp f).map_smul_of_tower

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Codisjoint s t
⊢ Codisjoint (supported M R s) (supported M R t)

Tactic:
codisjoint_iff,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Codisjoint s t
⊢ supported M R s ⊔ supported M R t = ⊤
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Codisjoint (supported M R s) (supported M R t)
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t

Tactic:
codisjoint_iff,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : supported M R s ⊔ supported M R t = ⊤
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t
Module: Mathlib.Data.Finset.Fin

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ map Fin.valEmbedding (s.attachFin h) = s

Tactic:
simp [map_eq_image]

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

Goal state before:
pp: n : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ico i j ↔ x✝ ∈ Ioc j.rev i.rev

Tactic:
simp [le_rev_iff, rev_lt_iff, and_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁷ : Fintype α
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : SMulCommClass R S M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ ((Fintype.bilinearCombination R S) v) (Pi.single i r) = r • v i

Tactic:
by
  simp [Fintype.bilinearCombination]

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ map (castAddEmb m) (Ici i) = Ico (castAdd m i) (natAdd n 0)

Tactic:
simp [map_eq_image]

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 ↦ n_1 + n_1) i

Tactic:
simp_rw [Function.comp, vecAlt0, vecAppend_eq_ite]

Goal state after:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ (if h : ↑i + ↑i < n then v ⟨↑i + ↑i, ⋯⟩ else v ⟨↑i + ↑i - n, ⋯⟩) = v (i + i)
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inl
y z : ℕ∞
⊢ (1 * y) ^ ⊤ = 1 ^ ⊤ * y ^ ⊤

pp: case top.inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
· simp only [one_mul, one_epow]

Goal state after:
case top.inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z : ℤ
h : a ≡ b [PMOD z • p]
⊢ a ≡ b [PMOD p]

Tactic:
rw [modEq_iff_zsmul] at *

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z : ℤ
h : ∃ m, m • z • p = b - a
⊢ ∃ m, m • p = b - a
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z : ℤ
h : a ≡ b [PMOD p]
⊢ z • a ≡ z • b [PMOD z • p]

Tactic:
rw [modEq_iff_zsmul] at *

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z : ℤ
h : ∃ m, m • p = b - a
⊢ ∃ m, m • z • p = z • b - z • a