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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
⊢ p ∘ₛₗ f.codLift p hp h = f

Tactic:
by
  ext x
  rw [comp_apply, codLift_apply, (h x).choose_spec]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (List.map List.prod (hd :: tl)).sum

Tactic:
rw [List.map_cons, List.sum_cons]
    exact ha this (ih HL.2)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
⊢ a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
by
  rw [mul_comm a, mul_comm c]; exact Associated.of_mul_left

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f g : M →ₛₗ[τ₁₂] M₂
w✝ : M
⊢ (f + g) w✝ ∈ f.range ⊔ g.range

Tactic:
apply add_mem_sup

Goal state after:
case hs
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f g : M →ₛₗ[τ₁₂] M₂
w✝ : M
⊢ f w✝ ∈ f.range

case ht
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f g : M →ₛₗ[τ₁₂] M₂
w✝ : M
⊢ g w✝ ∈ g.range
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Surjective ⇑f.rangeRestrict

Tactic:
rw [← range_eq_top, range_rangeRestrict]

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

Goal state before:
pp: case le
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
⊢ r • N ≤ {r} • N

Tactic:
rintro _ ⟨m, hm, rfl⟩
    rw [mem_set_smul_def, Submodule.mem_sInf]
    intro _ hp; exact hp rfl hm

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ (p ⊔ p').toAddSubmonoid ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid

Tactic:
rw [mem_toAddSubmonoid, mem_sup, AddSubmonoid.mem_sup]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubmonoid, ∃ z ∈ p'.toAddSubmonoid, y + z = x
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
⊢ (s.biUnion g).SupIndep f

Tactic:
intro a ha b hb hab

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb : b ∈ s.biUnion g
hab : b ∉ a
⊢ Disjoint (f b) (a.sup f)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ sSup s ∈ s

Tactic:
rcases t.eq_empty_or_nonempty with rfl | h

Goal state after:
case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ∅.sup id
⊢ sSup s ∈ s

case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝⁷ : FunLike F' α α
inst✝⁶ : NatCast F'
inst✝⁵ : One F'
inst✝⁴ : SMul ℕ α
inst✝³ : SMul ℕ F'
inst✝² : IsSMulApply ℕ F' α α
inst✝¹ : IsNatCastApply F' α
inst✝ : IsOneApplyEqSelf F' α
n : ℕ
⊢ ↑n = n • 1

Tactic:
by
  apply DFunLike.ext
  simp

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝⁷ : FunLike F' α α
inst✝⁶ : IntCast F'
inst✝⁵ : One F'
inst✝⁴ : SMul ℤ α
inst✝³ : SMul ℤ F'
inst✝² : IsSMulApply ℤ F' α α
inst✝¹ : IsIntCastApply F' α
inst✝ : IsOneApplyEqSelf F' α
n : ℤ
⊢ ↑n = n • 1

Tactic:
by
  apply DFunLike.ext
  simp

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
ι : Sort u_8
p : ι → Submodule R M
x : M
hx : x ∈ span R (⋃ i, ↑(p i))
⊢ x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
refine Submodule.span_induction (fun x hx => ?_) ?_ (fun x y _ _ hx hy => ?_)
    (fun r x _ hx => ?_) hx

Goal state after:
case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝ : M
hx✝ : x✝ ∈ span R (⋃ i, ↑(p i))
x : M
hx : x ∈ ⋃ i, ↑(p i)
⊢ x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x : M
hx : x ∈ span R (⋃ i, ↑(p i))
⊢ 0 ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝² : M
hx✝ : x✝² ∈ span R (⋃ i, ↑(p i))
x y : M
x✝¹ : x ∈ span R (⋃ i, ↑(p i))
x✝ : y ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
hy : y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ x + y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∉ ⋂ x ∈ s, f x
⊢ ?m.85

Tactic:
by simpa using hj

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

Goal state before:
pp: case zero_right
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u : M
hu : u ∈ span R s
⊢ (B u) 0 ∈ P'

Tactic:
| zero_right u hu =>

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
⊢ ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
      Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) := by
      intro x _ y _ h
      simp only [disjoint_iff_ne, mem_image]
      rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
      rw [Pi.cons_same, Pi.cons_same] at this
      exact h this
    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
    refine sum_congr rfl fun b _ => ?_
    have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
    rw [sum_image h₂, mul_sum]
    refine sum_congr rfl fun g _ => ?_
    rw [attach_insert, prod_insert, prod_image]
    · simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
    · exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj
    · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha

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

Goal state before:
pp: case neg
ι : 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_1 : ι), x ∉ s x_1
⊢ 1 = ⨆ i, (s i).mulIndicator f x

Tactic:
simp [hx, ← h1]

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

Goal state before:
pp: case inr.succ
R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
h✝ : Nontrivial R
n : ℕ
ih : abv ↑n ≤ ↑n
⊢ abv (↑n + 1) ≤ ↑n + 1

Tactic:
abv.add_le,

Goal state after:
case inr.succ
R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
h✝ : Nontrivial R
n : ℕ
ih : abv ↑n ≤ ↑n
⊢ abv ↑n + abv 1 ≤ ↑n + 1
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ abv b - abv a ≤ abv (b - a)

Tactic:
apply abv.le_sub

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
have hps : ∀ x, x ∈ s → p x := fun x hx ↦ hpsa x (mem_cons_of_mem hx)
    have hp_prod : p s.prod := prod_induction_nonempty p hp_mul hs0 hps
    rw [prod_cons, map_cons, prod_cons]
    exact (h_mul a s.prod (hpsa a (mem_cons_self a s)) hp_prod).trans
      (by gcongr; exacts [h0 _, hs hps])

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
h : ∀ b ∉ Set.range f, x b = 0
i : β
hc : i ∉ Set.range f
hi : ¬x i = 0
⊢ False

Tactic:
exact hi (h _ hc)

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

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

Tactic:
apply (s.card_nsmul_le_sum _ _ h).trans

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})
⊢ ∑ x ∈ s, #({b ∈ B | x ∈ b}) ≤ ∑ t ∈ B, #(s ∩ t)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
⊢ mapDomain f x = 0 ↔ x = 0

Tactic:
classical
  refine ⟨fun h ↦ Finsupp.ext (fun i ↦ ?_), fun h ↦ by rw [h, mapDomain_zero]⟩
  replace h := Finsupp.ext_iff.mp h (f i)
  simp [mapDomain_apply_eq_sum] at h; grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝³ : Nonempty α
inst✝² : Zero M
inst✝¹ : SMulZeroClass R M
inst✝ : FaithfulSMul R M
m₁✝ m₂✝ : R
h : ∀ (a : α →₀ M), m₁✝ • a = m₂✝ • a
a : α
m : M
⊢ m₁✝ • m = m₂✝ • m

Tactic:
simpa using DFunLike.congr_fun (h (single a m)) a

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

Goal state before:
pp: α : Type u_1
M✝ : Type u_2
N✝ : Type u_3
P : Type u_4
R✝ : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S✝ : Type u_8
inst✝¹⁷ : Semiring R✝
inst✝¹⁶ : Semiring R₂
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
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ f (r • m) = r • f m

Tactic:
conv_rhs => rw [← sum_single m, map_finsuppSum, smul_sum]
    erw [← sum_single (r • m), sum_mapRange_index single_zero, map_finsuppSum]
    congr; ext i m; exact (f.comp <| lsingle i).map_smul_of_tower r m

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

Goal state before:
pp: case pos
ι : Type u_7
N₀ : Type u_8
M₀ : Type u_9
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
n : N₀
f : ι → N₀ → M₀
h : ∀ (i : ι), f i n ≠ 0
h₂ : (mulSupport f).Finite
⊢ (∏ᶠ (i : ι), f i) n ≠ 0

pp: case neg
ι : Type u_7
N₀ : Type u_8
M₀ : Type u_9
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
n : N₀
f : ι → N₀ → M₀
h : ∀ (i : ι), f i n ≠ 0
h₂ : ¬(mulSupport f).Finite
⊢ (∏ᶠ (i : ι), f i) n ≠ 0

Tactic:
· rw [finprod_eq_prod f h₂]
    grind [Finset.prod_apply, Finset.prod_ne_zero_iff]

Goal state after:
case neg
ι : Type u_7
N₀ : Type u_8
M₀ : Type u_9
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
n : N₀
f : ι → N₀ → M₀
h : ∀ (i : ι), f i n ≠ 0
h₂ : ¬(mulSupport f).Finite
⊢ (∏ᶠ (i : ι), f i) n ≠ 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ mulSupport (s.mulIndicator f) ⊆ ↑t

Tactic:
Set.mulSupport_mulIndicator

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ s ∩ mulSupport f ⊆ ↑t
Module: Mathlib.Order.Interval.Set.Fin

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

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

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
⊢ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x

Tactic:
obtain ⟨l, hl, hx⟩ := (Finsupp.mem_span_image_iff_linearCombination R).mp h

Goal state after:
case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
h : x ∈ span R (v '' s)
l : α →₀ R
hl : l ∈ Finsupp.supported R R s
hx : (Finsupp.linearCombination R v) l = x
⊢ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
x : α
u : Fin 0 → α
⊢ ∀ (i : Fin 1), vecCons x u i = x

Tactic:
rw [Fin.forall_fin_one]

Goal state after:
α : Type u
x : α
u : Fin 0 → α
⊢ vecCons x u 0 = x
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
hU : (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset _ hU, Finset.prod_comm]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
hU : (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ y ∈ s, ∏ x ∈ ⋯.toFinset, f x y = ∏ b ∈ s, ∏ᶠ (a : α), f a b
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
⊢ (finCongr ⋯) (finAddFlip ⟨n, ⋯⟩) = 0

Tactic:
rw [finAddFlip_apply_mk_right le_rfl]

Goal state after:
n : ℕ
⊢ (finCongr ⋯) ⟨n - n, ⋯⟩ = 0
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ a ≡ b [PMOD p] ↔ ∃ i, i < n ∧ a ≡ b + i • p [PMOD n • p]

Tactic:
simp_rw [← sub_modEq_iff_modEq_add, modEq_comm (b := b)]

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ b ≡ a [PMOD p] ↔ ∃ i, i < n ∧ b ≡ a - i • p [PMOD n • p]
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2.inl
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i < ↑a
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)

Tactic:
rw [succAbove_of_castSucc_lt, contractNth_apply_of_lt _ _ _ _ h,
        succAbove_of_castSucc_lt] <;>
      simp only [lt_def, val_castSucc, val_succ] <;>
      lia

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
h : a ≡ b [MOD n]
⊢ n ∣ b - a

Tactic:
obtain h0 | h0 : a ≤ b ∨ b ≤ a := le_total a b
  · exact (modEq_iff_dvd' h0).mp h
  · rw [Nat.sub_eq_zero_of_le h0]
    exact Nat.dvd_zero n

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
let d := gcd m c

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

pp: case right.refine_2
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
⊢ m ∣ n.lcm m

Tactic:
· rw [← sub_eq_iff_eq_add] at this
          rw [← this, Int.sub_mul, sub_add, ← Int.mul_sub, Int.sub_ediv_of_dvd,
            Int.mul_ediv_cancel_left _ hnonzero, Int.mul_ediv_assoc _ h.dvd, ← sub_add, sub_self,
            zero_add, mul_assoc]
          · exact dvd_mul_right _ _
          · exact hcoedvd _

Goal state after:
case right.refine_2
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
⊢ m ∣ n.lcm m
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
inst✝ : Nontrivial R
n : ℕ
⊢ ↑n ≤ Module.rank R M ↔ ∃ v, LinearIndependent R v

Tactic:
refine le_rank_iff_exists_finset.trans ⟨fun ⟨s, s_card, s_ind⟩ ↦ ?_, fun ⟨v, v_ind⟩ ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
s : Finset M
s_card : s.card = n
s_ind : LinearIndepOn R id ↑s
⊢ ∃ v, LinearIndependent R v

case refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ v, LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
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
inst✝ : Nontrivial R
n : ℕ
⊢ ↑n ≤ Module.rank R M ↔ ∃ v, LinearIndependent R v

Tactic:
refine le_rank_iff_exists_finset.trans ⟨fun ⟨s, s_card, s_ind⟩ ↦ ?_, fun ⟨v, v_ind⟩ ↦ ?_⟩
  · exact ⟨_, s_ind.comp _ (s.equivFinOfCardEq s_card).symm.injective⟩
  · refine ⟨.map ⟨_, v_ind.injective⟩ .univ, by simp, ?_⟩
    simpa using (linearIndepOn_id_range_iff v_ind.injective).mpr v_ind

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

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
inst✝² : CommSemiring R'
S' : Type v
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R ≃+* R'
j : S ≃+* S'
hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)
⊢ Module.rank R S = Module.rank R' S'

Tactic:
simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hc

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0
⊢ N = ⊥

Tactic:
by
  rw [Submodule.eq_bot_iff]
  intro x hx
  contrapose! rank_eq with x_ne
  refine ⟨1, fun _ => ⟨x, hx⟩, ?_, one_ne_zero⟩
  rw [Fintype.linearIndependent_iff]
  rintro g sum_eq i
  simp only [Fin.default_eq_zero, Finset.univ_unique,
    Finset.sum_singleton] at sum_eq
  convert! (b.smul_eq_zero.mp sum_eq).resolve_right x_ne

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

Goal state before:
pp: case h.inr
P : Type u_4 → Prop
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [Finite α], Nat.card α = m → P α
α : Type u_4
inst✝¹ : Finite α
hn : Nat.card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Finite β
hlt : Nat.card β < n
⊢ P β

Tactic:
exact ih (Nat.card β) hlt _ rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∉ J
⊢ b i = 0 i

Tactic:
· exact hJ i hiJ

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ (factor H2) ((factor H1) x) = (factor ⋯) x

Tactic:
rw [← comp_apply]
  simp

Goal state after: