mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case cons
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x1 x2 ↦ x1 ≤ x2) as✝ bs✝
rt : as✝.prod ≤ bs✝.prod
⊢ a✝¹ * as✝.prod ≤ (b✝ ::ₘ bs✝).prod

Tactic:
prod_cons

Goal state after:
case cons
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x1 x2 ↦ x1 ≤ x2) as✝ bs✝
rt : as✝.prod ≤ bs✝.prod
⊢ a✝¹ * as✝.prod ≤ b✝ * bs✝.prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
a : α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedMul α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ (a ::ₘ t).prod

Tactic:
prod_cons

Goal state after:
α : Type u_2
inst✝² : CommMonoid α
a : α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedMul α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ a * t.prod
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
s : List R
h : ∀ (a : R), a ∈ s → 0 ≤ a
⊢ 0 ≤ s.prod

Tactic:
by
  induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact mul_nonneg h.1 (hind h.2)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ hx_w ∈ s.support

Tactic:
mem_support_iff,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ s hx_w ≠ 0
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 = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ (f a ::ₘ map f s).prod

Tactic:
prod_cons

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
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ f a * (map f s).prod
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ f a ≤ (f a ::ₘ map f s').prod

Tactic:
prod_cons

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ f a ≤ f a * (map f s').prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case pos
α : 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
⊢ v₁ a = v₂ a

Tactic:
rw [← mapDomain_apply' S _ hv₁ hf _, ← mapDomain_apply' S _ hv₂ hf _, eq] <;>
        · apply Set.union_subset hv₁ hv₂
          exact mod_cast h

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ i ∈ s, f i ^ 2 ≤ (∑ i ∈ s, f i) ^ 2

Tactic:
simp only [sq, sum_mul_sum]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ x ∈ s, f x * f x ≤ ∑ i ∈ s, ∑ j ∈ s, f i * f j
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
h : a ∉ f.support
ha : a ∈ (f + s.sum).support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
mem_support_iff,

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
h : a ∉ f.support
ha : (f + s.sum) a ≠ 0
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
⊢ t ∈ (mapDomain f x).support ↔ t ∈ image f x.support

Tactic:
mem_support_iff,

Goal state after:
α : 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 ↔ t ∈ image f x.support
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

Tactic:
← mul_lt_mul_iff_right,

Goal state after:
ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ (∏ i ∈ s \ t, f i) * ?a < (∏ i ∈ t \ s, f i) * ?a ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

case a
ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ M
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
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
⊢ ⊤ ≤ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))

Tactic:
rintro l ⟨⟩

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
l : α →₀ M
⊢ l ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
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
i : ι
⊢ (f (r • m)) i = (r • f m) i

Tactic:
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
inst✝ : Nontrivial M
s t : Set α
⊢ Codisjoint (supported M R s) (supported M R t) ↔ Codisjoint s t

Tactic:
refine ⟨fun h ↦ codisjoint_iff.mpr (eq_top_iff.mpr fun a ↦ ?_), codisjoint_supported_supported⟩

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 : Codisjoint (supported M R s) (supported M R t)
a : α
⊢ a ∈ ⊤ → a ∈ s ⊔ t
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
X : Type u_9
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
m✝ : S
x✝ : X → M
a✝ : X
⊢ ((lift M R X) (m✝ • x✝) ∘ₗ lsingle a✝) 1 = ((m✝ • (lift M R X) x✝) ∘ₗ lsingle a✝) 1

Tactic:
simp only [coe_comp, Function.comp_apply, lsingle_apply, lift_apply, Pi.smul_apply,
        sum_single_index, zero_smul, one_smul, LinearMap.smul_apply]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : SMulCommClass R R S
inst✝ : IsScalarTower R S S
M N : Submodule R S
ι : Type u_5
n : ι → ↥N
i : ι
m : ↥M
⊢ (M.mulRightMap n) (single i m) = ↑m * ↑(n i)

Tactic:
simp [mulRightMap]

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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
⊢ supported M R s ⊓ (lmapDomain M R f).ker ≤ ⊥

Tactic:
rintro l ⟨h₁, h₂⟩

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : l ∈ ↑(lmapDomain M R f).ker
⊢ l ∈ ⊥
Module: Mathlib.Data.Finset.Fin

Goal state before:
pp: n : ℕ
s t : Finset ℕ
hs : ∀ m ∈ s, m < n
ht : ∀ m ∈ t, m < n
⊢ s.attachFin hs ⊂ t.attachFin ht ↔ s ⊂ t

Tactic:
simp [← map_ssubset_map (f := Fin.valEmbedding)]

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

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

Tactic:
← preimage_val_Iic_val,

Goal state after:
n : ℕ
i : Fin n
⊢ val '' val ⁻¹' Iic ↑i = Iic ↑i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
x : M
⊢ x ∈ span R ↑s → ∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x

Tactic:
mem_span_iff_exists_finset_subset

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
x : M
⊢ (∃ f t, ↑t ⊆ ↑s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x) →
    ∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (j : ↑s), f ↑j = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
← finprod_mem_range,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (i : α) (_ : i ∈ range Subtype.val), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i

α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ Injective Subtype.val
Module: Mathlib.Data.Fin.VecNotation

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

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

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

Goal state before:
pp: case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ ∏ x, ∏ i ∈ t x, f i = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i ↦ ↑(t i)) i), f a

pp: case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ (↑Finset.univ).PairwiseDisjoint t

Tactic:
· simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]

Goal state after:
case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ (↑Finset.univ).PairwiseDisjoint t
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ Injective some

Tactic:
exact Option.some_injective _

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a - b ≤ a ↔ b ≤ a

Tactic:
by
  rw [← not_iff_not, Fin.not_le, Fin.not_le, lt_sub_iff]

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : x ≠ 0
y z : ℕ∞
y_z : y ≤ z
⊢ (fun y ↦ x ^ y) y ≤ (fun y ↦ x ^ y) z

Tactic:
induction y

Goal state after:
case top
x : ℕ∞
h : x ≠ 0
z : ℕ∞
y_z : ⊤ ≤ z
⊢ (fun y ↦ x ^ y) ⊤ ≤ (fun y ↦ x ^ y) z

case coe
x : ℕ∞
h : x ≠ 0
z : ℕ∞
a✝ : ℕ
y_z : ↑a✝ ≤ z
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y x z : ℕ∞
x_z : x ≤ z
⊢ x ^ y ≤ z ^ y

Tactic:
induction y

Goal state after:
case top
y x z : ℕ∞
x_z : x ≤ z
⊢ x ^ ⊤ ≤ z ^ ⊤

case coe
y x z : ℕ∞
x_z : x ≤ z
a✝ : ℕ
⊢ x ^ ↑a✝ ≤ z ^ ↑a✝
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
induction y

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

case inr.inr.coe
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ x ^ (↑a✝ + z) = x ^ ↑a✝ * x ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
induction y

Goal state after:
case inr.inr.inr.inr.top
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
y_0 : ⊤ ≠ 0
⊢ x ^ (⊤ * z) = (x ^ ⊤) ^ z

case inr.inr.inr.inr.coe
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
⊢ x ^ (↑a✝ * z) = (x ^ ↑a✝) ^ z
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
⊢ m.toNat • p + a = (-m).toNat • p + b

Tactic:
add_comm _ b,

Goal state after:
case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
⊢ m.toNat • p + a = b + (-m).toNat • p
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 *
  rcases h with ⟨m, h⟩
  use m
  rw [← zsmul_sub, ← h, ← mul_zsmul, ← mul_zsmul']

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ m, a - b = m • p) ↔ ∃ i, i < n ∧ ∃ m, a - i • p - b = m • n • p

Tactic:
sub_right_comm,

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ m, a - b = m • p) ↔ ∃ i, i < n ∧ ∃ m, a - b - i • p = m • n • p
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)

Tactic:
rcases lt_trichotomy (i : ℕ) a with (h | h | h)

Goal state after:
case refine_2.inl
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)

case refine_2.inr.inl
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i = ↑a
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)

case refine_2.inr.inr
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndepOn R v s ↔ Injective ⇑(Finsupp.linearCombinationOn ι M R v s)

Tactic:
by
  rw [← linearIndependent_restrict_iff]
  simp [LinearIndependent, Finsupp.linearCombination_restrict]

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n * c]

Tactic:
mul_comm a,

Goal state after:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ b * c [MOD n * c]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n]

Tactic:
mul_comm a,

Goal state after:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ b * c [MOD n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : range (w ∘ j) = range w
⊢ Surjective j

Tactic:
rw [range_comp, ← image_univ (f := w)] at p

Goal state after:
case mp
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ d ∣ a ↔ d ∣ b

Tactic:
by
  simp only [← modEq_zero_iff_dvd]
  replace h := h.of_dvd hdm
  exact ⟨h.symm.trans, h.trans⟩

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

Goal state before:
pp: case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
⊢ g i = 0

Tactic:
disjoint_def'

Goal state after:
case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
⊢ g i = 0
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card β ^ Finset.univ.card = Nat.card β ^ Nat.card α

Tactic:
Finset.card_univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card β ^ Fintype.card α = Nat.card β ^ Nat.card α
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inl.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Finite β
this : Fintype α := Fintype.ofFinite α
⊢ card (α → β) = card β ^ card α

Tactic:
let := Fintype.ofFinite β

Goal state after:
case inr.inl.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Finite β
this✝ : Fintype α := Fintype.ofFinite α
this : Fintype β := Fintype.ofFinite β
⊢ card (α → β) = card β ^ card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
h : Fintype α
ι : α → Type u_3
s : (i : α) → Set (ι i)
⊢ (univ.pi s).encard = ∏ i, (s i).encard

Tactic:
unfold encard ENat.card
  simp [Cardinal.mk_congr (Equiv.Set.univPi s), Cardinal.prod_eq_of_fintype]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Finite

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : Monoid.FG M
hS : S.FG
⊢ Monoid.FG (Localization S)

Tactic:
by
  rw [← Monoid.fg_iff_submonoid_fg] at hS; exact Monoid.fg_of_surjective mkHom mkHom_surjective

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ s.Finite ↔ t.Finite

Tactic:
← encard_lt_top_iff,

Goal state after:
α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ s.encard < ⊤ ↔ t.Finite
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ s.encard < ⊤ ↔ t.Finite

Tactic:
← encard_lt_top_iff,

Goal state after:
α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ s.encard < ⊤ ↔ t.encard < ⊤
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
⊢ l = 0

Tactic:
ext i; simp only [Finsupp.zero_apply]
      by_contra hn
      refine hn (H i _ ?_)
      refine (Finsupp.mem_span_image_iff_linearCombination R).2 ⟨Finsupp.single i (l i) - l, ?_, ?_⟩
      · rw [Finsupp.mem_supported']
        intro j hj
        have hij : j = i :=
          Classical.not_not.1 fun hij : j ≠ i =>
            hj ((mem_sdiff _).2 ⟨mem_univ _, fun h => hij (eq_of_mem_singleton h)⟩)
        simp [hij]
      · simp [hl]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ ∑ i ∈ (b.repr y).support, z * (b.repr y) i • b i = ∑ i ∈ (b.repr y).support, (b.repr y) i • b i * z

Tactic:
mul_smul_comm,

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ ∑ x ∈ (b.repr y).support, (b.repr y) x • (z * b x) = ∑ i ∈ (b.repr y).support, (b.repr y) i • b i * z