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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • b (y * z) = x • (b (z • 1) * b 1)
⊢ (algebraMap F E) (x * y) = b x

Tactic:
smul_eq_mul,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • b (y * z) = x • (b (z * 1) * b 1)
⊢ (algebraMap F E) (x * y) = b x
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • y • 1 = b (x • 1)
⊢ (algebraMap F E) (x * y) = b x

Tactic:
smul_eq_mul,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • y • 1 = b (x * 1)
⊢ (algebraMap F E) (x * y) = b x
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: case mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ algebraMapSubmonoid B M → x ∈ Submonoid.map f (algebraMapSubmonoid A M)

Tactic:
rintro ⟨r, hr, rfl⟩
    simp only [Submonoid.mem_map]
    use (algebraMap R A r)
    simp only [AlgHom.commutes, and_true]
    use r

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
⊢ p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)

Tactic:
by
    simpa [mul_comm, pow_add, hx, hy, mul_assoc, mul_left_comm] using hz

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
d : Mˣ
⊢ a * b ~ᵤ a * (b * ↑d)

Tactic:
exact ⟨d, mul_assoc _ _ _⟩

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

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

Tactic:
obtain ⟨u, rfl⟩ := h

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

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
apply h.of_pow_associated_of_prime' hp₁ hp₂ hk₁

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M),
      Associates.mk a ∣ Associates.mk a_1 * Associates.mk a_2 →
        ∃ a₁ a₂, a₁ ∣ Associates.mk a_1 ∧ a₂ ∣ Associates.mk a_2 ∧ Associates.mk a = a₁ * a₂) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
mk_surjective.exists,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M),
      Associates.mk a ∣ Associates.mk a_1 * Associates.mk a_2 →
        ∃ x x_1,
          Associates.mk x ∣ Associates.mk a_1 ∧
            Associates.mk x_1 ∣ Associates.mk a_2 ∧ Associates.mk a = Associates.mk x * Associates.mk x_1) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
⊢ s = 0 ∨ t = 0

Tactic:
by_contra! H

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : s ≠ 0 ∧ t ≠ 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inl
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]

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

Goal state before:
pp: R✝ : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹⁵ : CommSemiring R✝
inst✝¹⁴ : Semiring A₁
inst✝¹³ : Semiring A₂
inst✝¹² : Semiring A₃
inst✝¹¹ : Semiring A₁'
inst✝¹⁰ : Semiring A₂'
inst✝⁹ : Semiring A₃'
inst✝⁸ : Algebra R✝ A₁
inst✝⁷ : Algebra R✝ A₂
inst✝⁶ : Algebra R✝ A₃
inst✝⁵ : Algebra R✝ A₁'
inst✝⁴ : Algebra R✝ A₂'
inst✝³ : Algebra R✝ A₃'
e : A₁ ≃ₐ[R✝] A₂
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ↑(f * f⁻¹) x = x

Tactic:
rw [mul_inv_cancel]

Goal state after:
R✝ : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹⁵ : CommSemiring R✝
inst✝¹⁴ : Semiring A₁
inst✝¹³ : Semiring A₂
inst✝¹² : Semiring A₃
inst✝¹¹ : Semiring A₁'
inst✝¹⁰ : Semiring A₂'
inst✝⁹ : Semiring A₃'
inst✝⁸ : Algebra R✝ A₁
inst✝⁷ : Algebra R✝ A₂
inst✝⁶ : Algebra R✝ A₃
inst✝⁵ : Algebra R✝ A₁'
inst✝⁴ : Algebra R✝ A₂'
inst✝³ : Algebra R✝ A₃'
e : A₁ ≃ₐ[R✝] A₂
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ↑1 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 : R
⊢ x • 1 = x

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : R
⊢ x * 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 (e 1 * x)) = (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1 • 1)

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm (e 1 * x)) = (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1 * 1)
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) * e (e.symm (e 1 * x) • 1) = x

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm 1) * e (e.symm (e 1 * x) * 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
⊢ e (e.symm 1 • 1) * x = x

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ e (e.symm 1 * 1) * x = x
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
s : Set M
x : M
hx : x ∈ closure (univ • s)
⊢ x ∈ (span R s).toAddSubmonoid

Tactic:
refine closure_le.2 ?_ hx
    rintro - ⟨r, -, x, hx, rfl⟩
    exact smul_mem _ _ (subset_span hx)

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
s t : Set M
hst : Disjoint (span R s) (span R t)
h0s : 0 ∉ s
⊢ Disjoint s t

Tactic:
← sdiff_singleton_eq_self h0s

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set M
hst : Disjoint (span R s) (span R t)
h0s : 0 ∉ s
⊢ Disjoint (s \ {0}) t
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 y : M
h : x ∈ R ∙ y
a b : R
⊢ (a + b) • y = a • y + b • y

Tactic:
by simp [add_smul]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
y : ↑s
hy : ⟨c, hc⟩ < y
hy' : y < ⟨x, ⋯⟩
⊢ c < ?m.88 y hy hy'

Tactic:
by simpa using! hy

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
s : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
x : M
hx : x ∈ s
r : R
eq : f r = ⟨x, hx⟩
⊢ ↑(f (r • 1)) = x

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
x : M
hx : x ∈ s
r : R
eq : f r = ⟨x, hx⟩
⊢ ↑(f (r * 1)) = x
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
h : ¬(⨅ a, b ⊓ bif g a then a else aᶜ) = ⊥
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
⊢ c = ⊥

Tactic:
clear h

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
⊢ c = ⊥
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_3.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ↑(X ∪ Y) ⊆ S

pp: case refine_3.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ x + y ∈ span R ↑(X ∪ Y)

Tactic:
· rw [Finset.coe_union]
      exact Set.union_subset hX hY

Goal state after:
case refine_3.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ x + y ∈ span R ↑(X ∪ Y)
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x y : α
⊢ (if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = x ⊓ if y = ⊥ then ⊤ else ⊥

Tactic:
by
      rcases eq_bot_or_eq_top x with (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderTop α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyCoatomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]
  exact Lattice.isStronglyAtomic

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Tactic:
rw [isCompactElement_iff_le_of_directed_sSup_le] at hk
    let g : Finset ι → α := fun s => ⨆ i ∈ s, f i
    have h1 : DirectedOn (· ≤ ·) (Set.range g) := by
      rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩
      exact
        ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset Finset.subset_union_left,
          iSup_le_iSup_of_subset Finset.subset_union_right⟩
    have h2 : k ≤ sSup (Set.range g) :=
      h.trans
        (iSup_le fun i =>
          le_sSup_of_le ⟨{i}, rfl⟩
            (le_iSup_of_le i (le_iSup_of_le (Finset.mem_singleton_self i) le_rfl)))
    obtain ⟨-, ⟨s, rfl⟩, hs⟩ := hk (Set.range g) (Set.range_nonempty g) h1 h2
    exact ⟨s, hs⟩

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
⊢ s.mulIndicator f = f ↔ mulSupport f ⊆ s

Tactic:
simp only [funext_iff, subset_def, mem_mulSupport, mulIndicator_apply_eq_self, not_imp_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ sSup s ∈ s

Tactic:
clear h

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ sSup s ∈ s
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ (U.mulIndicator fun x ↦ a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
rw [mulIndicator_preimage, Pi.one_def, Set.preimage_const, preimage_const]
  split_ifs <;> simp [← compl_eq_univ_sdiff]

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

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

Tactic:
exact prod_congr rfl fun i hi => by simp [h i hi]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
⊢ Disjoint (f i) (sSup (f '' {j | j ≠ i}))

Tactic:
simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
hf : InjOn f {i | f i ≠ ⊥}
⊢ ∀ (i_1 : Finset α), ↑i_1 ⊆ f '' {j | j ≠ i} → Disjoint (f i) (i_1.sup id)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) (t.sup id)

Tactic:
← this,

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) ((Finset.image f ((insert i (t.preimage f hf)).erase i)).sup id)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ Disjoint (f i) (sSup (f '' {j | j ≠ i}))

Tactic:
simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ ∀ (i_1 : Finset α), ↑i_1 ⊆ f '' {j | j ≠ i} → Disjoint (f i) (i_1.sup id)
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: 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 α β
s : Finset ι
f : ι → F
x : α
⊢ (∏ i ∈ s, f i) x = ∏ i ∈ s, (f i) x

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s his h => simp [his, h]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f : α → M
a : α
ha : a ∈ s
⊢ sᶜ.mulIndicator f a * s.mulIndicator f a = f a

Tactic:
simp [ha]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f : α → M
a : α
ha : ¬a ∈ s
⊢ sᶜ.mulIndicator f a * s.mulIndicator f a = f a

Tactic:
simp [ha]

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
h : f.ker ≤ p
⊢ comap f (map f p) = p

Tactic:
by rw [Submodule.comap_map_eq, sup_of_le_left h]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f : α → M
a : α
ha : a ∈ s
⊢ s.mulIndicator f a * sᶜ.mulIndicator f a = f a

Tactic:
simp [ha]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f : α → M
a : α
ha : ¬a ∈ s
⊢ s.mulIndicator f a * sᶜ.mulIndicator f a = f a

Tactic:
simp [ha]

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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
this : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
← this,

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 τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
this : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = (⨆ i ∈ s, comap f (p i)) ⊔ f.ker
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Zero M
inst✝ : Unique α
f g : α →₀ M
h : f default = g default
a : α
⊢ f a = g a

Tactic:
rwa [Unique.eq_default a]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
e : R
⊢ (∀ (x : R), (x • e) • e = x • e) ↔ e * e = e

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
e : R
⊢ (∀ (x : R), x * e * e = x * e) ↔ e * e = e
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f (f 1 • 1) = f 1 ↔ IsIdempotentElem f

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f (f 1 * 1) = f 1 ↔ IsIdempotentElem f
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case pos
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : b ∈ Set.range ⇑f
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b

pp: case neg
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : b ∉ Set.range ⇑f
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b

Tactic:
· rcases h with ⟨a, rfl⟩
      simp

Goal state after:
case neg
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : b ∉ Set.range ⇑f
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
⊢ #f.support = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a)

Tactic:
by
  simp only [card_eq_one, support_eq_singleton]

Goal state after:
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:
smul_eq_mul,

Goal state after:
α : 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
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case pos
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : a = 0
⊢ abv (-a) = abv a

Tactic:
simp [ha]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
a✝ : i ∈ s
hi : i ∉ (indicator s f).support
⊢ single i ((indicator s f) i) = 0

Tactic:
rw [notMem_support_iff.mp hi, single_zero]

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
⊢ Injective (mapDomain f)

Tactic:
intro v₁ v₂ eq

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
f g : α →₀ M
⊢ subtypeDomain p f = subtypeDomain p g ↔ ∀ (x : α), p x → f x = g x

Tactic:
simp_rw [DFunLike.ext_iff, subtypeDomain_apply, Subtype.forall]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α →₀ γ
⊢ embDomain Embedding.inl a = a.sumElim 0

Tactic:
by
  ext (_ | _) <;> simp [embDomain_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β →₀ γ
⊢ embDomain Embedding.inr b = sumElim 0 b

Tactic:
by
  ext (_ | _) <;> simp [embDomain_apply]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
⊢ #s ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})

Tactic:
rw [← Finset.card_filter_add_card_filter_not fun i ↦ f i = ∅, add_comm]
  grw [card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
    nonempty_of_ne_empty (mem_filter.1 hi).2, filter_subset]

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

Goal state before:
pp: case pos
α : 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 : α
ha : P a
⊢ a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun a ↦ ¬P a) g.support) ⋯ ↔
    (if h : P a then f ⟨a, h⟩ else g ⟨a, h⟩) ≠ 0

Tactic:
simp [ha]

Goal state after: