mathlib-initiative/mathlib-tactics huggingface dataset:
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 = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a = a * 1

Tactic:
mul_one

Goal state after:
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a = a
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 = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a * c = a * c * 1

Tactic:
mul_one

Goal state after:
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a * c = a * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
⊢ Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rcases of_irreducible_mul h.irreducible with hx | hy
    · exact Or.inr ⟨hx, (associated_unit_mul_left y x hx).prime h⟩
    · exact Or.inl ⟨(associated_mul_unit_left x y hy).prime h, hy⟩
  · rintro (⟨hx, hy⟩ | ⟨hx, hy⟩)
    · exact (associated_mul_unit_left x y hy).symm.prime hx
    · exact (associated_unit_mul_right y x hx).prime hy

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ p * b * ↑a = p * 1

Tactic:
mul_one

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ p * b * ↑a = p
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Set α
t : Set β
a x✝ : α
⊢ {x✝ • 0} = 0

Tactic:
rw [smul_zero, singleton_zero]

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 : R
⊢ x * 1 = x

Tactic:
mul_one

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 : R
⊢ 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)) = (algebraMap R A) (e.symm (e 1 * x)) * 1

Tactic:
mul_one

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
⊢ (algebraMap R A) (e.symm (e 1 * x)) = (algebraMap R A) (e.symm (e 1 * 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 1) * ((algebraMap R A) (e.symm (e 1 * x)) * e 1) = x

Tactic:
← Algebra.smul_def _ (e 1),

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
⊢ (algebraMap R A) (e.symm 1) * e.symm (e 1 * x) • e 1 = x
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Bijective ⇑f
x : M
⊢ (ofBijective f h).symm (f x) = x

Tactic:
by
  simp [LinearEquiv.symm_apply_eq]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a ⊔ f b ∈ ⇑f '' s

Tactic:
rw [← map_sup]

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f (a ⊔ b) ∈ ⇑f '' s
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
b : β
⊢ IsAtom (l (u b)) ↔ IsAtom b

Tactic:
gi.l_u_eq

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
b : β
⊢ IsAtom b ↔ IsAtom b
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥

Tactic:
by
  simp only [← bot_covBy_iff, Pi.covBy_iff, bot_apply, eq_comm]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
i : ι
x : ↑(Iic a)
ht : Disjoint (↑(t i)) (⨆ j, ⨆ (_ : j ≠ i), ↑(t j))
⊢ x ≤ t i → x ≤ ⨆ j, ⨆ (_ : j ≠ i), t j → x ≤ ⊥

Tactic:
← Set.Iic.coe_iSup

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
i : ι
x : ↑(Iic a)
ht : Disjoint ↑(t i) ↑(⨆ i_1, ⨆ (_ : i_1 ≠ i), t i_1)
⊢ x ≤ t i → x ≤ ⨆ j, ⨆ (_ : j ≠ i), t j → x ≤ ⊥
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
⊢ s.Finite

Tactic:
by
  classical
    by_contra! contra
    obtain ⟨t, ht₁, ht₂⟩ := CompleteLattice.WellFoundedGT.isSupFiniteCompact α s
    replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t := by
      have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.sdiff (Finset.finite_toSet _)
      obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
      exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩
    obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
    replace hs : x ⊓ sSup s = ⊥ := by
      have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)
      simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot
    apply hx₁
    rw [← hs, eq_comm, inf_eq_left]
    exact le_sSup hx₀

Goal state after:
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
hs : span R s = ⊤
t : Set A
k : S
x : A
hx : x ∈ span R t
⊢ k • x ∈ span R (s • t)

Tactic:
by
  rw [span_smul_of_span_eq_top hs]
  exact (span S t).smul_mem k (span_le_restrictScalars R S t hx)

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

Goal state before:
pp: case insert
F : Type u_8
α : Type u_9
β : Type u_10
ι : Type u_11
inst✝⁴ : FunLike F α β
inst✝³ : CommMonoid β
inst✝² : CommMonoid F
inst✝¹ : IsOneApply F α β
inst✝ : IsMulApply F α β
f : ι → F
x : α
i : ι
s : Finset ι
his : i ∉ s
h : (∏ i ∈ s, f i) x = ∏ i ∈ s, (f i) x
⊢ (∏ i ∈ insert i s, f i) x = ∏ i ∈ insert i s, (f i) x

Tactic:
simp [his, h]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

pp: case neg
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : ¬S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
· refine ⟨sSup S, IsCompactElement.directed_sSup_lt_of_lt h hS cC.directedOn SC, ?_⟩
      intro; apply le_sSup

Goal state after:
case neg
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : ¬S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub
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
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
⊢ ∀ (a : M) (b : M'), a ∈ p ⊔ p' → b ∈ q₁ ⊔ q₁' → (a, b) ∈ p.prod q₁ ⊔ p'.prod q₁'

Tactic:
intro xx yy hxx hyy

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
p p' : Submodule R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
xx : M
yy : M'
hxx : xx ∈ p ⊔ p'
hyy : yy ∈ q₁ ⊔ q₁'
⊢ (xx, yy) ∈ p.prod q₁ ⊔ p'.prod q₁'
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
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ y : ↥(⨆ i ∈ s, p i)
hy : y ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)
hx : (⨆ i ∈ s, p i).subtype y ∈ ⨆ i ∈ s, p i
x✝ : ⟨(⨆ i ∈ s, p i).subtype y, hx⟩ ∈ ⊤
this : (⨆ i ∈ s, p i).subtype y ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))
⊢ ⟨(⨆ i ∈ s, p i).subtype y, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)

Tactic:
exact hy

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
x y : M
hy : y ∈ ↑p
e : f y = f x
⊢ x ∈ p ⊔ f.ker

Tactic:
exact mem_sup.2 ⟨y, hy, x - y, by simpa using sub_eq_zero.2 e.symm, by simp⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s t : Set α
a : α
h : ¬a ∈ s ∩ t
f : α → M
⊢ (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a * 1

Tactic:
mul_one

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s t : Set α
a : α
h : ¬a ∈ s ∩ t
f : α → M
⊢ (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a
Module: Mathlib.Algebra.Group.Indicator

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

Tactic:
mul_one

Goal state after:
case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = 1
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 f
this : g x = 1
⊢ f x * 1 = f x

Tactic:
mul_one

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 f
this : g x = 1
⊢ f x = f x
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case pos
α : 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
⊢ f x * 1 = f x

Tactic:
mul_one

Goal state after:
case pos
α : 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
⊢ f x = f x
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 q : Submodule R M
hpq : Disjoint p q
hker : f.ker ≤ q
⊢ map f p ⊓ map f q = ⊥

Tactic:
map_inf_eq_map_inf_comap,

Goal state after:
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 q : Submodule R M
hpq : Disjoint p q
hker : f.ker ≤ q
⊢ map f (p ⊓ comap f (map f q)) = ⊥
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
G : Type u_6
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ (t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f

Tactic:
mulIndicator_sdiff h,

Goal state after:
α : Type u_1
G : Type u_6
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ t.mulIndicator f * (s.mulIndicator f)⁻¹ = t.mulIndicator f / s.mulIndicator f
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₂
⊢ List.find? (fun b ↦ decide (p b)) l₁ = List.find? (fun b ↦ decide (p b)) l₂

Tactic:
refine List.find?_eq_find?_of_perm h ?_

Goal state after:
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
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 ∈ {a_2 ∈ s | ∃ (h : a_2 ∈ s), a a_2 h}) = a

Tactic:
mem_filter,

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}, (fun a_1 x ↦ a_1 ∈ s ∧ ∃ (h : a_1 ∈ s), a a_1 h) = a
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.powerset, ∀ (a_1 : ι), a_1 ∈ {x ∈ s | ∃ (_ : x ∈ s), x ∈ a} ↔ a_1 ∈ a

Tactic:
mem_filter,

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ∈ s.powerset, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst✝⁴ : Semiring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
this : ⨆ i ∈ s, comap f.range.subtype (p i) = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]

Goal state after:
M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_8
R₂ : Type u_9
inst✝⁴ : Semiring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_10
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : f.range = ⨆ i ∈ s, p i
this : ⨆ i ∈ s, comap f.range.subtype (p i) = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⨆ i ∈ s, comap f.rangeRestrict (comap f.range.subtype (p i))
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : ComplementedLattice α
⊢ IsAtomistic α

Tactic:
exact isAtomistic_of_complementedLattice

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
⊢ a ∈ (onFinset s f hf).support ↔ f a ≠ 0

Tactic:
Finsupp.mem_support_iff,

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
⊢ (onFinset s f hf) a ≠ 0 ↔ f a ≠ 0
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : ∀ (i : α), ∃ y, e y = g i
⊢ ∃ y, mapRange e he₀ y = g

Tactic:
choose f h using h

Goal state after:
case mpr
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
⊢ ∃ y, mapRange e he₀ y = g
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j =
    (g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) * 1

pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ ∀ x ∈ insert a s, ¬a < x

Tactic:
mul_one

Goal state after:
case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j =
    g a * ∏ i ∈ s, f i + g a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j

case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ ∀ x ∈ insert a s, ¬a < x
Module: Mathlib.Algebra.Group.Finsupp

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

Tactic:
rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]

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

Goal state before:
pp: ι : Type u_1
G : Type u_6
inst✝¹ : AddGroup G
inst✝ : DecidableEq ι
f g : ι →₀ G
⊢ (f - g).support ⊆ f.support ∪ g.support

Tactic:
by
  rw [sub_eq_add_neg, ← support_neg g]
  exact support_add

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

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ s.indicator f a ≤ {a | 0 ≤ f a}.indicator f a

Tactic:
indicator_apply

Goal state after:
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ (if a ∈ s then f a else 0) ≤ if a ∈ {a | 0 ≤ f a} then f a else 0
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
hyf : y ∈ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
rw [Finsupp.prod, Finsupp.prod, ← Finset.mul_prod_erase _ _ hyf, Finsupp.support_erase,
      Finset.prod_congr rfl]

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ ∀ x ∈ f.support.erase y, g x ((erase y f) x) = g x (f x)
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : MulZeroOneClass R
s : Set α
r : R
a : α
⊢ s.indicator (fun x ↦ r * 1) a = s.indicator (fun x ↦ r) a

Tactic:
mul_one

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
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ ∏ x ∈ s.attach, h (↑x) ((indicator s f) ↑x) = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)

Tactic:
refine Finset.prod_congr rfl (fun _ _ => ?_)

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
x✝¹ : ↥s
x✝ : x✝¹ ∈ s.attach
⊢ h (↑x✝¹) ((indicator s f) ↑x✝¹) = h (↑x✝¹) (f ↑x✝¹ ⋯)
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: α : Type u_1
R : Type u_6
inst✝ : MulZeroOneClass R
a : α
b : R
⊢ single a (b * 1) = single a b

Tactic:
mul_one

Goal state after:
α : Type u_1
R : Type u_6
inst✝ : MulZeroOneClass R
a : α
b : R
⊢ single a b = single a b
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
⊢ ∏ i ∈ cons a✝ s✝ hj, b i • f i = (∏ i ∈ cons a✝ s✝ hj, b i) • ∏ i ∈ cons a✝ s✝ hj, f i

Tactic:
rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]

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

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

Tactic:
conv_rhs => rw [← sum_single m, map_finsuppSum, smul_sum]

Goal state after:
α : Type u_1
M✝ : Type u_2
N✝ : Type u_3
P : Type u_4
R✝ : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S✝ : Type u_8
inst✝¹⁷ : Semiring R✝
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring S✝
inst✝¹³ : AddCommMonoid M✝
inst✝¹² : Module R✝ M✝
inst✝¹¹ : AddCommMonoid N✝
inst✝¹⁰ : Module R₂ N✝
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R₃ P
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ f (r • m) = m.sum fun a b ↦ r • f (single a b)
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
s t : Set α
⊢ supported M R (s ∪ t) = supported M R s ⊔ supported M R t

Tactic:
Set.union_eq_iUnion,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (⋃ b, bif b then s else t) = supported M R s ⊔ supported M R t