mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

Tactic:
mulIndicator_of_mem hx

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ i, s i
⊢ f x = ⨆ i, (s i).mulIndicator f x
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
⊢ g y 0 * (erase y f).prod g = f.prod g

Tactic:
hg y,

Goal state after:
case neg
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
⊢ 1 * (erase y f).prod g = f.prod g
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
⊢ ((∑ a, single a (f a)).sum fun x n ↦ n) = ∑ a, f a

Tactic:
sum_fintype _ _ fun _ ↦ rfl,

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
⊢ ∑ i, (∑ a, single a (f a)) i = ∑ a, f a
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
inst✝ : SemilatticeInf M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, HasFiniteMulSupport (f i)
hs : s.Nonempty
⊢ HasFiniteMulSupport fun a ↦ s.inf' hs fun x ↦ f x a

Tactic:
by
  simp only [HasFiniteMulSupport] at hf ⊢
  refine (s.finite_toSet.biUnion hf).subset fun a ha ↦ ?_
  simp only [mem_mulSupport, SetLike.mem_coe, Set.mem_iUnion, exists_prop] at ha ⊢
  contrapose! ha
  exact Finset.inf'_eq_of_forall hs (fun x ↦ f x a) ha

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Monoid M
f : α → M
g : α → ℕ
hg : HasFiniteSupport g
a : α
ha : a ∈ mulSupport fun a ↦ f a ^ g a
⊢ a ∈ support g

Tactic:
by contrapose! ha; simp_all

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

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
x : R
⊢ abv x ≤ 0 ↔ x = 0

Tactic:
by
  simp only [← abv.eq_zero, le_antisymm_iff, abv.nonneg, and_true]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case h₂
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ (map f s).prod ≤ (map g s).prod

pp: case c0
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ 0 ≤ (map f s).prod

pp: case b0
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ 0 ≤ g a

Tactic:
· grind

Goal state after:
case c0
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ 0 ≤ (map f s).prod

case b0
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ 0 ≤ g a
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
⊢ (∀ i ∈ insert a s, 1 ≤ f i) → (∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1)

Tactic:
H

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
⊢ ∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1
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
⊢ (↑f.support).PairwiseDisjoint fun a ↦ map (Embedding.sectR a β) (f a).support

Tactic:
by
    intro a₁ _ a₂ _ hne
    simp [Finset.disjoint_iff_ne, hne]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hf : Injective f
hs : (↑s).PairwiseDisjoint f
⊢ #s ≤ #(s.biUnion f) + 1

Tactic:
grw [card_le_card_biUnion_add_card_fiber hs,
    card_le_one.2 fun _ hi _ hj ↦ hf <| (mem_filter.1 hi).2.trans (mem_filter.1 hj).2.symm]

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

Goal state before:
pp: case e'_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
⊢ ↑x.support ⊆ Set.range ⇑f ↔ ∀ b ∉ Set.range ⇑f, x b = 0

Tactic:
· grind

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

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

Tactic:
exact image_mono h

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_7
s : Set α
t : Set α'
e : ↑s ≃ ↑t
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)

Tactic:
haveI := Classical.decPred fun x => x ∈ s

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α' : Type u_7
s : Set α
t : Set α'
e : ↑s ≃ ↑t
this : DecidablePred fun x ↦ x ∈ s
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)
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
⊢ x ∈ span R (Set.range v)

Tactic:
rw [← hl]

Goal state after:
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
⊢ (linearCombination R v) l ∈ span R (Set.range v)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
⊢ ∏ᶠ (i : α), f i = if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset h, f i else 1

Tactic:
split_ifs with h
  · exact finprod_eq_prod_of_mulSupport_toFinset_subset _ h (Finset.Subset.refl _)
  · rw [finprod, dif_neg]
    rw [HasFiniteMulSupport, mulSupport_comp_eq_preimage]
    exact mt (fun hf => hf.of_preimage Equiv.plift.surjective) h

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 : ι) (_ : p i), f i

Tactic:
finprod_cond_eq_prod_of_cond_iff (t := hf.toFinset)

Goal state after:
ι : 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

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.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ (linearCombinationOn α M R v s).range = ⊤

Tactic:
rw [linearCombinationOn, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top, LinearMap.range_comp,
    range_subtype]
  exact (span_image_eq_map_linearCombination _ _).le

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v✝ : α → M
r : S
v : α → M
⊢ Fintype.linearCombination R (r • v) = (RingHom.id S) r • Fintype.linearCombination R v

Tactic:
by ext; simp [Fintype.linearCombination, Finset.smul_sum, smul_comm]

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

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

Tactic:
Finsupp.lmapDomain_supported,

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Ioo a b) = ↑b - ↑a - 1

Tactic:
← Nat.card_Ioo,

Goal state after:
n : ℕ
a b : Fin n
⊢ #(Ioo a b) = #(Ioo ↑a ↑b)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
⊢ vecCons a (vecCons b x) ∘ ⇑(Equiv.swap 0 1) = vecCons b (vecCons a x)

Tactic:
ext j : 1
  match j with
  | 0 => simp
  | 1 => simp
  | ⟨i + 2, h⟩ =>
    have h' : (⟨i + 2, h⟩ : Fin n.succ.succ) = Fin.succ (Fin.succ ⟨i, by lia⟩) := by grind
    simp only [Nat.succ_eq_add_one, h', Function.comp_apply,
      Equiv.swap_apply_of_ne_of_ne (Fin.succ_ne_zero _) (Fin.succ_succ_ne_one _), cons_val_succ]

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 : ∀ (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'
⊢ ∑ i ∈ S, r₁ i • (⇑j ∘ v) i = ∑ i ∈ S, r₂ i • (⇑j ∘ v) i → ∀ i ∈ S, r₁ i = r₂ i

Tactic:
H

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'
H : ∑ i ∈ S, r₁ i • (⇑j ∘ v) i = ∑ i ∈ S, r₂ i • (⇑j ∘ v) i
⊢ ∀ i ∈ S, r₁ i = r₂ i
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (n * k + m).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_mul_left_add_left]

Goal state after:
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
⊢ i = j

Tactic:
by
  have h_single_eq : Finsupp.single i c = Finsupp.single j d :=
    li <| by simpa [Finsupp.linearCombination_apply] using h
  rcases (Finsupp.single_eq_single_iff ..).mp h_single_eq with (⟨H, _⟩ | ⟨hc, _⟩)
  · exact H
  · contradiction

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
⊢ (Finsupp.linearCombination R (v ∘ ⇑f)) (repr ⟨v i, ⋯⟩) = v i

Tactic:
(hv.comp f f.injective).linearCombination_repr

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
⊢ ↑⟨v i, ⋯⟩ = v i
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'
⊢ ∑ i ∈ S, r' i • (⇑j ∘ v) i = 0 → ∀ i ∈ S, r' i = 0

Tactic:
H

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'
H : ∑ i ∈ S, r' i • (⇑j ∘ v) i = 0
⊢ ∀ i ∈ S, r' i = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑n ∣ ↑a - ↑((↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat ∧
    ↑m ∣ ↑b - ↑((↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat

Tactic:
Int.toNat_of_nonneg (Int.emod_nonneg _ (Int.natCast_ne_zero.2 (lcm_ne_zero hn hm)))

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m) ∧
    ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: b a n : ℕ
h : a * b ≡ 1 [MOD n]
⊢ a.Coprime n

Tactic:
by
  obtain ⟨g, hh⟩ := Nat.gcd_dvd_right a n
  rw [Nat.coprime_iff_gcd_eq_one, ← Nat.dvd_one, ← Nat.modEq_zero_iff_dvd]
  calc
    1 ≡ a * b [MOD a.gcd n] := (hh ▸ h).symm.of_mul_right g
    _ ≡ 0 * b [MOD a.gcd n] := (Nat.modEq_zero_iff_dvd.mpr (Nat.gcd_dvd_left _ _)).mul_right b
    _ = 0 := by rw [zero_mul]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
⊢ card α = 1 ↔ Nonempty (Unique α)

Tactic:
unique_iff_subsingleton_and_nonempty α,

Goal state after:
α : Type u_3
⊢ card α = 1 ↔ Subsingleton α ∧ Nonempty α
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
⊢ 1 < card α ↔ Nontrivial α

Tactic:
by
  rw [← Cardinal.one_lt_iff_nontrivial]
  conv_rhs => rw [← Nat.cast_one]
  rw [← natCast_lt_toENat]
  simp only [ENat.card, Nat.cast_one]

Goal state after:
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 (Module.rank R M) = toNat (Module.rank R N)

Tactic:
rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + m / k * k = m

Tactic:
by
  rw [mul_comm]
  exact mod_add_div _ _

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ ↑(a % b).natAbs < ↑b.natAbs

Tactic:
Int.natAbs_of_nonneg (Int.emod_nonneg _ b0),

Goal state after:
a b : ℤ
b0 : b ≠ 0
⊢ a % b < ↑b.natAbs
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : t.encard = s.encard + 1
⊢ ∃ a, t = insert a s

Tactic:
rw [← encard_sdiff_add_encard_of_subset h, add_comm _ 1,
    (ENat.addLECancellable_of_lt_top hs.encard_lt_top).inj_left, encard_eq_one] at hst
  obtain ⟨x, hx⟩ := hst; use x; rw [← sdiff_union_of_subset h, hx, singleton_union]

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

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

Tactic:
apply mul_mem (ih _ _ _) (by simp [h2])

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
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
⊢ ∀ i_1 ∉ I, Function.update x i 1 i_1 = 1

η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
⊢ ∀ i_1 ∈ I, Pi.mulSingle i_1 (Function.update x i 1 i_1) ∈ H
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
x : G
hx : x ∈ ↑M
⊢ ↑((MonoidHom.id G) x) = 1

Tactic:
exact (QuotientGroup.eq_one_iff _).mpr hx

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
⊢ x ∈ MonoidHom.mrange (c.lift f H) → x ∈ MonoidHom.mrange f

Tactic:
rintro ⟨⟨y⟩, hy⟩

Goal state after:
case mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
w✝ : c.Quotient
y : M
hy : (c.lift f H) (Quot.mk (⇑c.toSetoid) y) = x
⊢ x ∈ MonoidHom.mrange f
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
⊢ ↑(insert (pred a) (Icc a b)) = ↑(Icc (pred a) b)

Tactic:
by simpa using Set.insert_Icc_left_eq_Icc_pred h

Goal state after:
Module: Mathlib.Data.Fintype.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ y, Infinite ↑(f ⁻¹' {y})

Tactic:
by_contra! hf
    cases nonempty_fintype β
    let key : Fintype α :=
      { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
        complete := by simp }
    exact key.false

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case pos.refine_2
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range fun i ↦ (partialSups f) i)

Tactic:
rwa [bddAbove_range_partialSups]

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

Goal state before:
pp: case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
i : ℕ
left✝¹ : k ≤ i
im : i < m
j : ℕ
left✝ : k ≤ j
jm : j < m
Hij : n - i = n - j
⊢ i = j

Tactic:
← tsub_tsub_cancel_of_le (this _ im),

Goal state after:
case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
i : ℕ
left✝¹ : k ≤ i
im : i < m
j : ℕ
left✝ : k ≤ j
jm : j < m
Hij : n - i = n - j
⊢ n - (n - i) = j
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case e'_3
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ f a.succ / f 0 = (if hi : ↑a + 1 < n + 1 then f ⟨↑a + 1, hi⟩ else 1) / if hi : 0 < n + 1 then f ⟨0, hi⟩ else 1

Tactic:
· grind

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

Goal state before:
pp: case e'_3.e'_5
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f b.succ = if hi : ↑b + 1 < n + 1 then f ⟨↑b + 1, hi⟩ else 1

pp: case e'_3.e'_6
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f a.castSucc = if hi : ↑a < n + 1 then f ⟨↑a, hi⟩ else 1

Tactic:
· grind

Goal state after:
case e'_3.e'_6
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f a.castSucc = if hi : ↑a < n + 1 then f ⟨↑a, hi⟩ else 1
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Tactic:
rw [antidiagonal_succ, prod_cons, prod_map]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏ x ∈ antidiagonal n,
        f (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) x) =
    f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)