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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_4
inst✝¹ : Semiring S
inst✝ : Algebra R S
r : R
⊢ algebraMapSubmonoid S (Submonoid.powers r) = Submonoid.powers ((algebraMap R S) r)

Tactic:
simp [Algebra.algebraMapSubmonoid]

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

Goal state before:
pp: case mp
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R B) r ∈ algebraMapSubmonoid B M

Tactic:
use r

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

Goal state before:
pp: case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R A) r ∈ algebraMapSubmonoid A M

Tactic:
use r

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

Goal state before:
pp: case mem
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝ : R
hx : x✝ ∈ s
⊢ x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
exact AddSubgroup.subset_closure (Submonoid.subset_closure hx)

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mp.refine_2
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit x
⊢ Irreducible y

Tactic:
irreducible_isUnit_mul h'

Goal state after:
case mp.refine_2
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible y
h' : IsUnit x
⊢ Irreducible y
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
u v : Mˣ
⊢ x * ↑(u * v) = x * ↑u * ↑v

Tactic:
rw [Units.val_mul, mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
⊢ ∀ (a : (Associates M)ˣ), a = default

Tactic:
rintro ⟨a, b, hab, hba⟩
    induction a, b using Quotient.inductionOn₂ with | _ a b
    exact Units.ext <| Quotient.sound <| associated_one_of_associated_mul_one <| Quotient.exact hab

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q r : M
h : DvdNotUnit p q
h' : q ~ᵤ r
⊢ DvdNotUnit p r

Tactic:
obtain ⟨u, rfl⟩ := h'
  obtain ⟨hp, x, hx⟩ := h
  refine ⟨hp, x * u, mt isUnit_of_mul_isUnit_left hx.1, ?_⟩
  rw [← mul_assoc, ← hx.right]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : LeftInverse ⇑g ⇑f
x : P
hx : x ∈ (f ∘ₗ g - id).ker
⊢ f (g x) = x

Tactic:
by simpa [sub_eq_zero] using hx

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ 1 * x = x

Tactic:
one_mul

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ x = x
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1 • 1) = x

Tactic:
rw [map_smul, Algebra.smul_def, mul_left_comm, ← Algebra.smul_def _ (e 1),
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, ← mul_assoc, ← Algebra.smul_def,
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, one_mul]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x z y : α
⊢ z ≤ x → x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ z

Tactic:
simp_rw [inf_comm x, sup_comm _ z]
  exact sup_inf_le_assoc_of_le y

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Frame α
f : ι → α
i : ι
x : α
hxf : x ≤ f i
hx : ¬x = ⊥
ha : IsAtom x
h : x ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬x ≤ f i
hxa : x ≤ x
⊢ False

Tactic:
exact ha' _ hxf

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') ↔ ∀ (z : M), ∃ x y, x ∈ p ∧ y ∈ p' ∧ x + y = z

Tactic:
exact forall_congr' (fun z => mem_sup.trans <| by simp)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Tactic:
refine and_congr_right fun _ ↦ forall_congr' fun H ↦ ?_
  contrapose!
  rw [lt_iff_le_not_ge, lt_iff_le_and_ne, and_and_and_comm]
  simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]

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
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
by
  rw [← span_singleton_le_iff_mem, le_iSup_iff]
  simp only [span_singleton_le_iff_mem]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective ⇑f
inst✝ : IsPrincipal R M
m : M
hm : ⊤ = R ∙ m
r : R
x✝ : f (r • m) ∈ ⊤
⊢ f (r • m) ∈ R ∙ f m

Tactic:
simpa only [map_smul] using smul_mem _ r (mem_span_singleton_self _)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
x : α
⊢ IsAtom {x}

Tactic:
exact isAtom_singleton x

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
x✝² : u ⊆ t
i : ι'
x✝¹ : i ∈ t
x✝ : i ∉ u
⊢ Disjoint ((fun i' ↦ s.sup fun i ↦ f (i, i')) i) (u.sup fun i' ↦ s.sup fun i ↦ f (i, i'))

Tactic:
suffices Disjoint ((s.image ((·, i))).sup f) ((s ×ˢ u).sup f) by
      simpa only [sup_image, sup_product_right]

Goal state after:
case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
x✝² : u ⊆ t
i : ι'
x✝¹ : i ∈ t
x✝ : i ∉ u
⊢ Disjoint ((image (fun x ↦ (x, i)) s).sup f) ((s ×ˢ u).sup f)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mp
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ sSupIndep {a, b} → Disjoint a b

Tactic:
intro h
    exact h.pairwiseDisjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab

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

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
hxk : x < k
⊢ False

Tactic:
exact hxk.ne (hxk.le.antisymm hkx)

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

Goal state before:
pp: M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ (a :: l).prod = 0

Tactic:
rw [prod_cons]

Goal state after:
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ a * l.prod = 0
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ prod ⟦l⟧ = 0 ↔ 0 ∈ ⟦l⟧

Tactic:
rw [quot_mk_to_coe, prod_coe]; exact List.prod_eq_zero_iff

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s : Multiset α
this : s.powerset.card = 2 ^ s.card
⊢ s.antidiagonal.card = 2 ^ s.card

Tactic:
rwa [← antidiagonal_map_fst, card_map] at this

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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ map f p = f.range ↔ Codisjoint p f.ker

Tactic:
simp_rw [le_antisymm_iff, LinearMap.map_le_range, true_and, ← map_top, map_le_iff_le_comap,
    comap_map_eq, codisjoint_iff_le_sup]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ 1 * g x = g x

Tactic:
one_mul

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ g x = g x
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ 1 * g x = g x

Tactic:
one_mul

Goal state after:
case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ g x = g x
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
⊢ K ∙ x ⊔ s ≤ q

Tactic:
rcases SetLike.exists_of_lt hpq with ⟨y, hyq, hyp⟩

Goal state after:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
y : V
hyq : y ∈ q
hyp : y ∉ s
⊢ K ∙ x ⊔ s ≤ q
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
| 1 * (e * e)

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝ : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
| e * e
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
s : ι
hs : s ∈ s✝
⊢ f s = f s / n * n

Tactic:
Nat.div_mul_cancel (hf _ 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
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
this :
  (Function.support g ⊆ ↑s ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ g = ⇑(indicator s f) ↔ Function.support g ⊆ ↑s ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i

Tactic:
simp only [this, funext_iff, indicator_apply]
    grind

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

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

Tactic:
classical exact Pi.single_eq_same (M := fun _ ↦ M) a b

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
h : f a = 0
b : M
⊢ f.update a b = single a b + f

Tactic:
update_eq_single_add_erase,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f : ι →₀ M
a : ι
h : f a = 0
b : M
⊢ single a b + erase a f = single a b + f
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case pos
α : 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 (f y) * (erase y f).prod g = f.prod g

Tactic:
exact Finsupp.mul_prod_erase f y g hyf

Goal state after:
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
⊢ 1 * f.prod g = f.prod g

Tactic:
one_mul

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
⊢ f.prod g = f.prod g
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
f g : ι → M₀
x : ι
hfg : x ∈ support fun x ↦ f x * g x
hf : f x = 0
⊢ (fun x ↦ f x * g x) x = 0

Tactic:
by simp only [hf, zero_mul]

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

Goal state before:
pp: 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
x : ℤ
⊢ abv ↑x.natAbs = abv ↑x

Tactic:
obtain ⟨_, rfl | rfl⟩ := Int.eq_nat_or_neg x <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
a : α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedMul α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ (a ::ₘ t).prod

Tactic:
rw [prod_cons]

Goal state after:
α : Type u_2
inst✝² : CommMonoid α
a : α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedMul α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ a * t.prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ f i * f j = ∏ k ∈ cons i {j} ⋯, f k

Tactic:
rw [prod_cons, prod_singleton]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
obtain h | h := (sum_nonneg hg).eq_or_lt'

Goal state after:
case inl
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : ∑ i ∈ s, g i = 0
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

case inr
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

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

Tactic:
exact hle x hx h'x.2

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ ∏ x ∈ s \ t ∪ s ∩ t, f x ≤ (∏ i ∈ t \ s, f i) * ∏ x ∈ s ∩ t, f x ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Tactic:
sdiff_union_inter,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ ∏ x ∈ s, f x ≤ (∏ i ∈ t \ s, f i) * ∏ x ∈ s ∩ t, f x ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ s \ t ∪ s ∩ t, f x < (∏ i ∈ t \ s, f i) * ∏ x ∈ s ∩ t, f x ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

Tactic:
sdiff_union_inter,

Goal state after:
ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ s, f x < (∏ i ∈ t \ s, f i) * ∏ x ∈ s ∩ t, f x ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i
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
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
hx : Function.invFunOn f s c ∈ ↑((lmapDomain M R (Function.invFunOn f s)) l).support
⊢ ∃ a ∈ s, f a = c

Tactic:
simpa using hl hc

Goal state after:
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
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
⊢ ∃ a ∈ s, f a = c

Tactic:
simpa using hl hc

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ t

Tactic:
refine ((mem_inter_iff x t (mulSupport f)).mp ?_).1

Goal state after:
case refine_1
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ s
⊢ x ∈ ↑t ∩ mulSupport f
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ioi i ↔ x✝ ∈ Iio i.rev

Tactic:
simp [lt_rev_iff]

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
m : M
s : Set M
⊢ m ∈ span R s ↔ ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = m

Tactic:
by
  conv_lhs => rw [← Set.image_id s]
  exact Finsupp.mem_span_image_iff_linearCombination R (v := _root_.id (α := M))

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
n : ℕ
f : Fin n → R
g : Fin n → ↑s
⊢ ∃ x, (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i, (x i).1 • (x i).2 = ∑ i, f i • ↑(g i)

Tactic:
exact ⟨fun i ↦ (f i, g i), fun i ↦ (g i).2, rfl⟩

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case pos.succ
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h : ↑⟨i + 1, hi⟩ < m + 1
⊢ vecCons x u ⟨↑⟨i + 1, hi⟩, h⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨i + 1, hi⟩

Tactic:
simp only [Nat.add_lt_add_iff_right] at h
      simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : f a = 1
⊢ 1 * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
one_mul

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : f a = 1
⊢ ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n k : ℕ
h : k < n
⊢ (finRotate (n + 1)) ⟨k, ⋯⟩ = ⟨k + 1, ⋯⟩

Tactic:
ext
  dsimp [finRotate_succ]
  simp [finAddFlip_apply_mk_left h, Nat.add_comm]

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

Goal state before:
pp: case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)

Tactic:
have H : ¬ (fun i ↦ (f i : R)).HasFiniteMulSupport :=
      fun h ↦ hf <| h.of_comp cast_one cast_injective

Goal state after:
case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
H : ¬HasFiniteMulSupport fun i ↦ ↑(f i)
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
⊢ f i = (Finsupp.lapply i) (Finsupp.single i (f i))

Tactic:
Finsupp.lapply_apply,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
⊢ f i = (Finsupp.single i (f i)) i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
⊢ (Finsupp.lapply i) (Finsupp.single j (f j)) = 0

Tactic:
Finsupp.lapply_apply,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
⊢ (Finsupp.single j (f j)) i = 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ ∏ i, f i = ∏ i, f (castAdd b i)

Tactic:
by
  rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : LinearIndependent R v
w : ι → G
⊢ LinearIndependent R (w • v)

Tactic:
rw [linearIndependent_iff''ₛ] at hv ⊢

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → G
⊢ ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • (w • v) i = ∑ i ∈ s, g i • (w • v) i → ∀ (i : ι), f i = g i