mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
⊢ ∀ (x y : M₁),
    ↑e ∘ₗ codRestrict i.range (f (x + y)) ⋯ = ↑e ∘ₗ codRestrict i.range (f x) ⋯ + ↑e ∘ₗ codRestrict i.range (f y) ⋯

Tactic:
intro x₁

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
x₁ : M₁
⊢ ∀ (y : M₁),
    ↑e ∘ₗ codRestrict i.range (f (x₁ + y)) ⋯ = ↑e ∘ₗ codRestrict i.range (f x₁) ⋯ + ↑e ∘ₗ codRestrict i.range (f y) ⋯
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a : α
⊢ ⊥ ⋖ a ↔ IsAtom a

Tactic:
simp only [CovBy, bot_lt_iff_ne_bot, IsAtom, not_imp_not]

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := ⋯
⊢ p ≤ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

Tactic:
intro m hm
    by_cases h : m = 0
    · rw [h]
      simp
    · exact @le_sSup _ _ S _ ⟨m, ⟨hm, ⟨h, rfl⟩⟩⟩ m (mem_span_singleton_self m)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ lowerBounds s
⊢ ⊤ ≤ if ⊥ ∈ s then ⊥ else ⊤

Tactic:
rw [if_neg]
          intro con
          exact top_ne_bot (eq_bot_iff.2 (h con))

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
⊢ (map g s).SupIndep f ↔ s.SupIndep (f ∘ ⇑g)

Tactic:
refine ⟨fun hs t ht i hi hit => ?_, fun hs => ?_⟩

Goal state after:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : (map g s).SupIndep f
t : Finset ι'
ht : t ⊆ s
i : ι'
hi : i ∈ s
hit : i ∉ t
⊢ Disjoint ((f ∘ ⇑g) i) (t.sup (f ∘ ⇑g))

case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : Lattice α
inst✝ : OrderBot α
f : ι → α
s : Finset ι'
g : ι' ↪ ι
hs : s.SupIndep (f ∘ ⇑g)
⊢ (map g s).SupIndep f
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ (∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)) ↔
    Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 2 ⊔ f 0) ∧ Disjoint (f 2) (f 0 ⊔ f 1)

Tactic:
sup_comm (f 2) (f 0)

Goal state after:
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ (∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)) ↔
    Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (f ∘ Subtype.val) ↔ s.SupIndep f

Tactic:
classical
    rw [Finset.supIndep_iff_disjoint_erase]
    refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
    rw [Finset.sup_eq_iSup]
    congr! 1
    refine iSup_subtype.trans ?_
    congr! 1
    simp [iSup_and, @iSup_comm _ (_ ∈ s)]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f g : ι → α
h₁ : iSupIndep g
h₂ : iSup f = ⊤
⊢ f ≤ g ↔ f = g

Tactic:
refine ⟨fun h₃ ↦ funext fun i ↦ ?_, le_of_eq⟩

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f g : ι → α
h₁ : iSupIndep g
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
⊢ f i = g i
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
h : ¬a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
a : α
f : α → β → M
b : β
⊢ s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
a : α
f : α → β → M
b : β
h : a ∈ s
⊢ s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a

case neg
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
a : α
f : α → β → M
b : β
h : ¬a ∈ s
⊢ s.mulIndicator f a b = s.mulIndicator (fun i ↦ f i b) a
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ {i | t i ≠ ⊥}.Finite

Tactic:
by
  refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn
  exact WellFoundedLT.finite_of_sSupIndep ht.sSupIndep_range

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

Goal state before:
pp: ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
⊢ Set.EqOn (fun b ↦ ∏ i ∈ v, f i b) (fun b ↦ ∏ i ∈ v, f' i b) s

Tactic:
by
  convert! eqOn_finsetProd h v <;> simp

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

Goal state before:
pp: case h
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ a ∉ {x}

Tactic:
rw [Set.mem_singleton_iff]

Goal state after:
case h
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ ¬a = x
Module: Mathlib.Data.List.Find

Goal state before:
pp: α : Type u_1
p₁ p₂ : α → Bool
l : List α
h : ∀ (x : α), x ∈ l → p₁ x = p₂ x
⊢ find? p₁ l = find? p₂ l

Tactic:
by
  induction l with grind

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
ι : Type u_8
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
hp : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
obtain ⟨k, hk⟩ := hs

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
⊢ ⨆ i ∈ s, comap f (p i) = ⊤
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝² : DecidablePred p
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
s : Multiset α
hp₁ : {x | x ∈ s ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ s → (p₁ x ↔ p₂ x)
⊢ {x | x ∈ s ∧ p₂ x}.Subsingleton

Tactic:
simp_rw +contextual [← exists_prop, ← h, exists_prop, hp₁]

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

Tactic:
rw [hf, hg]

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

Goal state before:
pp: case inr
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i / n * n

Tactic:
refine sum_congr rfl fun s hs ↦ ?_

Goal state after:
case inr
ι : Type u_5
s✝ : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s✝, n ∣ f i
hn : n > 0
s : ι
hs : s ∈ s✝
⊢ f s = f s / n * n
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case inr
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i / n * n

Tactic:
refine sum_congr rfl fun s hs ↦ ?_

Goal state after:
case inr
ι : Type u_5
s✝ : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s✝, n ∣ f i
hn : n ≠ 0
s : ι
hs : s ∈ s✝
⊢ f s = f s / n * n
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f : M → N
hf : f 0 = 0
hf' : ∀ (x y : M), f (x + y) = f x + f y
v₁ v₂ : ι →₀ M
x✝ : ι
⊢ (mapRange f hf (v₁ + v₂)) x✝ = (mapRange f hf v₁ + mapRange f hf v₂) x✝

Tactic:
simp only [hf', add_apply, mapRange_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
⊢ ∃ x, l = single x b ∧ f x = a

Tactic:
have h_map_support : Finset.map f l.support = {a} := by
      rw [← support_embDomain, h, support_single _ hb]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
⊢ ∃ x, l = single x b ∧ f x = a
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: case h.left
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
⊢ l = single c b

Tactic:
ext d
      rw [← embDomain_apply_self f l, h]
      grind

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
⊢ (s.indicator fun i ↦ f i * g i) = fun i ↦ s.indicator f i * s.indicator g i

Tactic:
funext
  simp only [indicator]
  split_ifs
  · rfl
  rw [mul_zero]

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
x✝ : ι
⊢ x✝ ∈ s ↔ x✝ ∈ t

Tactic:
← indicator_eq_one_iff_mem M₀,

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
x✝ : ι
⊢ s.indicator 1 x✝ = 1 ↔ t.indicator 1 x✝ = 1
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MonoidWithZero M₀
inst✝ : IsReduced M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
⊢ (support fun a ↦ f a ^ n) = support f

Tactic:
by
  ext; exact (pow_eq_zero_iff hn).not

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ -↑u • x = -(u • x)

Tactic:
_root_.neg_smul,

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ -(↑u • x) = -(u • x)
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inl
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ 1 < (v x)⁻¹

Tactic:
exact (one_lt_inv₀ <| v.pos hx₀).mpr h

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

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ x a = 0 → (single (f a) 0) (f a) = 0

Tactic:
· intro _
    rw [single_zero, coe_zero, Pi.zero_apply]

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, ¬z = a → Disjoint (f z) (f a)) ∧
      ∀ (a : β), (a ∈ i → ¬a = z → Disjoint (f a) (f z)) ∧ (a ∈ i → ∀ a_2 ∈ i, ¬a = a_2 → Disjoint (f a) (f a_2))

Tactic:
forall_and,

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, ¬z = a → Disjoint (f z) (f a)) ∧
      (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ ∀ x ∈ i, ∀ a ∈ i, ¬x = a → Disjoint (f x) (f a)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
l : ↥(supported M R s)
a : α
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
l : ↥(supported M R s)
a : α
h : a ∈ s
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a

case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
l : ↥(supported M R s)
a : α
h : a ∉ s
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a
Module: Mathlib.LinearAlgebra.Finsupp.Supported

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

Tactic:
by
  rw [Set.inter_eq_iInter, supported_iInter, iInf_bool_eq]; rfl

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

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

Tactic:
rw [← preimage_val_Iio_val, image_preimage_eq_inter_range, range_val, inter_eq_left]

Goal state after:
n : ℕ
i : Fin n
⊢ Iio ↑i ⊆ Iio n
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case h₂
α : 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 α
⊢ map (linearCombination R v) (supported R R s) ≤ span R (v '' s)

Tactic:
· refine map_le_iff_le_comap.2 fun z hz => ?_
    have : ∀ i, z i • v i ∈ span R (v '' s) := by
      intro c
      have := Classical.decPred fun x => x ∈ s
      by_cases h : c ∈ s
      · exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))
      · simp [(Finsupp.mem_supported' R _).1 hz _ h]
    rw [mem_comap, linearCombination_apply]
    refine sum_mem ?_
    simp [this]

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 t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
apply finprod_mem_inter_mulSupport_eq
  ext x
  exact and_congr_left (h x)

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

Goal state before:
pp: ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
| (b.repr x) i

Tactic:
← b'.sum_repr x

Goal state after:
ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
| (b.repr (∑ i, (b'.repr x) i • b' i)) i
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Ici a) = Ico (↑a) n

Tactic:
by
  rw [← attachFin_Ico_eq_Ici, map_valEmbedding_attachFin]

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∈ s
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a

case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∉ s
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ (a + b).rev = a.rev - b

Tactic:
← last_sub,

Goal state after:
case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ last n✝ - (a + b) = a.rev - b
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ last n✝ - (a + b) = a.rev - b

Tactic:
← last_sub,

Goal state after:
case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ last n✝ - (a + b) = last n✝ - a - b
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∈ s
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r

case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
h : a ∉ s
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ (∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) →
    ∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i

Tactic:
rintro hv f g hfg i

Goal state after:
case mpr
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
hv : ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ↑↑s → R
hfg : ∑ i, f i • v ↑i = ∑ i, g i • v ↑i
i : ↑↑s
⊢ f i = g i
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ m.Coprime n ↔ IsRelPrime m n

Tactic:
coprime_iff_gcd_eq_one,

Goal state after:
m n : ℕ
⊢ m.gcd n = 1 ↔ IsRelPrime m n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m.gcd n → d ∣ 1

Tactic:
exact ⟨fun h _ ↦ (h ▸ ·), (dvd_one.mp <| · dvd_rfl)⟩

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

Goal state before:
pp: case succ.succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝¹ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝¹ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n✝ : ℕ
fn : Fin (n✝ + 1)
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * (n✝ + 1)

Tactic:
refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_

Goal state after:
case succ.succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝¹ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝¹ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n✝ : ℕ
fn : Fin (n✝ + 1)
⊢ ∏ i, n i + n✝ * ∏ j, n j = (∏ i, n i) * (n✝ + 1)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑(n.gcd m) * ↑a + (↑n * n.gcdA m * ↑b - ↑n * n.gcdA m * ↑a)) / ↑(n.gcd m)

Tactic:
← Int.mul_sub,

Goal state after:
case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑(n.gcd m) * ↑a + ↑n * n.gcdA m * (↑b - ↑a)) / ↑(n.gcd m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑b - (↑(n.gcd m) * ↑b - (↑m * n.gcdB m * ↑b - ↑m * n.gcdB m * ↑a)) / ↑(n.gcd m)

Tactic:
← Int.mul_sub,

Goal state after:
case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑b - (↑(n.gcd m) * ↑b - ↑m * n.gcdB m * (↑b - ↑a)) / ↑(n.gcd m)
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
induction i with

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 1 → R) →ₗ[R] M
hf : Injective ⇑f
⊢ Injective ⇑(f ∘ₗ ?m.100)

Tactic:
apply hf.comp (LinearEquiv.piUnique R ..).symm.injective

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Finite
⊢ s.encard = ↑h.toFinset.card

Tactic:
have := h.fintype
  rw [encard, ENat.card_eq_coe_fintype_card, toFinite_toFinset, toFinset_card]

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

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

Tactic:
encard_eq_top_iff

Goal state after:
α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ t.Infinite ↔ t.Infinite
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 : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (if i ∈ s then g i else 0) • v i = 0

Tactic:
by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]

Goal state after: