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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
y : M
u : Mˣ
⊢ Prime (↑u * y) ↔ Prime y

Tactic:
by simp [Prime]

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

Goal state before:
pp: M : Type u_1
inst✝ : MonoidWithZero M
a : M
h : a ~ᵤ 0
⊢ a = 0

Tactic:
let ⟨u, h⟩ := h.symm

Goal state after:
M : Type u_1
inst✝ : MonoidWithZero M
a : M
h✝ : a ~ᵤ 0
u : Mˣ
h : 0 * ↑u = a
⊢ a = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = 0
ha0 : ¬a = 0
con : a * c = 0
⊢ False

Tactic:
apply ha0 a_eq

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
hf : Function.Surjective ⇑f
t : Subring S
⊢ t ≤ f.range

Tactic:
simp [hf]

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

Goal state before:
pp: case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x * (a * b) = 0

Tactic:
· rw [mul_comm a b, ← mul_assoc, h', zero_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b c d : Associates M
h₁ : a ≤ b
h₂ : c ≤ d
x : Associates M
hx : b = a * x
y : Associates M
hy : d = c * y
⊢ b * d = a * c * (x * y)

Tactic:
by simp [hx, hy, mul_comm, mul_left_comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ a * b

Tactic:
exact le_mul_right

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Set α
⊢ s • 0 ⊆ 0

Tactic:
simp [subset_def, mem_smul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
t : Set β
⊢ 0 • t ⊆ 0

Tactic:
simp [subset_def, mem_smul]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
⊢ ∀ (c : ↥q), (p.subtype.domRestrict q) c ∈ map p.subtype q

Tactic:
rintro ⟨x, hx⟩; exact ⟨x, hx, rfl⟩

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

Goal state before:
pp: case refine_1
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ x ∈ p

Tactic:
rcases hx with ⟨⟨_, h⟩, _, rfl⟩

Goal state after:
case refine_1
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
val✝ : M
h : val✝ ∈ p
left✝ : ⟨val✝, h⟩ ∈ ↑q
⊢ p.subtype ⟨val✝, h⟩ ∈ p
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: case refine_2
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ ⟨x, ⋯⟩ ∈ q

Tactic:
rcases hx with ⟨⟨_, h⟩, _, rfl⟩

Goal state after:
case refine_2
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
val✝ : M
h : val✝ ∈ p
left✝ : ⟨val✝, h⟩ ∈ ↑q
⊢ ⟨p.subtype ⟨val✝, h⟩, ⋯⟩ ∈ q
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
h : ↑x ⊔ b ≤ ↑y ⊔ b
⊢ a ⊓ (↑x ⊔ b) ≤ a ⊓ (↑y ⊔ b)

Tactic:
exact inf_le_inf_left _ h

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
hbot : ¬x ⊓ yᶜ = ⊥
a : α
ha : IsAtom a
hle : a ≤ x ⊓ yᶜ
hx : a ≤ x
hy' : a ≤ yᶜ
hy : a ≤ y
this : a ≤ y ⊓ yᶜ
⊢ a = ⊥

Tactic:
simpa using this

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w x y z : M
a : R
⊢ (∃ b c, a • x + b • y + c • z = w) → ∃ z_1, (∃ a b, a • y + b • z = z_1) ∧ w = a • x + z_1

Tactic:
· rintro ⟨b, c, rfl⟩
    exact ⟨b • y + c • z, ⟨b, c, rfl⟩, by rw [add_assoc]⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
rw [← sSup_image]

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
⊢ IsLUB s (if ⊤ ∈ s then ⊤ else ⊥)

Tactic:
by
      refine ⟨fun x h ↦ ?_, fun x h ↦ ?_⟩
      · rcases eq_bot_or_eq_top x with (rfl | rfl)
        · exact bot_le
        · rw [if_pos h]
      · rcases eq_bot_or_eq_top x with (rfl | rfl)
        · rw [if_neg]
          intro con
          exact bot_ne_top (eq_top_iff.2 (h con))
        · exact le_top

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
rw [← sSup_image]

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s
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

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

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

Goal state after:
case mpr
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ Disjoint a b → sSupIndep {a, b}
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
b : R
c : S
x✝ : c ∈ span R s
hc : c • x ∈ span R (s • t)
⊢ (b • c) • x ∈ span R (s • t)

Tactic:
rw [IsScalarTower.smul_assoc]

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
b : R
c : S
x✝ : c ∈ span R s
hc : c • x ∈ span R (s • t)
⊢ b • c • x ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0✝ : S
y : A
hy✝ : y ∈ t
r : R
s0 : S
hx✝ : s0 ∈ span R s
hy : s0 • y ∈ span R (s • t)
⊢ (r • s0) • y ∈ span R (s • t)

Tactic:
rw [IsScalarTower.smul_assoc]

Goal state after:
case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0✝ : S
y : A
hy✝ : y ∈ t
r : R
s0 : S
hx✝ : s0 ∈ span R s
hy : s0 • y ∈ span R (s • t)
⊢ r • s0 • y ∈ span R (s • t)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
le_inf_iff

Goal state after:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ t, ↑t ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
le_inf_iff

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ t, ↑t ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ (embDomain f v) (f a) = v a

Tactic:
embDomain,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ { support := map f v.support,
        toFun := fun b ↦
          match Multiset.find? (fun a ↦ f a = b) v.support.val ⋯ with
          | some a => v a
          | none => 0,
        mem_support_toFun := ⋯ }
      (f a) =
    v a
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j)

Tactic:
prod_sub_ordered

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i ∈ s, 1 - ∑ i ∈ s, (f i * ∏ j ∈ s with j < i, (1 - f j)) * ∏ j ∈ s with i < j, 1 =
    1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

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

Tactic:
by_cases hyf : y ∈ f.support
  · exact Finsupp.mul_prod_erase f y g hyf
  · rw [notMem_support_iff.mp hyf, hg y, erase_of_notMem_support hyf, one_mul]

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

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

Tactic:
simp [indicator_apply, imp_false]

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
f g : ι → M₀
x : ι
⊢ (x ∈ support fun x ↦ f x * g x) ↔ x ∈ support f ∩ support g

Tactic:
simp [not_or]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
hf0 : ∀ (x : ι), 0 ≤ f x
hf : ∀ (x : ι), f x ≤ 1
x✝¹ x✝ : Finset ι
hst : x✝¹ ⊆ x✝
⊢ ∀ i ∈ x✝, i ∉ x✝¹ → f i ≤ 1

Tactic:
simp [hf]

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

Goal state before:
pp: α : Type u_12
M : Type u_13
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f.support = g.support

Tactic:
rw [← image_fst_graph, h, image_fst_graph]

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : α
xs : List α
⊢ 0 < x ∧ 0 < xs.prod ↔ 0 < x ∧ ∀ (x : α), x ∈ xs → 0 < x

Tactic:
list_prod_pos

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
a : α
h : ¬(mapDomain (⇑f) x) (f a) = 0
⊢ ∃ a_1, ¬x a_1 = 0 ∧ f a_1 = f a

Tactic:
exact ⟨a, by simpa [f.injective] using h⟩

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
v₁ : α →₀ M
⊢ ∀ ⦃a₂ : α →₀ M⦄, mapDomain f v₁ = mapDomain f a₂ → v₁ = a₂

Tactic:
v₂

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
⊢ mapDomain f v₁ = mapDomain f v₂ → v₁ = v₂
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 : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
⊢ ∀ ⦃x₂ : α →₀ M⦄, x₂ ∈ {w | ↑w.support ⊆ S} → mapDomain f v₁ = mapDomain f x₂ → v₁ = x₂

Tactic:
v₂

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
⊢ v₂ ∈ {w | ↑w.support ⊆ S} → mapDomain f v₁ = mapDomain f v₂ → v₁ = v₂
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
inst✝ : MulLeftMono N
hf : ∀ (x : ι), f x ≤ 1
x✝¹ x✝ : Finset ι
hst : x✝¹ ⊆ x✝
⊢ ∀ i ∈ x✝, i ∉ x✝¹ → f i ≤ 1

Tactic:
simp [hf]

Goal state after:
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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ ∀ ⦃a : α⦄ (x : Subtype P),
    x ∈ f.support ∧ (Embedding.subtype P) x = a → ¬∃ a_1 ∈ g.support, (Embedding.subtype fun a ↦ ¬P a) a_1 = a

Tactic:
Embedding.coe_subtype,

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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ ∀ ⦃a : α⦄ (x : Subtype P), x ∈ f.support ∧ ↑x = a → ¬∃ a_1 ∈ g.support, ↑a_1 = a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ i ∈ l.splitSupport ↔ l.split i ≠ 0

Tactic:
rw [splitSupport, mem_image, Ne, ← support_eq_empty, ← Ne,
    ← Finset.nonempty_iff_ne_empty, split, comapDomain, Finset.Nonempty]

Goal state after:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ (∃ a ∈ l.support, a.fst = i) ↔
    ∃ x, x ∈ { support := l.support.preimage (Sigma.mk i) ⋯, toFun := fun a ↦ l ⟨i, a⟩, mem_support_toFun := ⋯ }.support
Module: Mathlib.LinearAlgebra.Finsupp.Defs

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
a a' : α
h : a ≠ a'
⊢ lapply a ∘ₗ lsingle a' = 0

Tactic:
by ext; simp [h.symm]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ 0 • ⋯.choose = 0

Tactic:
· rw [zero_smul]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Iio ↑i ⊆ Iio n

Tactic:
exact Iio_subset_Iio i.is_lt.le

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

Tactic:
apply Finset.one_lt_prod'

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
⊢ ∀ i ∈ hf.toFinset, 1 ≤ f i

case hs
ι : 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
⊢ ∃ i ∈ hf.toFinset, 1 < f i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
j : Fin (n + m)
hj : j ∈ Ici (i.addNat m)
this : ↑i + m ≤ ↑j
⊢ j ∈ range fun x ↦ x.addNat m

Tactic:
refine ⟨⟨j - m, by lia⟩, ?_⟩

Goal state after:
n m : ℕ
i : Fin n
j : Fin (n + m)
hj : j ∈ Ici (i.addNat m)
this : ↑i + m ≤ ↑j
⊢ (fun x ↦ x.addNat m) ⟨↑j - m, ⋯⟩ = j
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : 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
x : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (c : R) (x : M), (fun i ↦ (b.reindexRange.repr (c • x)) ⟨b i, ⋯⟩) = c • fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩

pp: ι : 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
x : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (i : ι), (fun i_1 ↦ (b.reindexRange.repr (b i)) ⟨b i_1, ⋯⟩) = ⇑(single i 1)

Tactic:
· intro c x
    ext i
    simp

Goal state after:
ι : 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
x : M
i : ι
a✝ : Nontrivial R
⊢ ∀ (i : ι), (fun i_1 ↦ (b.reindexRange.repr (b i)) ⟨b i_1, ⋯⟩) = ⇑(single i 1)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = 1

Tactic:
← finprod_mem_one s

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ s), 1
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 : Finset M
x : M
⊢ (∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x) → x ∈ span R ↑s

Tactic:
by rintro ⟨f, -, rfl⟩; exact sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hx

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
k : Fin n
hk : ¬p k
⊢ #{i | p i} ≤ #(Iio k)

Tactic:
exact card_le_card (by 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
a b : α
h : a ≠ b
⊢ ∏ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a * f b

Tactic:
by
  rw [finprod_mem_insert, finprod_mem_singleton]
  exacts [h, finite_singleton b]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inl
n i : ℕ
hi : i < n
⊢ (Sum.inl ⟨i, hi⟩).isLeft = decide True

Tactic:
Sum.isLeft_inl,

Goal state after:
case inl
n i : ℕ
hi : i < n
⊢ true = decide True
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inl
n i : ℕ
hi : i < n
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)

Tactic:
simp_rw [finSumNatEquiv_symm_apply_of_lt hi, hi, Sum.isLeft_inl, decide_true]

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) = v ∘ fun n_1 ↦ n_1 + n_1

Tactic:
by
  ext i
  simp_rw [Function.comp, vecAlt0, vecAppend_eq_ite]
  split_ifs with h <;> congr
  · rw [Fin.val_mk] at h
    exact (Nat.mod_eq_of_lt h).symm
  · rw [Fin.val_mk, not_lt] at h
    simp only [Nat.mod_eq_sub_mod h]
    refine (Nat.mod_eq_of_lt ?_).symm
    lia

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
s : Multiset α
f : α → M
⊢ (map f s).prod = ∏ᶠ (a : α), f a ^ count a s

Tactic:
Finset.prod_multiset_map_count,

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
s : Multiset α
f : α → M
⊢ ∏ m ∈ s.toFinset, f m ^ count m s = ∏ᶠ (a : α), f a ^ count a s
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case e_a
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ∏ i, ∏ j ≤ i, f i.succ j = ∏ i, ∏ j ≥ i, f j.succ i

Tactic:
apply Finset.prod_comm'

Goal state after:
case e_a
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ∀ (x y : Fin n), x ∈ univ ∧ y ∈ Iic x ↔ x ∈ Ici y ∧ y ∈ univ
Module: Mathlib.Data.Nat.GCD.Basic

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

Tactic:
Coprime,

Goal state after:
m n : ℕ
⊢ m.gcd (n + m) = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ m.gcd (n + m) = 1 ↔ m.Coprime n

Tactic:
Coprime,

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

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

Tactic:
Coprime,

Goal state after:
m n : ℕ
⊢ (m + n).gcd n = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ (m + n).gcd n = 1 ↔ m.Coprime n

Tactic:
Coprime,

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

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

Tactic:
Coprime,

Goal state after:
m n : ℕ
⊢ (m + n).gcd m = 1 ↔ n.Coprime m
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ (m + n).gcd m = 1 ↔ n.Coprime m

Tactic:
Coprime,

Goal state after:
m n : ℕ
⊢ (m + n).gcd m = 1 ↔ n.gcd m = 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndepOn R v s ↔
    ∀ f ∈ Finsupp.supported R R s,
      ∀ g ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g

Tactic:
simp only [LinearIndepOn, linearIndependent_iffₛ, Finsupp.mem_supported,
    Finsupp.linearCombination_apply, Set.subset_def, Finset.mem_coe]
  refine ⟨fun h l₁ h₁ l₂ h₂ eq ↦ (Finsupp.subtypeDomain_eq_iff h₁ h₂).1 <| h _ _ <|
    (Finsupp.sum_subtypeDomain_index h₁).trans eq ▸ (Finsupp.sum_subtypeDomain_index h₂).symm,
    fun h l₁ l₂ eq ↦ ?_⟩
  refine Finsupp.embDomain_injective (Embedding.subtype (· ∈ s)) <| h _ ?_ _ ?_ ?_
  iterate 2 simpa using fun _ h _ ↦ h
  simp_rw [Finsupp.embDomain_eq_mapDomain]
  rwa [Finsupp.sum_mapDomain_index, Finsupp.sum_mapDomain_index] <;>
    intros <;> simp only [zero_smul, add_smul]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

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

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ m.gcd (n + k * m) = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

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

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ m.gcd (n + k * m) = 1 ↔ m.gcd n = 1