mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∀ (i : Finset α), (↑i ⊆ range fun x ↦ f ↑x) → a ⊓ i.sup id = ⊥

Tactic:
intro u hu

Goal state after:
α : 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
⊢ a ⊓ u.sup id = ⊥
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l ++ List.map (cons a) (powersetAux' l)).zip
      ((List.map (cons a) (powersetAux' l)).reverse ++ (powersetAux' l).reverse) ~
    List.map (Prod.map id (cons a)) ((powersetAux' l).zip (powersetAux' l).reverse) ++
      List.map (Prod.map (cons a) id) ((powersetAux' l).zip (powersetAux' l).reverse)

Tactic:
← zip_map,

Goal state after:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l ++ List.map (cons a) (powersetAux' l)).zip
      ((List.map (cons a) (powersetAux' l)).reverse ++ (powersetAux' l).reverse) ~
    (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++
      List.map (Prod.map (cons a) id) ((powersetAux' l).zip (powersetAux' l).reverse)
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l ++ List.map (cons a) (powersetAux' l)).zip
      ((List.map (cons a) (powersetAux' l)).reverse ++ (powersetAux' l).reverse) ~
    (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++
      List.map (Prod.map (cons a) id) ((powersetAux' l).zip (powersetAux' l).reverse)

Tactic:
← zip_map,

Goal state after:
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (powersetAux' l ++ List.map (cons a) (powersetAux' l)).zip
      ((List.map (cons a) (powersetAux' l)).reverse ++ (powersetAux' l).reverse) ~
    (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++
      (List.map (cons a) (powersetAux' l)).zip (List.map id (powersetAux' l).reverse)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
by
    by_cases h : { c : α | IsCompactElement c ∧ c ≤ b } ⊆ {⊥}
    · left
      rw [← sSup_compact_le_eq b, sSup_eq_bot]
      exact h
    · rcases Set.not_subset.1 h with ⟨c, ⟨hc, hcb⟩, hcbot⟩
      right
      have hc' := CompleteLattice.Iic_coatomic_of_compact_element hc
      rw [← isAtomic_iff_isCoatomic] at hc'
      obtain con | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le (⟨c, le_refl c⟩ : Set.Iic c)
      · exfalso
        apply hcbot
        simp only [Subtype.ext_iff, Set.Iic.coe_bot] at con
        exact con
      rw [← Subtype.coe_le_coe, Subtype.coe_mk] at hac
      exact ⟨a, ha.of_isAtom_coe_Iic, hac.trans hcb⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
hg : g a = 0
⊢ 0 = g a

Tactic:
hg

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
hf : f a = 0
hg : g a = 0
⊢ 0 = 0
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
h : a ∉ f.support
⊢ f a = g a

Tactic:
have hf : f a = 0 := notMem_support_iff.1 h
        have hg : g a = 0 := by rwa [h₁, notMem_support_iff] at h
        rw [hf, hg]

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
⊢ e.symm 0 = 0

Tactic:
by simp [← hf]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ (single a b) a' = 0

Tactic:
classical exact Pi.single_eq_of_ne' h _

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
hfg : f ≠ g
⊢ Nonempty α ∧ Nontrivial M

Tactic:
obtain ⟨a, ha⟩ := ne_iff.mp hfg

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f g : α →₀ M
hfg : f ≠ g
a : α
ha : f a ≠ g a
⊢ Nonempty α ∧ Nontrivial M
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
⊢ motive f

Tactic:
· have hs' : (erase a f).support = s := by
      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
    rw [← single_add_erase a f]
    refine single_add _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')
    rw [← mem_support_iff, hs]
    exact mem_insert_self a s

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case neg
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ i, s i
⊢ 1 ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
← h1

Goal state after:
case neg
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ i, s i
⊢ ⊥ ≤ (⨆ i, (s i).mulIndicator (f i)) a
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
ι : Type u_3
inst✝ : Finite α
f : ι → α → M
hf : ∀ (a : α), HasFiniteMulSupport fun x ↦ f x a
⊢ HasFiniteMulSupport f

Tactic:
simp only [HasFiniteMulSupport] at hf ⊢
  refine (Set.finite_iUnion hf).subset fun i hi ↦ ?_
  simp only [mem_mulSupport, Set.mem_iUnion] at hi ⊢
  exact ne_iff.mp hi

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

Tactic:
rw [mapDomain_of_notMem_range, embDomain_of_notMem_range] <;> assumption

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
b : β
hb : b ∉ Set.range ⇑f
hg : g b = 0
⊢ 0 = g b

Tactic:
hg

Goal state after:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
b : β
hb : b ∉ Set.range ⇑f
hg : g b = 0
⊢ 0 = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
⊢ mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) l) = erase 0 l

Tactic:
refine .trans ?_ (mapDomain_comapDomain _ (add_left_injective 1) _ fun _ ↦ ?_)
  · congr; ext; simp
  · simp_all [Nat.pos_iff_ne_zero]

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

Goal state before:
pp: case h
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ insert i s ⊆ t

Tactic:
simp [Finset.insert_subset_iff, h, ht]

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
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : Zero N
g : (i : ι) → (αs i →₀ M) → N
hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0
i : ι
⊢ l.split i = 0 ↔ g i (l.split i) = 0

Tactic:
hg

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
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : Zero N
g : (i : ι) → (αs i →₀ M) → N
hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0
i : ι
⊢ g i (l.split i) = 0 ↔ g i (l.split i) = 0
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : CommMonoid N
inst✝¹ : MulDistribMulAction M N
ι : Sort u_4
inst✝ : Finite ι
f : ι → N
r : M
⊢ r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x

Tactic:
by
  cases nonempty_fintype (PLift ι)
  simp only [finprod_eq_prod_plift_of_mulSupport_subset (s := Finset.univ) (by simp),
    Finset.smul_prod']

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
i' : ι'
⊢ (b.repr ≪≫ₗ Finsupp.domLCongr e).symm (single i' 1) = b.repr.symm (single (e.symm i') 1)

Tactic:
rw [LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single]

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

Goal state before:
pp: α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
⊢ f a ∣ finprod f

Tactic:
by_cases ha : a ∈ mulSupport f
  · rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)]
    exact Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)
  · rw [notMem_mulSupport.mp ha]
    exact one_dvd (finprod f)

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
p : Submodule R M
h : range ⇑b ⊆ ↑p
⊢ p = ⊤

Tactic:
simpa using span_mono (R := R) h

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

Goal state before:
pp: case coe.top.inl
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_0 : x < 1
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

Tactic:
exact (h (Order.lt_one_iff.1 x_0)).rec

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
⊢ f i = g i

Tactic:
by
      have h :=
        hv (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i)) <| by
          simpa only [map_sum, Finsupp.linearCombination_single] using eq
      have (f : ι → R) : f i = (∑ j ∈ s, Finsupp.single j (f j)) i :=
        calc
          f i = (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single i (f i)) := by
            { rw [Finsupp.lapply_apply, Finsupp.single_eq_same] }
          _ = ∑ j ∈ s, (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single j (f j)) :=
            Eq.symm <|
              Finset.sum_eq_single i
                (fun j _hjs hji => by rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne' hji])
                fun hnis => hnis.elim his
          _ = (∑ j ∈ s, Finsupp.single j (f j)) i := (map_sum ..).symm
      rw [this f, this g, h]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
⊢ (List.ofFn f).prod = ∏ i, f i

Tactic:
simp [prod_eq_multiset_prod]

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
⊢ LinearIndependent R v ↔
    ∀ (s : Finset ι) (f g : ι → R),
      (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i

Tactic:
by
  classical
  exact linearIndependent_iff'ₛ.trans
    ⟨fun H s f g eq hv i ↦ if his : i ∈ s then H s f g hv i his else eq i his,
      fun H s f g eq i hi ↦ by
      convert!
        H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
          (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i <;>
      exact (if_pos hi).symm⟩

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

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
a b p : M
inst✝ : IsAddTorsionFree M
n : ℕ
hn : n ≠ 0
⊢ n • a ≡ n • b [PMOD n • p] ↔ a ≡ b [PMOD p]

Tactic:
by
  simp only [modEq_iff_nsmul, ← mul_nsmul _ n, mul_nsmul' _ n, ← nsmul_add, nsmul_right_inj hn]

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))
⊢ Injective (⇑f ∘ ⇑(Finsupp.linearCombination R v)) ↔ Injective ⇑(Finsupp.linearCombination R v)

Tactic:
rw [hf_inj.injective_iff]

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))
⊢ Set.range ⇑(Finsupp.linearCombination R v) ⊆ ↑(span R (Set.range v))
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ r₂ : ι → R'
H : ∑ i ∈ S, r₁ i • (⇑j ∘ v) i = ∑ i ∈ S, r₂ i • (⇑j ∘ v) i
s : ι
hs : s ∈ S
⊢ r₁ s = r₂ s

Tactic:
comp_apply,

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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ r₂ : ι → R'
s : ι
hs : s ∈ S
H : ∑ x ∈ S, r₁ x • j (v x) = ∑ x ∈ S, r₂ x • j (v x)
⊢ r₁ s = r₂ s
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc < j

pp: case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc.castSucc < j.succ

Tactic:
· assumption

Goal state after:
case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc.castSucc < j.succ
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ a = b

Tactic:
by
  apply Int.ofNat.inj
  rw [eq_comm, ← sub_eq_zero]
  exact Int.eq_zero_of_abs_lt_dvd h.dvd h2

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
H : ∑ i ∈ S, r' i • (⇑j ∘ v) i = 0
s : ι
hs : s ∈ S
⊢ r' s = 0

Tactic:
comp_apply,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
s : ι
hs : s ∈ S
H : ∑ x ∈ S, r' x • j (v x) = 0
⊢ r' s = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
v : Fin m → M
x : M
hli : LinearIndependent R v
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
⊢ LinearIndependent R fun i ↦ Fin.cons x v ((finRotate (m + 1)) i)

Tactic:
← Function.comp_def

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
v : Fin m → M
x : M
hli : LinearIndependent R v
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
⊢ LinearIndependent R (Fin.cons x v ∘ ⇑(finRotate (m + 1)))
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
⊢ ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Tactic:
hg

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 : 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 ∈ s, g i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case inl
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj✝ : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
x : ι
hx : x ∈ s
⊢ v ↑⟨x, ⋯⟩ = ((Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x) ∘ ⇑(Equiv.Set.union hdj)) ⟨x, ⋯⟩

Tactic:
comp_apply,

Goal state after:
case inl
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj✝ : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
x : ι
hx : x ∈ s
⊢ v ↑⟨x, ⋯⟩ = Sum.elim (fun x ↦ v ↑x) (fun x ↦ v ↑x) ((Equiv.Set.union hdj) ⟨x, ⋯⟩)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case inr
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj✝ : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
x : ι
hx : x ∈ t
⊢ v ↑⟨x, ⋯⟩ = ((Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x) ∘ ⇑(Equiv.Set.union hdj)) ⟨x, ⋯⟩

Tactic:
comp_apply,

Goal state after:
case inr
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj✝ : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
x : ι
hx : x ∈ t
⊢ v ↑⟨x, ⋯⟩ = Sum.elim (fun x ↦ v ↑x) (fun x ↦ v ↑x) ((Equiv.Set.union hdj) ⟨x, ⋯⟩)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case insert
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
⊢ ∑ i ∈ insert a s, g i • ⇑i = 0 → ∀ i ∈ insert a s, g i = 0

Tactic:
hg

Goal state after:
case insert
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
⊢ ∀ i ∈ insert a s, g i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ s, g i * i x * i y - ∑ i ∈ s, g i * a x * i y =
    ∑ i ∈ insert a s, g i * i x * i y - ∑ i ∈ insert a s, g i * a x * i y

Tactic:
by simp [Finset.sum_insert has]

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ (∑ i ∈ insert a s, g i • ⇑i) (x * y) - a x * (∑ i ∈ insert a s, g i • ⇑i) y = 0

Tactic:
hg

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ 0 (x * y) - a x * 0 y = 0