mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Span.Basic

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

Tactic:
suffices ⨆ i ∈ s, (p i).comap (LinearMap.range f).subtype = ⊤ by
    rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]; rfl
  exact hf ▸ biSup_comap_subtype_eq_top s p

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
x : M
hx : x ∈ N
y : ↥N
⊢ ↑y ∈ R ∙ x ↔ y ∈ R ∙ ⟨x, hx⟩

Tactic:
mem_span_singleton

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
x : M
hx : x ∈ N
y : ↥N
⊢ (∃ a, a • x = ↑y) ↔ ∃ a, a • ⟨x, hx⟩ = y
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
⊢ Injective fun f ↦ indicator s f

Tactic:
by
  intro a b h
  ext i hi
  rw [← indicator_of_mem hi a, ← indicator_of_mem hi b]
  exact DFunLike.congr_fun h i

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : i ∈ (indicator s f).support
⊢ i ∈ s

Tactic:
mem_support_iff

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : (indicator s f) i ≠ 0
⊢ i ∈ s
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case cons
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
ih : (s✝.sum f).support ⊆ s✝.sup fun x ↦ (f x).support
⊢ ((cons a✝ s✝ h✝).sum f).support ⊆ (cons a✝ s✝ h✝).sup fun x ↦ (f x).support

Tactic:
| cons _ _ _ ih =>

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

Goal state before:
pp: case pos
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : a = 0
⊢ abv (-a) = abv a

pp: case neg
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (-a) = abv a

Tactic:
· simp [ha]

Goal state after:
case neg
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (-a) = abv a
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_1 ∈ f.support, { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_1 = (a, m)) ↔ f a = m ∧ m ≠ 0

Tactic:
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
M : Type u_5
inst✝ : Zero M
c : α × M
f : α →₀ M
⊢ c ∈ f.graph ↔ f c.1 = c.2 ∧ c.2 ≠ 0

Tactic:
cases c

Goal state after:
case mk
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
fst✝ : α
snd✝ : M
⊢ (fst✝, snd✝) ∈ f.graph ↔ f (fst✝, snd✝).1 = (fst✝, snd✝).2 ∧ (fst✝, snd✝).2 ≠ 0
Module: Mathlib.Data.Finsupp.Basic

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

Tactic:
mapDomain,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ (x.sum fun a ↦ single (f a)) (f a) = x a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
hb : b ∉ f '' ↑x.support
⊢ (mapDomain f x) b = 0

Tactic:
mapDomain,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
hb : b ∉ f '' ↑x.support
⊢ (x.sum fun a ↦ single (f a)) b = 0
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 : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ (mapDomain f x) (f a) = x a

Tactic:
mapDomain,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ (x.sum fun a ↦ single (f a)) (f a) = x a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a

Tactic:
rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
      convert! add_zero (x a)
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase 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
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a

Tactic:
· rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)

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
h : a ∉ f.support
ha : f a + s.sum a ≠ 0
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
notMem_support_iff.1 h,

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 : 0 + s.sum a ≠ 0
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : 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 : α →₀ β →₀ M
a₁ : α
a✝¹ : a₁ ∈ ↑f.support
a₂ : α
a✝ : a₂ ∈ ↑f.support
⊢ a₁ ≠ a₂ → (Disjoint on fun a ↦ map (Embedding.sectR a β) (f a).support) a₁ a₂

Tactic:
hne

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
inst✝ : Zero M
f : α →₀ β →₀ M
a₁ : α
a✝¹ : a₁ ∈ ↑f.support
a₂ : α
a✝ : a₂ ∈ ↑f.support
hne : a₁ ≠ a₂
⊢ (Disjoint on fun a ↦ map (Embedding.sectR a β) (f a).support) a₁ a₂
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α ↪ β
g : β ↪ γ
⊢ embDomain (f.trans g) v = embDomain g (embDomain f v)

Tactic:
by
  simp only [embDomain_eq_mapDomain, ← mapDomain_comp, Embedding.coe_trans]

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: case cons
M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : CommMonoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
b : ι → M
f : ι → N
a✝ : ι
s✝ : Finset ι
hj : a✝ ∉ s✝
ih : ∏ i ∈ s✝, b i • f i = (∏ i ∈ s✝, b i) • ∏ i ∈ s✝, f i
⊢ (b a✝ * ∏ i ∈ s✝, b i) • (f a✝ * ∏ i ∈ s✝, f i) = (∏ i ∈ cons a✝ s✝ hj, b i) • ∏ i ∈ cons a✝ s✝ hj, f i

Tactic:
← prod_cons hj,

Goal state after:
case cons
M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : CommMonoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
b : ι → M
f : ι → N
a✝ : ι
s✝ : Finset ι
hj : a✝ ∉ s✝
ih : ∏ i ∈ s✝, b i • f i = (∏ i ∈ s✝, b i) • ∏ i ∈ s✝, f i
⊢ (∏ x ∈ cons a✝ s✝ hj, b x) • (f a✝ * ∏ i ∈ s✝, f i) = (∏ i ∈ cons a✝ s✝ hj, b i) • ∏ i ∈ cons a✝ s✝ hj, f i
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 ↔
    (True ∧ ∀ a ∈ i, ¬z = a → Disjoint (f z) (f a)) ∧
      ∀ a ∈ i, (¬a = z → Disjoint (f a) (f z)) ∧ ∀ a_2 ∈ i, ¬a = a_2 → Disjoint (f a) (f a_2)

Tactic:
true_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)) ∧
      ∀ a ∈ i, (¬a = z → Disjoint (f a) (f z)) ∧ ∀ a_2 ∈ i, ¬a = a_2 → Disjoint (f a) (f a_2)
Module: Mathlib.Data.Finset.Fin

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ ↑(image Fin.val (s.attachFin h)) = ↑s

Tactic:
rw [coe_image, coe_attachFin, Set.image_preimage_eq_iff]

Goal state after:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ ↑s ⊆ Set.range Fin.val
Module: Mathlib.Order.Interval.Set.Fin

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

Tactic:
rw [← preimage_val_Icc_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
  exact fun k hk ↦ hk.2.trans_lt j.is_lt

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

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v) l = x
⊢ (l.sum fun i a ↦ a • v i) ∈ span R (Set.range v)

Tactic:
exact sum_mem fun i _ => Submodule.smul_mem _ _ (subset_span (mem_range_self i))

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
c : ι → R
⊢ ⇑(b.repr (∑ i, c i • b i)) = c

Tactic:
by
  simp_rw [← b.equivFun_symm_apply, ← b.equivFun_apply, b.equivFun.apply_symm_apply]

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

Goal state before:
pp: ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ 1 < ∏ i ∈ hf.toFinset, f i

pp: case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∀ {x : ι}, f x ≠ 1 → (p x ↔ x ∈ hf.toFinset)

Tactic:
· apply Finset.one_lt_prod'
    · simp +contextual [h]
    · aesop

Goal state after:
case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
p : ι → Prop
h : ∀ (i : ι), p i → 1 ≤ f i
h' : ∃ i, p i ∧ 1 < f i
hf : (mulSupport f ∩ {i | p i}).Finite
⊢ ∀ {x : ι}, f x ≠ 1 → (p x ↔ x ∈ hf.toFinset)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ Ioo (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m

Tactic:
exact Ioo_subset_Ioi_self.trans <| image_addNat_Ioi m i ▸ image_subset_range _ _

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 : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ ↑t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ ↑t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑t), f i

Tactic:
rw [← Finset.coe_union, ← Finset.coe_inter]
    simp only [finprod_mem_coe_finset, Finset.prod_union_inter]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ (∃ l ∈ supported R R s, (linearCombination R _root_.id) l = x) →
    ∃ f t, ↑t ⊆ _root_.id '' s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x

Tactic:
rintro ⟨l, hl, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
l : M →₀ R
hl : l ∈ supported R R s
⊢ ∃ f t, ↑t ⊆ _root_.id '' s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = (linearCombination R _root_.id) l
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)

Goal state after:
case pos
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∈ mulSupport f
⊢ f a ∣ ∏ i ∈ Finite.toFinset hf, f i
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 : α) (_ : a ∈ s), f a * r

Tactic:
rw [finsum_mul]

Goal state after:
α : 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 : α) (_ : a ∈ s), f a * r
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
⊢ ∏ᶠ (abc : α × β × γ), f abc = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)

Tactic:
rw [finprod_curry f h]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
⊢ ∏ᶠ (a : α) (b : β × γ), f (a, b) = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
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
v : ι → M
hli : LinearIndependent R v
i : ι
hi : v i ∈ span R (range v)
⊢ (Basis.span hli).repr ⟨v i, hi⟩ = single i 1

Tactic:
by
  rw [← LinearEquiv.eq_symm_apply]
  simp [Basis.span]

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

Goal state before:
pp: case mp
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
b : Basis ι R M
⊢ ∀ (y : M), ∃ r, r • b default = y

Tactic:
simpa [span_singleton_eq_top_iff, Set.range_unique] using b.span_eq

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

Goal state before:
pp: case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ True ∧ y ≠ 0

Tactic:
true_and,

Goal state after:
case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ y ≠ 0
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
prod_ofFn

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
⊢ ∏ i, f i = ∏ i, f i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
i : ℕ
h : i < 0 + 1
x : M
p : Fin 0 → M
⊢ ∏ j, ⟨i, h⟩.insertNth x p j = x * ∏ j, p j

Tactic:
simp [fin_one_eq_zero ⟨i, h⟩]

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✝⁵ : 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 : LinearIndependent R v
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ LinearIndependent R' (⇑j ∘ v)

Tactic:
rw [linearIndependent_iff'ₛ] at hv ⊢

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 ι) (f g : ι → R'), ∑ i ∈ s, f i • (⇑j ∘ v) i = ∑ i ∈ s, g i • (⇑j ∘ v) i → ∀ i ∈ s, f i = g i
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 : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
h_surj : Surjective ⇑f
x : M
hx : x ∈ s
⊢ x ∈ t

Tactic:
rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩

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 : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
h_surj : Surjective ⇑f
x : M
hx : x ∈ s
y : ↑t
hy : f y = ⟨x, hx⟩
⊢ x ∈ t
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m / ↑d ∣ ↑c / ↑d * (↑b - ↑a)

Tactic:
rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.natCast_dvd_natCast.mpr hcd), mul_comm]

Goal state after:
case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m / ↑d ∣ ↑c * (↑b - ↑a) / ↑(m.gcd c)
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 - (↑a + ↑n * n.gcdA m * ((↑b - ↑a) / ↑(n.gcd m)))

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.gcd m) ∣ ↑(n.gcd m) * ↑a

Tactic:
← sub_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 - ↑a - ↑n * n.gcdA m * ((↑b - ↑a) / ↑(n.gcd m))

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.gcd m) ∣ ↑(n.gcd m) * ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(if hn : n = 0 then ⟨a, ⋯⟩
      else
        if hm : m = 0 then ⟨b, ⋯⟩
        else ⟨((↑n * (n.xgcd m).1 * ↑b + ↑m * (n.xgcd m).2 * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat, ⋯⟩) <
    n.lcm m

Tactic:
rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_natCast (lcm n m)]

Goal state after:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ((↑n * (n.gcdA m, n.gcdB m).1 * ↑b + ↑m * (n.gcdA m, n.gcdB m).2 * ↑a) / ↑(n.gcd m) % ↑(↑(n.lcm m)).toNat).toNat <
    (↑(n.lcm m)).toNat
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2)) + 2 * (m / 2)

Tactic:
two_mul_odd_div_two hm1,

Goal state after:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2)) + (m - 1)
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
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ (g a • ⇑a) 1 = (∑ i ∈ insert a s, g i • ⇑i) 1

Tactic:
rw [Finset.sum_insert has, Finset.sum_eq_zero, add_zero]

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
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ ∀ x ∈ s, g x • ⇑x = 0
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M ≃ₗ[R] N
⊢ toNat (lift.{?u.31, v} (Module.rank R M)) = toNat (Module.rank R N)

Tactic:
f.lift_rank_eq,

Goal state after:
R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M ≃ₗ[R] N
⊢ toNat (lift.{v, w} (Module.rank R N)) = toNat (Module.rank R N)
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : 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
⊢ Function.update x i 1 j = 1

pp: η : 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
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H

Tactic:
· by_cases heq : j = i
      · subst heq
        simp
      · simpa [heq] using h1 j (by simpa [heq] using hj)

Goal state after:
η : 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
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : Finite ↑s ∧ t.Finite
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
← finite_coe_iff

Goal state after:
case inl
α : Type u_1
s t : Set α
h : Finite ↑s ∧ Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
← mul_inv_cancel_right x⁻¹ y

Goal state after:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ Even sᶜ.ncard ↔ Even s.ncard

Tactic:
rwa [iff_comm, ← Nat.even_add, ncard_add_ncard_compl]

Goal state after: