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

Goal state before:
pp: case cons.inr.nil
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
HL' : ∀ x ∈ [], x ∈ s
⊢ C (-[].prod)

Tactic:
exact hneg1

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : a = b
⊢ a * ↑1 = b

Tactic:
by rwa [Units.val_one, mul_one]

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 : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
⊢ (f.domRestrict S).range ≤ f.range

Tactic:
by
  rintro x ⟨⟨y, hy⟩, rfl⟩
  exact LinearMap.mem_range_self f y

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✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
⊢ ∀ (x y : M₁),
    ↑e ∘ₗ codRestrict i.range (f (x + y)) ⋯ = ↑e ∘ₗ codRestrict i.range (f x) ⋯ + ↑e ∘ₗ codRestrict i.range (f y) ⋯

Tactic:
intro x₁ x₂; ext y; simp [f.map_add, ← e.map_add, codRestrict]

Goal state after:
Module: Mathlib.Order.ModularLattice

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

Tactic:
sup_eq_right.2 x.prop.1

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc (a ⊓ b) a)
⊢ ↑x = ↑x
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (c ⊔ b) a

Tactic:
rwa [sup_comm, disjoint_comm] at hsup

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

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
s : AddSubmonoid M
⊢ (span ℕ ↑s).toAddSubmonoid = s

Tactic:
by
  rw [span_nat_eq_addSubmonoidClosure, s.closure_eq]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : IsModularLattice α
a b c : α
inst✝² : BoundedOrder α
inst✝¹ : ComplementedLattice α
inst✝ : Fact (a ≤ b)
x✝ : ↑(Icc a b)
x : α
ha : a ≤ x
hb : x ≤ b
⊢ ∃ b_1, IsCompl ⟨x, ⋯⟩ b_1

Tactic:
simp_rw [Set.Icc.isCompl_iff]

Goal state after:
α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : IsModularLattice α
a b c : α
inst✝² : BoundedOrder α
inst✝¹ : ComplementedLattice α
inst✝ : Fact (a ≤ b)
x✝ : ↑(Icc a b)
x : α
ha : a ≤ x
hb : x ≤ b
⊢ ∃ b_1, x ⊓ ↑b_1 = a ∧ x ⊔ ↑b_1 = b
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
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
y₁ : M
hy₁ : y₁ ∈ p
z₁ : M
hz₁ : z₁ ∈ p'
y₂ : M
hy₂ : y₂ ∈ p
z₂ : M
hz₂ : z₂ ∈ p'
⊢ y₁ + y₂ + (z₁ + z₂) = y₁ + z₁ + (y₂ + z₂)

Tactic:
rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm y₂]

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
r : R
hr : IsUnit r
x : M
⊢ R ∙ r • x = R ∙ x

Tactic:
by
  lift r to Rˣ using hr
  rw [← Units.smul_def]
  exact span_singleton_group_smul_eq R r x

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

Tactic:
by
  cases isEmpty_or_nonempty ι
  · simpa [iSup_of_empty]
  · exact hs.iSup_mem_of_nonempty hf

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

Goal state before:
pp: case zero
R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h : ∀ y ∈ s, Commute y x
y : A
⊢ Commute 0 x

Tactic:
exact .zero_left _

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : α
hx : x ∈ s
⊢ x ∈ S

Tactic:
(Mathlib.Tactic.useSyntax
 "use"
 []
 (group)
 [(choice
   («term{_}» "{" [`x] "}")
   (Term.structInst
    "{"
    []
    (Term.structInstFields [(Term.structInstField (Term.structInstLVal `x []) [])])
    (Term.optEllipsis [])
    []
    "}"))])

Goal state after:
case h
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : α
hx : x ∈ s
⊢ ↑{x} ⊆ s ∧ x = {x}.sup id
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: case insert
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a✝ : ι
s✝ : Finset ι
ha : a✝ ∉ s✝
ih : ∏ x ∈ s✝, f x = 0 ↔ ∃ a ∈ s✝, f a = 0
⊢ ∏ x ∈ insert a✝ s✝, f x = 0 ↔ ∃ a ∈ insert a✝ s✝, f a = 0

Tactic:
| insert _ _ ha ih =>

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0

Tactic:
rw [Ne, prod_eq_zero_iff]
  push Not; rfl

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

Goal state before:
pp: case mpr.add
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ x y : M
hx : x ∈ span R S
hy : y ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
hy' : f ⟨y, hy⟩ = g ⟨y, hy⟩
⊢ g ⟨x, hx⟩ + f ⟨y, hy⟩ = g ⟨x, hx⟩ + g ⟨y, hy⟩

Tactic:
hy'

Goal state after:
case mpr.add
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ x y : M
hx : x ∈ span R S
hy : y ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
hy' : f ⟨y, hy⟩ = g ⟨y, hy⟩
⊢ g ⟨x, hx⟩ + g ⟨y, hy⟩ = g ⟨x, hx⟩ + g ⟨y, hy⟩
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x y : ↥p
hxy : (inclusionSpan S p) x = (inclusionSpan S p) y
⊢ x = y

Tactic:
Subtype.ext_iff

Goal state after:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x y : ↥p
hxy : ↑((inclusionSpan S p) x) = ↑((inclusionSpan S p) y)
⊢ x = y
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i ↦ s i) i = w✝
⊢ Disjoint a (sSup ((⋃ i, s i) \ {a}))

Tactic:
exfalso

Goal state after:
case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i ↦ s i) i = w✝
⊢ False
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : ¬Nonempty η
⊢ sSupIndep (⋃ i, s i)

Tactic:
rintro a ⟨_, ⟨i, _⟩, _⟩
    exfalso
    exact hη ⟨i⟩

Goal state after:
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
⊢ ∏ i ∈ s, (f i).indicator g = (⋂ x ∈ s, f x).indicator (g ^ #s)

Tactic:
simp [prod_indicator]

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
x : M
⊢ IsCompactElement (R ∙ x)

Tactic:
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ ∀ (s : Set (Submodule R M)), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → R ∙ x ≤ sSup s → ∃ x_1 ∈ s, R ∙ x ≤ x_1
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg.inl
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
con : ⟨c, ⋯⟩ = ⊥
⊢ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
exfalso

Goal state after:
case neg.inl
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
con : ⟨c, ⋯⟩ = ⊥
⊢ False
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✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
f : M →ₛₗ[σ₁₂] M₂
inst✝ : RingHomSurjective σ₁₂
p q : Submodule R₂ M₂
hf : Injective ⇑f
hp : p ≤ f.range
hq : q ≤ f.range
⊢ p ⊔ q ≤ f.range

Tactic:
simp [sup_le_iff, hp, hq]

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 ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.pi fun x ↦ {True, False}, (fun a_1 x ↦ a_1 ∈ s ∧ ∃ (h : a_1 ∈ s), a a_1 h) = a

Tactic:
funext_iff,

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.pi fun x ↦ {True, False}, ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) = a x x_1
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Submodule R M
x : M
⊢ Disjoint s (R ∙ x) ↔ ∀ (r : R), r • x ∈ s → r • x = 0

Tactic:
by
  rw [disjoint_comm]; simp +contextual [disjoint_def, mem_span_singleton]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
⊢ erase a (f + f') = erase a f + erase a f'

Tactic:
ext s; by_cases hs : s = a
  · rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
  rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case pos
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
hda : d a = 1
hda' : ∀ (i : α), i ≠ a → d i = 0
b : α
hb : b = a
⊢ d b = (single a 1) b

pp: case neg
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
hda : d a = 1
hda' : ∀ (i : α), i ≠ a → d i = 0
b : α
hb : ¬b = a
⊢ d b = (single a 1) b

Tactic:
· rw [hb, single_eq_same, hda]

Goal state after:
case neg
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
hda : d a = 1
hda' : ∀ (i : α), i ≠ a → d i = 0
b : α
hb : ¬b = a
⊢ d b = (single a 1) b
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_1
d : α →₀ ℕ
⊢ (∃ a, d = single a 1) → (d.sum fun x n ↦ n) = 1

Tactic:
· rintro ⟨a, rfl⟩
    rw [sum_eq_single a ?_ (fun _ ↦ rfl), single_eq_same]
    exact fun _ _ hba ↦ single_eq_of_ne hba

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
s✝ : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
⊢ (g a).prod h * (∑ i ∈ s, g i).prod h = (g a + ∑ x ∈ s, g x).prod h

Tactic:
prod_add_index' h_zero h_add

Goal state after:
α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
s✝ : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
⊢ (g a).prod h * (∑ i ∈ s, g i).prod h = (g a).prod h * (∑ x ∈ s, g x).prod h
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
⊢ Injective (mapDomain f)

Tactic:
intro v₁ v₂ eq
  ext a
  have : mapDomain f v₁ (f a) = mapDomain f v₂ (f a) := by rw [eq]
  rwa [mapDomain_apply hf, mapDomain_apply hf] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ (∀ (a : α), f a ∉ l.support) → ∀ (a : β), a ∉ l.support

Tactic:
intro h a ha

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
h : ∀ (a : α), f a ∉ l.support
a : β
ha : a ∈ l.support
⊢ False
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
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
| l

Tactic:
rw [← embDomain_comapDomain (f := ⟨f, hf⟩) hl (M := M), embDomain_eq_mapDomain]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
| mapDomain (⇑{ toFun := f, inj' := hf }) (comapDomain (⇑{ toFun := f, inj' := hf }) l ⋯)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
s : Finset ι
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h₁ : ∏ i ∈ s, f i = 1
h₂ : ∃ i ∈ s, f i ≠ 1
⊢ ∃ i ∈ s, 1 < f i

Tactic:
by
  contrapose! h₁
  obtain ⟨i, m, i_ne⟩ : ∃ i ∈ s, f i ≠ 1 := h₂
  apply ne_of_lt
  calc
    ∏ j ∈ s, f j < ∏ j ∈ s, 1 := prod_lt_prod' h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩
    _ = 1 := prod_const_one

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

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

Tactic:
smul_mul_smul_comm,

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ (∀ (x y : α), x ∈ m.toFinset → y ∈ m.toFinset → count x m - 1 ≠ 0 → count y m - 1 ≠ 0 → x = y ∧ count x m - 1 = 1) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2

Tactic:
simp only [← pos_iff_ne_zero, Nat.sub_pos_iff_lt, mem_toFinset, Nat.pred_eq_succ_iff]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ (∀ (x y : α), x ∈ m → y ∈ m → 1 < count x m → 1 < count y m → x = y ∧ count x m = 0 + 2) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ mulSupport ((fun x ↦ f (g x)) ∘ PLift.down) ⊆ ↑(Finite.toFinset h)

Tactic:
rw [h.coe_toFinset]

Goal state after:
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ mulSupport ((fun x ↦ f (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R s = (linearCombination R Subtype.val).range

Tactic:
range_linearCombination,

Goal state after:
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R s = span R (Set.range Subtype.val)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
v : ι → M
a✝ : ι
⊢ ((linearCombination R v ∘ₗ ↑(addSingleEquiv i c h₀)) ∘ₗ lsingle a✝) 1 =
    (linearCombination R (v + fun x ↦ c x • v i) ∘ₗ lsingle a✝) 1

Tactic:
simp [addSingleEquiv]

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
x✝ : Fin n
⊢ vecAppend ⋯ ![] v x✝ = v x✝

Tactic:
simp [vecAppend_eq_ite]

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
x✝ : Fin (n + 0)
⊢ vecAppend ⋯ v ![] x✝ = v x✝

Tactic:
simp [vecAppend_eq_ite]

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

Goal state before:
pp: case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, (fun i ↦ ↑(t i)) i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i ↦ ↑(t i)) i), f a

Tactic:
← biUnion_univ,

Goal state after:
case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ univ, ↑(t x)), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i ↦ ↑(t i)) i), f a
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Ico a.castSucc b.castSucc, f i = ∏ i ∈ Ico a b, f i.castSucc

Tactic:
simp [← map_castSuccEmb_Ico]

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

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

Tactic:
by
  rw [Coprime, Coprime, gcd_add_self_right]

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

Goal state before:
pp: m n : ℕ
⊢ m.Coprime n ↔ IsRelPrime m n

Tactic:
simp_rw [coprime_iff_gcd_eq_one, IsRelPrime, ← and_imp, ← dvd_gcd_iff, isUnit_iff_dvd_one]
  exact ⟨fun h _ ↦ (h ▸ ·), (dvd_one.mp <| · dvd_rfl)⟩

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

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

Tactic:
by
  rw [modEq_iff_dvd] at *
  exact (dvd_mul_left (n : ℤ) (m : ℤ)).trans h

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
⊢ ∀ (x_1 : Fin n → ℕ),
    (∀ (a : Fin (∏ i, x_1 i)), ⟨∑ i, (↑a / ∏ j, x_1 (Fin.castLE ⋯ j)) % x_1 i * ∏ j, x_1 (Fin.castLE ⋯ j), ⋯⟩ = a) →
      ∀ (a : Fin (∏ i, Fin.cons x x_1 i)),
        ⟨∑ i, (↑a / ∏ j, Fin.cons x x_1 (Fin.castLE ⋯ j)) % Fin.cons x x_1 i * ∏ j, Fin.cons x x_1 (Fin.castLE ⋯ j),
            ⋯⟩ =
          a

Tactic:
xs

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
⊢ (∀ (a : Fin (∏ i, xs i)), ⟨∑ i, (↑a / ∏ j, xs (Fin.castLE ⋯ j)) % xs i * ∏ j, xs (Fin.castLE ⋯ j), ⋯⟩ = a) →
    ∀ (a : Fin (∏ i, Fin.cons x xs i)),
      ⟨∑ i, (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % Fin.cons x xs i * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j), ⋯⟩ = a
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
⊢ Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α

Tactic:
simp [Nat.card, mk_eq_zero_iff, aleph0_le_mk_iff]

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

Goal state before:
pp: case inr
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
x✝ : ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ((∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0)
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
hgi : f i ≠ 0
⊢ ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ∃ i ∈ s, f i ≠ 0

Tactic:
· exact ⟨t, s, f, hst.symm, heq.symm, i, hi, hgi⟩

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

Goal state before:
pp: case zero
⊢ Nat.card (ZMod 0) = 0

pp: case succ
n✝ : ℕ
⊢ Nat.card (ZMod (n✝ + 1)) = n✝ + 1

Tactic:
· exact @Nat.card_eq_zero_of_infinite _ Int.infinite

Goal state after:
case succ
n✝ : ℕ
⊢ Nat.card (ZMod (n✝ + 1)) = n✝ + 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
t : Finset ι
f : ι → R
h : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0

Tactic:
exact h.1 i hi

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ (t \ s).encard + s.encard = t.encard

Tactic:
by
  rw [← encard_union_eq disjoint_sdiff_left, sdiff_union_of_subset h]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Finite

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : Monoid.FG M
hS : Monoid.FG ↥S
⊢ Monoid.FG (Localization S)

Tactic:
exact Monoid.fg_of_surjective mkHom mkHom_surjective

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
⊢ LinearIndepOn R v ↑s ↔ ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0

Tactic:
by
  classical
  simp_rw [LinearIndepOn, Fintype.linearIndependent_iff]
  constructor
  · rintro hv f hf i hi
    rw [← s.sum_attach] at hf
    exact hv (f ∘ Subtype.val) hf ⟨i, hi⟩
  · rintro hv f hf₀ i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (by simpa +contextual [← s.sum_attach]) i

Goal state after: