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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective ⇑(f' ^ n)
⊢ Surjective ⇑f'

Tactic:
rw [← Nat.succ_pred_eq_of_pos (Nat.pos_iff_ne_zero.mpr hn), pow_succ', coe_mul] at h
  exact Surjective.of_comp h

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

Goal state before:
pp: R : Type u_9
A : Type u_10
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
u v : Aˣ
x : A
⊢ (mulRightLinearEquiv R (u * v)) x = (mulRightLinearEquiv R v) ((mulRightLinearEquiv R u) x)

Tactic:
by simp [mul_assoc]

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

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
⊢ map (a • f) p ≤ map f p

Tactic:
rw [map_le_iff_le_comap, comap_smul f _ a h, ← map_le_iff_le_comap]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
f : M → N
hf : ∀ (x y : M), f (x * y) = f x * f y
⊢ ∀ {a b : N}, a ∈ Set.range f → b ∈ Set.range f → a * b ∈ Set.range f

Tactic:
exact srange_mk_aux_mul hf

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
simp only [Subsemiring.mem_toNonUnitalSubsemiring, subsemiringClosure_mem] at hx
    induction hx using AddSubmonoid.closure_induction <;> aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ x ∈ closure s ↔ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
constructor
  · intro hx
    rw [mem_closure_iff] at hx
    induction hx using AddSubmonoid.closure_induction with
    | mem x hx =>
      suffices ∃ t : List R, (∀ y ∈ t, y ∈ s) ∧ t.prod = x from
        let ⟨t, ht1, ht2⟩ := this
        ⟨[t], List.forall_mem_singleton.2 ht1, by
          rw [List.map_singleton, List.sum_singleton, ht2]⟩
      induction hx using Submonoid.closure_induction with
      | mem x hx => exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩
      | one => exact ⟨[], List.forall_mem_nil _, rfl⟩
      | mul x y _ _ ht hu =>
        obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu
        exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩
    | zero => exact ⟨[], List.forall_mem_nil _, rfl⟩
    | add x y _ _ hL hM =>
      obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM
      exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by
        rw [List.map_append, List.sum_append, HL2, HM2]⟩
  · rintro ⟨L, HL1, rfl⟩
    exact
      list_sum_mem fun r hr =>
        let ⟨t, ht1, ht2⟩ := List.mem_map.1 hr
        ht2 ▸ list_prod_mem _ fun y hy => subset_closure <| HL1 t ht1 y hy

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
s : Set R
x : R
hx : x ∈ closure s
⊢ f x ∈ closure (⇑f '' s)

Tactic:
← f.map_closure,

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ f x ∈ map f (closure s)
Module: Mathlib.Algebra.Prime.Lemmas

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

Tactic:
rw [mul_comm, prime_units_mul]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
⊢ IsLUB {a | IsAtom a ∧ a ≤ b} b

Tactic:
rcases isLUB_atoms b with ⟨s, hsb, hs⟩
  exact ⟨fun c hc ↦ hc.2, fun c hc ↦ hsb.2 fun i hi ↦ hc ⟨hs _ hi, hsb.1 hi⟩⟩

Goal state after:
Module: Mathlib.Order.Atoms

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

Tactic:
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.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : j ∈ {i}
hj : j ∉ s
⊢ Disjoint (f j) (s.sup f)

Tactic:
rw [eq_empty_of_ssubset_singleton ⟨hs, fun h => hj (h hji)⟩, sup_empty]
    exact disjoint_bot_right

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
h_inf : x ⊓ a = x
⊢ x ≤ a

Tactic:
rwa [inf_eq_left] at h_inf

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ j, ⨆ (_ : j ≠ f i'), t j)

Tactic:
rw [← hf.iSup_comp]

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i' : ι'
⊢ Disjoint (t (f i')) (⨆ x, ⨆ (_ : f x ≠ f i'), t (f x))
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥
⊢ (⨆ i_1, ⨆ (_ : t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1) ⊔ ⨆ i_1, ⨆ (_ : ¬t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1 =
    ⨆ i_1, ⨆ (h : t i_1 ≠ ⊥), ⨆ (_ : ⟨i_1, h⟩ ≠ ⟨i, hi⟩), t ↑⟨i_1, h⟩

Tactic:
simp only [iSup_comm (ι' := _ ≠ i), this, ne_eq, sup_of_le_right, Subtype.mk.injEq, iSup_bot,
    bot_le]

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : Algebra R A
h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
x : R
y : S
z : A
⊢ (x • y) • z = x • y • z

Tactic:
simp_rw [Algebra.smul_def, map_mul, mul_assoc, h]

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
by_cases h : a ∈ s
  · exact Or.inr (mulIndicator_of_mem h f)
  · exact Or.inl (mulIndicator_of_notMem h f)

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ (↑↑↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
by
      rw [algebraMap_apply R S A, algebraMap_apply R S B]
      exact f.commutes (algebraMap R S r)

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : ℕ →o α
n : ℕ
hn : a n = sSup (range ⇑a)
m : ℕ
hm : n ≤ m
⊢ ¬a n < a m

Tactic:
rw [hn]

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
a : ℕ →o α
n : ℕ
hn : a n = sSup (range ⇑a)
m : ℕ
hm : n ≤ m
⊢ ¬sSup (range ⇑a) < a m
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A ≃ₐ[S] B
r : R
⊢ f.toRingEquiv.toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
by
      rw [algebraMap_apply R S A, algebraMap_apply R S B]
      exact f.commutes (algebraMap R S r)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x = ⊥

Tactic:
rw [← hs, eq_comm, inf_eq_left]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x ≤ sSup s
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
s : Finset ι
⊢ (∏ i ∈ s, if p i then 1 else 0) = if ∀ i ∈ s, p i then 1 else 0

Tactic:
by
  rw [prod_ite_zero, prod_const_one]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
T : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : S
a : Set S
hx : x ∈ span R a
⊢ (algebraMap S T) x ∈ span R (⇑(algebraMap S T) '' a)

Tactic:
by
  rw [span_algebraMap_image_of_tower, mem_map]
  exact ⟨x, hx, rfl⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
⊢ a ⊓ sSup ↑t = ⊥

Tactic:
have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
h' : a ⊓ sSup (↑(insert a t) \ {a}) = ⊥
⊢ a ⊓ sSup ↑t = ⊥

case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
⊢ ↑(insert a t) ⊆ s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
h' : a ⊓ sSup (↑(insert a t) \ {a}) = ⊥
⊢ a ⊓ sSup ↑t = ⊥

Tactic:
rwa [Finset.coe_insert, Set.insert_sdiff_self_of_notMem] at h'

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
h' : a ⊓ sSup (insert a ↑t \ {a}) = ⊥
⊢ a ∉ ↑t
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
hp₁ : {x | x ∈ ⟦l₁⟧ ∧ p x}.Subsingleton
hp₂ : {x | x ∈ ⟦l₂⟧ ∧ p x}.Subsingleton
x✝ : hp₁ ≍ hp₂
⊢ {x | x ∈ l₁ ∧ decide (p x) = true}.Subsingleton

Tactic:
simpa using hp₁

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ f.support.Nonempty ↔ f ≠ 0

Tactic:
by
  contrapose!; exact support_eq_empty

Goal state after:
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
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (f.prod fun x v ↦ if a = x then b x v else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
dsimp [Finsupp.prod]
  rw [f.support.prod_ite_eq]

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

Goal state before:
pp: case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a✝ : List R
h : ∀ (a : R), a ∈ a✝ → 0 < a
⊢ 0 < a✝.prod

Tactic:
apply List.prod_pos h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
s : Multiset α
a : α
ha : a ∈ s
⊢ f a ≤ (map f s).prod

Tactic:
by
  obtain ⟨s', rfl⟩ := exists_cons_of_mem ha
  rw [map_cons, prod_cons]
  calc f a = f a * 1 := (mul_one (f a)).symm
    _ ≤ f a * (s'.map f).prod := by
      gcongr
      · exact le_trans (zero_le_one' β) (h1 a)
      · simp_all [one_le_prod]

Goal state after:
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
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ ∏ i ∈ insert a s, f i = ∏ i ∈ insert a s, g i ↔ ∀ i ∈ insert a s, f i = g i

Tactic:
Finset.prod_insert ha,

Goal state after:
ι : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ f a * ∏ x ∈ s, f x = ∏ i ∈ insert a s, g i ↔ ∀ i ∈ insert a s, f i = g 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
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ f a * ∏ x ∈ s, f x = ∏ i ∈ insert a s, g i ↔ ∀ i ∈ insert a s, f i = g i

Tactic:
Finset.prod_insert ha,

Goal state after:
ι : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ f a * ∏ x ∈ s, f x = g a * ∏ x ∈ s, g x ↔ ∀ i ∈ insert a s, f i = g i
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
αs : ι → Type u_12
inst✝³ : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst✝² : Fintype η
ιs✝ : η → Type u_14
inst✝¹ : Zero α✝
α : Type u_15
ιs : η → Type u_16
inst✝ : AddMonoid α
f g : (j : η) × ιs j →₀ α
⊢ sigmaFinsuppEquivPiFinsupp.toFun (f + g) = sigmaFinsuppEquivPiFinsupp.toFun f + sigmaFinsuppEquivPiFinsupp.toFun g

Tactic:
ext
      simp

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

Goal state before:
pp: case single_add
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
x : α
a : M
l : α →₀ M
a✝¹ : x ∉ l.support
a✝ : a ≠ 0
ih : l ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
⊢ single x a + l ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))

Tactic:
| single_add x a l _ _ ih =>

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

Goal state before:
pp: case pos
α : 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 : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ l x = 0 x

Tactic:
Finsupp.sum_eq_single x,

Goal state after:
case pos
α : 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 : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (single (f x) (l x)) (f x) = 0
⊢ l x = 0 x

case pos.h₀
α : 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 : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ ∀ (b : α), l b ≠ 0 → b ≠ x → (single (f b) (l b)) (f x) = 0

case pos.h₁
α : 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 : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ l x = 0 → (single (f x) 0) (f x) = 0
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ some ((finSuccAboveEquiv p).symm x) = some ((p.castLT ⋯).predAbove ↑x)

Tactic:
simpa [finSuccAboveEquiv] using finSuccEquiv'_ne_last_apply h x.property

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)

Tactic:
classical
    by_cases hs : (s ∩ mulSupport (f ∘ g)).Finite
    · have hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y := by
        simpa only [hs.mem_toFinset]
      have := finprod_mem_eq_prod (comp f g) hs
      unfold Function.comp at this
      rw [this, ← Finset.prod_image hg]
      refine finprod_mem_eq_prod_of_inter_mulSupport_eq f ?_
      rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
    · unfold Function.comp at hs
      rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]
      rwa [image_inter_mulSupport_eq, infinite_image_iff hg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ range g), f i = ∏ᶠ (j : β), f (g j)

Tactic:
rw [← image_univ, finprod_mem_image', finprod_mem_univ]
  rwa [univ_inter]

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

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

Tactic:
vecAlt0,

Goal state after:
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ vecAppend ⋯ v v ⟨↑i + ↑i, ⋯⟩ = v (i + i)
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 :
  ∀ (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 ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i : ι
⊢ g₁ i = g₂ i

Tactic:
refine (Group.isUnit (w i)).smul_left_cancel.mp ?_

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 ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i : ι
⊢ w i • g₁ i = w i • g₂ i
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rcases lt_or_ge c b with h | h

Goal state after:
case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
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
v : ι → M
w : ι → Rˣ
h : LinearIndependent R (w • v)
⊢ LinearIndependent R v

Tactic:
convert! h.units_smul (fun i ↦ (w i)⁻¹)

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → Rˣ
h : LinearIndependent R (w • v)
⊢ v = (fun i ↦ (w i)⁻¹) • w • v
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
⊢ range v = w

Tactic:
specialize
      p w ((↑) : w → M) i' (fun i => ⟨v i, range_subset_iff.mp h i⟩)
        (by
          ext
          simp)

Goal state after:
case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
p : Surjective fun i ↦ ⟨v i, ⋯⟩
⊢ range v = w
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case zero
ι : Type u_1
M : Type u_2
m : ℕ
a : Fin (m ^ 0)
b : Fin 0
⊢ ↑a / m ^ ↑b % m < m

pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
b : Fin (n + 1)
⊢ ↑a / m ^ ↑b % m < m

Tactic:
· exact b.elim0

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
b : Fin (n + 1)
⊢ ↑a / m ^ ↑b % m < m
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
h : a ≤ b
⊢ (∃ c, b - a = n * c) ↔ ∃ t, b = a + n * t

Tactic:
exact exists_congr (fun _ => Nat.sub_eq_iff_eq_add' h)

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

Goal state before:
pp: case zero
ι : Type u_1
M : Type u_2
n : Fin 0 → ℕ
a : Fin (∏ i, n i)
b : Fin 0
⊢ (↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b < n b

pp: case succ
ι : Type u_1
M : Type u_2
n✝ : ℕ
n : Fin (n✝ + 1) → ℕ
a : Fin (∏ i, n i)
b : Fin (n✝ + 1)
⊢ (↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b < n b

Tactic:
· exact b.elim0

Goal state after:
case succ
ι : Type u_1
M : Type u_2
n✝ : ℕ
n : Fin (n✝ + 1) → ℕ
a : Fin (∏ i, n i)
b : Fin (n✝ + 1)
⊢ (↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b < n b
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
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)

Tactic:
by
  rw [Module.rank]
  refine le_trans ?_ (lift_le.mpr <| le_ciSup bddAbove_of_small ⟨_, hv.linearIndepOn_id⟩)
  exact lift_mk_le'.mpr ⟨(Equiv.ofInjective _ hv.injective).toEmbedding⟩

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.encard = ↑s.toFinset.card

Tactic:
have h := toFinite s

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ s.encard = ↑s.toFinset.card