mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
⊢ Irreducible (y * ↑u) ↔ Irreducible y

Tactic:
simp only [irreducible_iff, Units.isUnit_mul_units, and_congr_right_iff]
  refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩
  · rw [← u.isUnit_mul_units B]
    apply h
    rw [← mul_assoc, ← HAB]
  · rw [← u⁻¹.isUnit_mul_units B]
    apply h
    rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]

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

Goal state before:
pp: M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
p q : M
pp : Prime p
qp : Prime q
⊢ p ∣ q ↔ p = q

Tactic:
rw [pp.dvd_prime_iff_associated qp, ← associated_eq_eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b

Tactic:
simp only [DvdNotUnit, mk_ne_zero, mk_surjective.exists, isUnit_mk, mk_mul_mk,
    mk_eq_mk_iff_associated, Associated.comm (x := b)]
  refine Iff.rfl.and ?_
  constructor
  · rintro ⟨x, hx, u, rfl⟩
    refine ⟨x * u, ?_, mul_assoc ..⟩
    simpa
  · rintro ⟨x, ⟨hx, rfl⟩⟩
    use x

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⊤
p p' : Submodule R₂ M₂
H : comap f p ≤ comap f p'
⊢ p ≤ p'

Tactic:
SetLike.le_def,

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 : f.range = ⊤
p p' : Submodule R₂ M₂
H : comap f p ≤ comap f p'
⊢ ∀ ⦃x : M₂⦄, x ∈ p → x ∈ p'
Module: Mathlib.Order.SupClosed

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F β α
inst✝ : SupHomClass F β α
hs : SupClosed s
f : F
a : β
ha : a ∈ ⇑f ⁻¹' s
b : β
hb : b ∈ ⇑f ⁻¹' s
⊢ a ⊔ b ∈ ⇑f ⁻¹' s

Tactic:
by simpa [map_sup] using hs ha hb

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
v₀ : M
⊢ s ≤ R ∙ v₀ ↔ ∀ v ∈ s, ∃ r, r • v₀ = v

Tactic:
SetLike.le_def,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
v₀ : M
⊢ (∀ ⦃x : M⦄, x ∈ s → x ∈ R ∙ v₀) ↔ ∀ v ∈ s, ∃ r, r • v₀ = v
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
this : (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) = b
⊢ b ≤ sSup {a | IsAtom a ∧ a ≤ b}

Tactic:
rw [← this]

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
this : (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) = b
⊢ (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) ≤ sSup {a | IsAtom a ∧ a ≤ ⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ}
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h✝ : IsEmpty ι
⊢ ⨆ i, f i ∈ s

pp: case inr
ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h✝ : Nonempty ι
⊢ ⨆ i, f i ∈ s

Tactic:
· simpa [iSup_of_empty]

Goal state after:
case inr
ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h✝ : Nonempty ι
⊢ ⨆ i, f i ∈ s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h✝ : Nonempty ι
⊢ ⨆ i, f i ∈ s

Tactic:
· exact hs.iSup_mem_of_nonempty hf

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

Goal state before:
pp: R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h : ∀ y ∈ s, Commute y x
⊢ ∀ y ∈ span R s, Commute y x

Tactic:
by
  intro y hy
  induction hy using span_induction with
  | mem _ _ => aesop
  | zero => exact .zero_left _
  | add _ _ _ _ h₁ h₂ => exact h₁.add_left h₂
  | smul _ _ _ h => exact h.smul_left _

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderTop α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyAtomic αᵒᵈ

Tactic:
exact Lattice.isStronglyAtomic

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s

Tactic:
by
  classical
    rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]
    constructor
    · intro H ι s hs
      obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
      have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
      choose f hf using this
      refine ⟨Finset.univ.image f, ht'.trans ?_⟩
      rw [Finset.sup_le_iff]
      intro b hb
      rw [← show s (f ⟨b, hb⟩) = id b from hf _]
      exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
    · intro H s hs
      obtain ⟨t, ht⟩ :=
        H s Subtype.val
          (by
            delta iSup
            rwa [Subtype.range_coe])
      refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
      rw [Finset.sup_le_iff]
      exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
⊢ 0 • x ∈ span R (s • t)

Tactic:
by rw [zero_smul]; exact zero_mem _

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

Goal state before:
pp: case intro
I : Type u_7
inst✝³ : DecidableEq I
M : I → Type u_8
inst✝² : (i : I) → CommMonoid (M i)
inst✝¹ : Finite I
N : Type u_9
inst✝ : CommMonoid N
g h : ((i : I) → M i) →* N
H : ∀ (i : I) (x : M i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → M i
⊢ g (∏ i, Pi.mulSingle i (k i)) = h (∏ i, Pi.mulSingle i (k i))

Tactic:
map_prod,

Goal state after:
case intro
I : Type u_7
inst✝³ : DecidableEq I
M : I → Type u_8
inst✝² : (i : I) → CommMonoid (M i)
inst✝¹ : Finite I
N : Type u_9
inst✝ : CommMonoid N
g h : ((i : I) → M i) →* N
H : ∀ (i : I) (x : M i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → M i
⊢ ∏ x, g (Pi.mulSingle x (k x)) = h (∏ i, Pi.mulSingle i (k i))
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ IsIdempotentElem (f 1) ↔ IsIdempotentElem f

Tactic:
rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, IsIdempotentElem,
    LinearMap.ext_iff]
  simp_rw [Module.End.mul_apply]
  exact ⟨fun h r ↦ by rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h], (· 1)⟩

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

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

Tactic:
· rw [← mem_range] at hnk
    rw [prod_eq_zero hnk, prod_eq_zero hnk] <;> simp

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : s = a
⊢ (erase a (f + f')) s = (erase a f + erase a f') s

pp: case neg
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : ¬s = a
⊢ (erase a (f + f')) s = (erase a f + erase a f') s

Tactic:
· rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : ¬s = a
⊢ (erase a (f + f')) s = (erase a f + erase a f') s
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a a' : α
f : α →₀ M
⊢ (erase a f) a' = if a' = a then 0 else f a'

Tactic:
rw [erase, coe_mk]

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a a' : α
f : α →₀ M
⊢ (if a' = a then 0 else f a') = if a' = a then 0 else f a'
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
⊢ ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)

Tactic:
convert! add_single using 7 with _ _ _ H

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
a✝⁴ : ι
a✝³ : M
a✝² : ι →₀ M
H : ∀ c ∈ a✝².support, c < a✝⁴
a✝¹ : a✝³ ≠ 0
a✝ : motive a✝²
⊢ single a✝⁴ a✝³ + a✝² = a✝² + single a✝⁴ a✝³
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : α → M
g : α → M → N
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
hg : ∀ (a : α), g a 0 = 1
⊢ ∀ x ∈ s, x ∉ (onFinset s f hf).support → g x ((onFinset s f hf) x) = 1

Tactic:
simp +contextual [*]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ g y (f y) * ∏ a ∈ (erase y f).support, g a ((erase y f) a) = ∏ a ∈ f.support, g a (f a)

Tactic:
← Finset.mul_prod_erase _ _ hyf,

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ g y (f y) * ∏ a ∈ (erase y f).support, g a ((erase y f) a) = g y (f y) * ∏ x ∈ f.support.erase y, g x (f x)
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
f g : ι → M₀
hg : ∀ (x : ι), g x ≠ 0
⊢ (support fun x ↦ f x * g x) = support f

Tactic:
simp [support_eq_univ hg]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = (Multiset.map (fun g ↦ g.sum h) s).sum
⊢ (a ::ₘ s).sum.sum h = (Multiset.map (fun g ↦ g.sum h) (a ::ₘ s)).sum

Tactic:
by
    rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0

Tactic:
simp_rw [graph, mem_map, mem_support_iff]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_1 = (a, m)) ↔ f a = m ∧ m ≠ 0
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 M
f : α ≃ β
l : α →₀ M
a : β
⊢ a ∈ map f.toEmbedding l.support ↔ l (f.symm a) ≠ 0

Tactic:
simp only [Finset.mem_map_equiv, mem_support_toFun]; rfl

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
S : Set α
f : α → β
hf : Set.InjOn f S
⊢ Set.InjOn (mapDomain f) {w | ↑w.support ⊆ S}

Tactic:
by
  intro v₁ hv₁ v₂ hv₂ eq
  ext a
  classical
    by_cases h : a ∈ v₁.support ∪ v₂.support
    · rw [← mapDomain_apply' S _ hv₁ hf _, ← mapDomain_apply' S _ hv₂ hf _, eq] <;>
        · apply Set.union_subset hv₁ hv₂
          exact mod_cast h
    · simp_all

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

Tactic:
rw [Subsingleton.elim D] <;> rfl

Goal state after:
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
ha : a ∈ (f ::ₘ s).sum.support
h : a ∉ f.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
simp_rw [Multiset.sum_cons, mem_support_iff, add_apply, notMem_support_iff.1 h,
          zero_add] at ha

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 : s.sum a ≠ 0
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), #({b ∈ B | a ∈ b}) ≤ n
⊢ ∑ s ∈ B, #s = ∑ s ∈ B, #(univ ∩ s)

Tactic:
simp_rw [univ_inter]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), n ≤ #({b ∈ B | a ∈ b})
⊢ ∑ s ∈ B, #(univ ∩ s) = ∑ s ∈ B, #s

Tactic:
simp_rw [univ_inter]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∀ i ∈ s, f i = 1 → f i ≤ 1

Tactic:
exact fun _ _ ↦ le_of_eq

Goal state after:
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 : α → β
x : α →₀ M
a : α
⊢ (mapDomain f x) (f a) = ∑ i ∈ x.support with f i = f a, x i

Tactic:
simp [mapDomain, sum, single_apply, Finset.sum_ite]

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
⊢ supported R R s = span R ((fun i ↦ single i 1) '' s)

Tactic:
refine (span_eq_of_le _ ?_ (SetLike.le_def.2 fun l hl => ?_)).symm
  · rintro _ ⟨_, hp, rfl⟩
    exact single_mem_supported R 1 hp
  · rw [← l.sum_single]
    refine sum_mem fun i il => ?_
    rw [show single i (l i) = l i • single i 1 by simp]
    exact smul_mem _ (l i) (subset_span (mem_image_of_mem _ (hl il)))

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

Goal state before:
pp: case pos
α : 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.sum fun a ↦ single (f a)) = 0
x : α
this : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
⊢ l x = 0 x

Tactic:
have : Finsupp.sum l (fun a => Finsupp.single (f a)) (f x) = 0 := by
      rw [h₂]
      rfl
    rw [Finsupp.sum_apply, Finsupp.sum_eq_single x, single_eq_same] at this
    · simpa
    · intro y hy xy
      simp only [SetLike.mem_coe, mem_supported, subset_def, mem_support_iff] at h₁
      simp [mt (H _ (h₁ _ hy) _ xs) xy]
    · simp +contextual

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Ico ↑i ↑j ⊆ Iio n

Tactic:
exact fun k hk ↦ hk.2.trans j.is_lt

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Ioo ↑i ↑j ⊆ Iio n

Tactic:
exact fun k hk ↦ hk.2.trans j.is_lt

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

Goal state before:
pp: ι : 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
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ ↑b.repr = f_i
⊢ (b.repr x) i = f_i x

Tactic:
rw [← this]

Goal state after:
ι : 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
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ ↑b.repr = f_i
⊢ (b.repr x) i = (lapply i ∘ₗ ↑b.repr) x
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ 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
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
this : Module R' R := compHom R ↑f.symm
x : R'
y : R
z : M
⊢ (x • y) • z = x • y • z

Tactic:
by
        change (f.symm x * y) • z = x • (y • z)
        rw [mul_smul, ← h, f.apply_symm_apply]

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

Goal state before:
pp: case inl
ι : 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
i : ι
h : b i ∈ range ⇑b
h✝ : Subsingleton R
this : Subsingleton M := Module.subsingleton R M
⊢ b.reindexRange ⟨b i, h⟩ = b i

Tactic:
simp [reindexRange, eq_iff_true_of_subsingleton]

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

Goal state before:
pp: x y : ℕ∞
⊢ x ^ y = if y < ⊤ then x ^ y.toNat else if x = 0 then 0 else if x = 1 then 1 else ⊤

Tactic:
cases y with
  | top => simp only [lt_self_iff_false, ↓reduceIte]; rfl
  | coe n => simp only [natCast_lt_top, ↓reduceIte, toNat_natCast]; rfl

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
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (f g : ι → R), ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g i

Tactic:
linearIndependent_iff_injective_fintypeLinearCombination,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ Injective ⇑(Fintype.linearCombination R v) ↔ ∀ (f g : ι → R), ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
⊢ f 0 = 0

Tactic:
by simp [f]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v

Tactic:
simp_rw [LinearIndependent, Finsupp.linearCombination_linear_comp, coe_comp]

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ Injective (⇑f ∘ ⇑(Finsupp.linearCombination R v)) ↔ Injective ⇑(Finsupp.linearCombination R v)
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
⊢ m • z • p = z • b - z • a

Tactic:
rw [← zsmul_sub, ← h, ← mul_zsmul, ← mul_zsmul']

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
⊢ k = k / m * (m / n * n)

Tactic:
Nat.div_mul_cancel hkn,

Goal state after:
case inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
⊢ k = k / m * m
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
⊢ i = j

Tactic:
rcases (Finsupp.single_eq_single_iff ..).mp h_single_eq with (⟨H, _⟩ | ⟨hc, _⟩)

Goal state after:
case inl
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
H : i = j
right✝ : c = d
⊢ i = j

case inr
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc✝ : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
hc : c = 0
right✝ : d = 0
⊢ i = j
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) = (Finsupp.linearCombination R v) l
this : ↑hv.linearCombinationEquiv l = x
⊢ hv.repr x = hv.linearCombinationEquiv.symm (hv.linearCombinationEquiv l)

Tactic:
rw [← this]

Goal state after:
ι : 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) = (Finsupp.linearCombination R v) l
this : ↑hv.linearCombinationEquiv l = x
⊢ hv.repr (↑hv.linearCombinationEquiv l) = hv.linearCombinationEquiv.symm (hv.linearCombinationEquiv l)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
this : s ∪ t = t
⊢ s ⊆ t

Tactic:
rw [← this]

Goal state after:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
this : s ∪ t = t
⊢ s ⊆ s ∪ t