mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)).range ≤ ⨆ i, supported M R (s i)
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)

Tactic:
LinearMap.range_comp,

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
this : map (supported M R (⋃ i, s i)).subtype (restrictDom M R (⋃ i, s i)).range ≤ ⨆ i, supported M R (s i)
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : p
this : Unique p
⊢ ∏ᶠ (i : p), f i = f h

Tactic:
exact finprod_unique f

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

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
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
i : α
x✝ : f i ≠ 0
hi : i ≠ a
⊢ f i • Pi.single a c i = 0

Tactic:
rw [Pi.single_eq_of_ne hi, smul_zero]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
⊢ mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)

Tactic:
rw [A, Finset.coe_map]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
⊢ ⇑Equiv.plift.symm '' mulSupport f ⊆ ⇑Equiv.plift.symm.toEmbedding '' ↑s
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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✝ : Unique α
l : α →₀ R
v : α → M
⊢ (linearCombination R v) l = l default • v default

Tactic:
rw [← linearCombination_single, ← unique_single l]

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

Goal state before:
pp: M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R s = (linearCombination R Subtype.val).range

Tactic:
by
  rw [range_linearCombination, Subtype.range_coe_subtype, Set.ofPred_mem_eq]

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

Goal state before:
pp: ι : Type u_7
N₀ : Type u_8
M₀ : Type u_9
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
n : N₀
f : ι → N₀ → M₀
h : ∀ (i : ι), f i n ≠ 0
⊢ (∏ᶠ (i : ι), f i) n ≠ 0

Tactic:
by
  by_cases h₂ : f.mulSupport.Finite
  · rw [finprod_eq_prod f h₂]
    grind [Finset.prod_apply, Finset.prod_ne_zero_iff]
  · simp [finprod_of_infinite_mulSupport h₂]

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

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
v : α → M
s : Set α
⊢ span R (v '' s) ≤ (linearCombination R v ∘ₗ (supported R R s).subtype).range

Tactic:
LinearMap.range_comp,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ span R (v '' s) ≤ map (linearCombination R v) (supported R R s).subtype.range
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ rev ⁻¹' Ioi i = Iio i.rev

Tactic:
by ext; simp [lt_rev_iff]

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

Goal state before:
pp: M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
⊢ ∏ᶠ (x : α), 0 ≤ 1

Tactic:
by
  rw [← finprod_one (α := α)]
  by_cases H : (fun _ : α ↦ (0 : M)).HasFiniteMulSupport
  · exact finprod_le_finprod H (fun _ ↦ le_rfl) (by fun_prop) fun _ ↦ zero_le_one
  · rw [finprod_of_not_hasFiniteMulSupport H]
    exact finprod_one.symm.le

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
v : α → M
⊢ (Finsupp.linearCombination R v ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R R α).symm).range = span R (Set.range v)

Tactic:
LinearMap.range_comp,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ map (Finsupp.linearCombination R v) (↑(Finsupp.linearEquivFunOnFinite R R α).symm).range = span R (Set.range v)
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
rw [← finprod_mem_one s]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ s), 1
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr).range = span R (range f)

Tactic:
LinearMap.range_comp,

Goal state after:
M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ map (linearCombination R id) (lmapDomain R R f ∘ₗ ↑b.repr).range = span R (range f)
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ map (linearCombination R id) (lmapDomain R R f ∘ₗ ↑b.repr).range = span R (range f)

Tactic:
LinearMap.range_comp,

Goal state after:
M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ map (linearCombination R id) (map (lmapDomain R R f) (↑b.repr).range) = span R (range f)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
⊢ vecAppend ho u v = fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Tactic:
ext i
  rw [vecAppend, Fin.append, Function.comp_apply, Fin.addCases]
  congr with hi
  simp only [eq_rec_constant]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)

Tactic:
by
  classical
    by_cases hs : (s ∩ mulSupport (f ∘ g)).Finite
    · have hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y := by
        simpa only [hs.mem_toFinset]
      have := finprod_mem_eq_prod (comp f g) hs
      unfold Function.comp at this
      rw [this, ← Finset.prod_image hg]
      refine finprod_mem_eq_prod_of_inter_mulSupport_eq f ?_
      rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
    · unfold Function.comp at hs
      rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]
      rwa [image_inter_mulSupport_eq, infinite_image_iff hg]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
⊢ (Finsupp.lapply i) (Finsupp.single j (f j)) = 0

Tactic:
rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne' hji]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
simp [sub_modEq_iff_modEq_add]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v) l = ↑x
this : ↑(↑hv.linearCombinationEquiv l) = ↑x
⊢ ↑hv.linearCombinationEquiv l = x

Tactic:
exact Subtype.ext_iff.2 this

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ {n : ℕ} (x₀ : ℕ) (x : Fin n → ℕ),
    (∀ (a : Fin (∏ i, x i)), ⟨∑ i, (↑a / ∏ j, x (Fin.castLE ⋯ j)) % x i * ∏ j, x (Fin.castLE ⋯ j), ⋯⟩ = a) →
      ∀ (a : Fin (∏ i, Fin.cons x₀ x i)),
        ⟨∑ i, (↑a / ∏ j, Fin.cons x₀ x (Fin.castLE ⋯ j)) % Fin.cons x₀ x i * ∏ j, Fin.cons x₀ x (Fin.castLE ⋯ j), ⋯⟩ = a

Tactic:
· intro n x xs ih a
        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
        ext
        simp_rw [Fin.sum_univ_succ, Fin.cons_succ]
        have := fun i : Fin n =>
          Fintype.prod_equiv (finCongr <| Fin.val_succ i)
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Nat.succ_le_succ (Fin.is_lt _).le) j))
            fun j => rfl
        simp_rw [this]
        clear this
        simp_rw [Fin.val_zero, Fintype.prod_empty, Nat.div_one, mul_one, Fin.cons_zero,
          Fin.prod_univ_succ, Fin.castLE_zero, Fin.cons_zero, ← Nat.div_div_eq_div_mul,
          mul_left_comm (_ % _ : ℕ), ← mul_sum]
        convert! Nat.mod_add_div _ _
        exact ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq (Fin.prod_univ_succ _))

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

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
s : { s // LinearIndepOn R id s }
le : ↑(n + 1) ≤ #↑↑s
t : Finset ↑↑s
ht : n + 1 = t.card
⊢ ∃ s, s.card = n + 1 ∧ LinearIndepOn R id ↑s

Tactic:
exact ⟨t.map (.subtype _), by simpa using ht.symm, s.2.mono <| by simp⟩

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ t.encard

Tactic:
rw [← union_sdiff_cancel h, encard_union_eq disjoint_sdiff_right]; exact le_self_add

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

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
r : R
x✝ : S
this : (algebraMap R' S') (i r) = j ((algebraMap R S) r)
⊢ ↑j (r • x✝) = i r • ↑j x✝

Tactic:
simp only [smul_def, AddMonoidHom.coe_coe, map_mul, this]

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
p : Submodule R M
h : lift.{v, v'} (Module.rank R ↥(f ∘ₗ p.subtype).range) ≤ lift.{v', v} (Module.rank R ↥p)
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)

Tactic:
LinearMap.range_comp,

Goal state after:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
p : Submodule R M
h : lift.{v, v'} (Module.rank R ↥(Submodule.map f p.subtype.range)) ≤ lift.{v', v} (Module.rank R ↥p)
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R'
T : Type u'
inst✝⁶ : Module R R'
inst✝⁵ : NonAssocSemiring T
inst✝⁴ : Module R T
inst✝³ : Module R' T
inst✝² : IsScalarTower R' T T
inst✝¹ : FaithfulSMul R' T
inst✝ : IsScalarTower R R' T
⊢ Module.rank R R' ≤ Module.rank R T

Tactic:
by
  simpa using Module.lift_rank_bot_le_lift_rank_of_isScalarTower R R' T

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ s.encard ≤ t.encard

Tactic:
grw [← f_inj.encard_image, hf.image_subset]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case pos
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
heq : j = i
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j

Tactic:
subst heq

Goal state after:
case pos
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
I : Finset η
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
j : η
hnotMem : j ∉ I
h1 : ∀ i ∉ insert j I, x i = 1
h2 : ∀ i ∈ insert j I, Pi.mulSingle i (x i) ∈ H
⊢ x j = (Function.update x j 1 * Pi.mulSingle j (x j)) j
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case pos
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
heq : j = i
⊢ Function.update x i 1 j = 1

Tactic:
subst heq

Goal state after:
case pos
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
I : Finset η
x : (i : η) → f i
j : η
hj hnotMem : j ∉ I
h1 : ∀ i ∉ insert j I, x i = 1
h2 : ∀ i ∈ insert j I, Pi.mulSingle i (x i) ∈ H
⊢ Function.update x j 1 j = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Odd (insert a s).ncard ↔ Even s.ncard

Tactic:
by
  rw [ncard_insert_of_notMem ha hs, Nat.odd_add]
  simp only [← Nat.not_even_iff_odd, Nat.not_even_one, iff_false, Decidable.not_not]

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)
c d : A
⊢ ∑ i ∈ (b.repr c).support, z * ((b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) =
    ∑ i ∈ (b.repr d).support, (∑ i ∈ (b.repr c).support, z * (b.repr c) i • b i) * (b.repr d) i • b i

Tactic:
simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
        Finset.smul_sum, smul_mul_assoc, mul_smul_comm, (h.2 _ _).1,
        (@SMulCommClass.smul_comm R R A)]

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)
c d : A
⊢ ∑ x ∈ (b.repr c).support, ∑ x_1 ∈ (b.repr d).support, (b.repr c) x • (b.repr d) x_1 • (z * b x * b x_1) =
    ∑ x ∈ (b.repr d).support, ∑ x_1 ∈ (b.repr c).support, (b.repr c) x_1 • (b.repr d) x • (z * b x_1 * b x)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ ↑s

Tactic:
← ha

Goal state after:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ a • ↑s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ ↑s

Tactic:
← ha

Goal state after:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ op a • ↑s
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
⊢ m ∈ span R (range ⇑b) ↔ ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)

Tactic:
refine
    ⟨fun hm i => ⟨(b.restrictScalars R).repr ⟨m, hm⟩ i, b.restrictScalars_repr_apply R ⟨m, hm⟩ i⟩,
      fun h => ?_⟩
  rw [← b.linearCombination_repr m, Finsupp.linearCombination_apply S _]
  refine sum_mem fun i _ => ?_
  obtain ⟨_, h⟩ := h i
  simp_rw [← h, algebraMap_smul]
  exact smul_mem _ _ (subset_span (Set.mem_range_self i))

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
x : α
⊢ x ∈ insert (succ b) (Ioc a b) ↔ x ∈ Ioc a (succ b)

Tactic:
simp +contextual [or_and_left, le_succ_iff_eq_or_le, lt_succ_of_le_of_not_isMax h hb]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
⊢ Ioc a (pred b) = Ioo a b

Tactic:
by_cases hb : IsMin b

Goal state after:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : IsMin b
⊢ Ioc a (pred b) = Ioo a b

case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M : Type v
ι : Type x
inst✝⁶ : Semiring R
φ : ι → Type i
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : DecidableEq ι
inst✝² : Finite ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i
i : ι
x : φ i
⊢ f (Pi.single i x) = g (Pi.single i x)

Tactic:
convert! LinearMap.congr_fun (h i) x

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
by_cases hb : IsMin b

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : ¬IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (f j) c = update (fun i ↦ (f i) c) i (b c) j

Tactic:
update_of_ne h

Goal state after:
case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (f j) c = (f j) c
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ map (LinearMap.fst R M M₂) (snd R M M₂) = ⊥

Tactic:
by
  aesop (add simp snd)

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
⊢ {x ∈ antidiagonal n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅

Tactic:
ext ⟨a, b⟩

Goal state after:
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
⊢ (a, b) ∈ {x ∈ antidiagonal n | x.1 = m} ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case inr
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : m ≤ k
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

Tactic:
· have : n + 1 - k ≤ n + 1 - m := by
      rw [tsub_le_tsub_iff_left h]
      exact hkm
    simp only [hkm, Ico_eq_empty_of_le, prod_empty, Ico_eq_empty_of_le this]

Goal state after:
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ y = (a ∪ y) ∩ (b ∪ y)

Tactic:
rw [← inter_union_distrib_right, union_eq_self_of_subset_left xy]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
s : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
inst✝ : Nonempty ι
t : Set α
⊢ t ∈ ⨅ i, 𝓟 (s i) ↔ ∃ i, True ∧ s i ⊆ t

Tactic:
simpa only [true_and] using! mem_iInf_of_directed (h.mono_comp _ monotone_principal.dual) t

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝ : ∀ (j : ι), Nonempty (α j)
i : ι
f : Filter (α i)
⊢ (comap (eval i) f).NeBot ↔ f.NeBot

Tactic:
simp [comap_eval_neBot_iff', *]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e✝ e : α ≃ β
inst✝ : Mul β
⊢ let x := e.mul;
  α ≃* β

Tactic:
by
  intros
  exact
    { e with
      map_mul' := fun x y => by
        simp [mul_def] }

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

Goal state before:
pp: R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : Zero N
inst✝² : SMul R M
inst✝¹ : SMul R N
inst✝ : NoZeroSMulDivisors R N
f : M → N
hf : Injective f
h0 : f 0 = 0
hs : ∀ (c : R) (x : M), f (c • x) = c • f x
x✝¹ : R
x✝ : M
h : x✝¹ • x✝ = 0
⊢ x✝¹ • f x✝ = 0

Tactic:
rw [← hs, h, h0]

Goal state after: