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

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₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
x : M
⊢ p (Exists.choose ⋯) = f x

Tactic:
(h x).choose_spec

Goal state after:
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₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
x : M
⊢ f x = f x
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hg : g.ker = ⊥
⊢ (g ∘ₛₗ f).ker = f.ker

Tactic:
rw [ker_comp, hg, Submodule.comap_bot]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ center G₀ˣ ⊆ Units.val ⁻¹' center G₀

Tactic:
by
  simp_rw [subset_def, mem_preimage, _root_.Semigroup.mem_center_iff]
  intro u hu a
  obtain rfl | ha := eq_or_ne a 0
  · rw [zero_mul, mul_zero]
  · exact congr_arg Units.val <| hu <| Units.mk0 a ha

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

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
⊢ x * (x - (algebraMap R A) r) ^ (n + 1) = (x - (algebraMap R A) r) ^ (n + 1) * x

Tactic:
rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² x✝¹ : G
x✝ : R
⊢ (x✝² * x✝¹) • (algebraMap R A) x✝ = x✝² • x✝¹ • (algebraMap R A) x✝

Tactic:
mul_smul

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² x✝¹ : G
x✝ : R
⊢ x✝² • x✝¹ • (algebraMap R A) x✝ = x✝² • x✝¹ • (algebraMap R A) x✝
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:
simpa [mul_comm, pow_add, hx, hy, mul_assoc, mul_left_comm] using hz

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
⊢ e.symm (x • e 1) = x

Tactic:
rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
x✝ : { p' // p' ≤ p }
q : Submodule R M
hq : q ≤ p
⊢ ↑((fun p' ↦ ⟨map p.subtype p', ⋯⟩) ((fun q ↦ comap p.subtype ↑q) ⟨q, hq⟩)) = ↑⟨q, hq⟩

Tactic:
simp [map_comap_subtype p, inf_of_le_right hq]

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

Goal state before:
pp: case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ (g * g ^ n) • a

Tactic:
mul_smul

Goal state after:
case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ g • g ^ n • a
Module: Mathlib.Algebra.Order.Group.Action

Goal state before:
pp: case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ (g * g ^ n) • a ≤ a

Tactic:
mul_smul

Goal state after:
case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g • g ^ n • a ≤ a
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
⊢ (span R s).toAddSubmonoid = closure (univ • s)

Tactic:
refine le_antisymm (fun x (hx : x ∈ span R s) ↦ ?of_mem_span) (fun x hx ↦ ?of_mem_closure)
  case of_mem_span =>
    induction hx using span_induction with
    | mem x hx => exact subset_closure ⟨1, trivial, x, hx, one_smul R x⟩
    | zero => exact zero_mem _
    | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
    | smul r₁ y _h hy =>
      clear _h
      induction hy using closure_induction with
      | mem _ h =>
        obtain ⟨r₂, -, x, hx, rfl⟩ := h
        exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
      | zero => simp only [smul_zero, zero_mem]
      | add _ _ _ _ h₁ h₂ => simpa only [smul_add] using add_mem h₁ h₂
  case of_mem_closure =>
    refine closure_le.2 ?_ hx
    rintro - ⟨r, -, x, hx, rfl⟩
    exact smul_mem _ _ (subset_span hx)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a x : α
h : IsAtom a
⊢ x ≤ a ↔ x = ⊥ ∨ x = a

Tactic:
le_iff_lt_or_eq,

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a x : α
h : IsAtom a
⊢ x < a ∨ x = a ↔ x = ⊥ ∨ x = a
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b : α
ha : IsAtom a
⊢ ¬Disjoint a b ↔ a ≤ b

Tactic:
rw [disjoint_iff, ← inf_eq_left]; exact ha.ne_bot_iff_eq inf_le_left

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : Lattice α
s : Set α
⊢ ⇑ofDual ⁻¹' latticeClosure s = latticeClosure (⇑ofDual ⁻¹' s)

Tactic:
ext
  simp [latticeClosure, (Equiv.Set.congr toDual).surjective.forall, Equiv.image_eq_preimage_symm]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb : b ∈ s.biUnion g
hab : b ∉ a
⊢ Disjoint (f b) (a.sup f)

Tactic:
obtain ⟨i', hi', hb⟩ := mem_biUnion.mp hb

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
⊢ Disjoint (f b) (a.sup f)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: 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 x y
⊢ ∀ y ∈ span R s, Commute x y

Tactic:
by
  simp only [Commute.symm_iff (a := x)] at *
  exact .span_left h

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b ↦ f ⟨i, b⟩
⊢ (s.sigma g).SupIndep f

Tactic:
by
  classical
  rw [Finset.sigma_eq_biUnion]
  apply Finset.SupIndep.biUnion
  · simpa using! hs
  · simpa [Finset.supIndep_map] using! hg

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f g : ι → α
h₂ : iSup f = ⊤
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ j, ⨆ (_ : j ≠ i), f j) (g i)
⊢ f i = g i

Tactic:
replace h₂ : Codisjoint (f i) (⨆ (j) (_ : j ≠ i), f j) := by
    rw [codisjoint_iff, ← iSup_split_single f i, h₂]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f g : ι → α
h₃ : f ≤ g
i : ι
h₁ : Disjoint (⨆ j, ⨆ (_ : j ≠ i), f j) (g i)
h₂ : Codisjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ f i = g i
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr.smul
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✝ : M
a : R
x : M
hx : x ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
⊢ a • f ⟨x, hx⟩ = a • g ⟨x, hx⟩

Tactic:
hx'

Goal state after:
case mpr.smul
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✝ : M
a : R
x : M
hx : x ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
⊢ a • g ⟨x, hx⟩ = a • g ⟨x, hx⟩
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case e'_1.mp
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
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f = g → f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype

Tactic:
rintro rfl
    rfl

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R s ≤ span R (r • s)

Tactic:
convert! span_smul_le (r • s) ((hr.unit⁻¹ :) : R)
    simp [smul_smul]

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
⊢ Disjoint a (sSup (s \ {a}))

Tactic:
by
    rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot]
    intro t
    rw [iSup_eq_bot, Finset.sup_id_eq_sSup]
    intro ht
    classical
      have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot
      · rwa [Finset.coe_insert, Set.insert_sdiff_self_of_notMem] at h'
        exact fun con => ((Set.mem_sdiff a).1 (ht con)).2 (Set.mem_singleton a)
      · rw [Finset.coe_insert, Set.insert_subset_iff]
        exact ⟨ha, Set.Subset.trans ht sdiff_subset⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
⊢ (⨆ x, f ↑x) ⊓ a = ⊥

Tactic:
← sSup_range,

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
⊢ sSup (range fun x ↦ f ↑x) ⊓ a = ⊥
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: R : Type u_4
inst✝ : CommSemiring R
s✝ : Multiset (Multiset R)
a : Multiset R
s : Multiset (Multiset R)
ih : (map sum s).prod = (map prod s.Sections).sum
⊢ (map sum (a ::ₘ s)).prod = (map prod (a ::ₘ s).Sections).sum

Tactic:
by
    simp [ih, map_bind, sum_map_mul_left, sum_map_mul_right]

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Multiset ι
f g : ι → R
⊢ (map (fun i ↦ f i + g i) 0).prod = (map (fun p ↦ (map f p.1).prod * (map g p.2).prod) (antidiagonal 0)).sum

Tactic:
simp only [map_zero, prod_zero, antidiagonal_zero, map_singleton, mul_one, sum_singleton]

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

Goal state before:
pp: case h
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
a✝ : List R
h : ∀ (b : R), b ∈ ⟦a✝⟧ → Commute a b
⊢ Commute a (↑a✝).sum

Tactic:
sum_coe

Goal state after:
case h
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
a✝ : List R
h : ∀ (b : R), b ∈ ⟦a✝⟧ → Commute a b
⊢ Commute a a✝.sum
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

Tactic:
Set.mem_union,

Goal state after:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x ∈ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case refine_1
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
x✝ : α
⊢ Membership.mem ⟦l₁⟧ = Membership.mem ⟦l₂⟧

Tactic:
exact congrArg _ (Quotient.sound h)

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

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ IsAtom x ∧ x ≤ c

Tactic:
Set.mem_union,

Goal state after:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x ∈ {a}
⊢ IsAtom x ∧ x ≤ c
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: κ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
s : Finset κ
f : κ → R
n : ℕ
⊢ (∑ a ∈ s, f a) ^ n = ∑ p ∈ piFinset fun _i ↦ s, ∏ i, f (p i)

Tactic:
by
  convert! @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d; simp

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

Tactic:
by simp_rw [Finset.ext_iff, mem_filter, mem_powerset]; tauto

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

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s : Submodule K V
⊢ s ⩿ K ∙ x ⊔ s

Tactic:
refine ⟨le_sup_right, fun q hpq hqp ↦ hqp.not_ge ?_⟩
  rcases SetLike.exists_of_lt hpq with ⟨y, hyq, hyp⟩
  obtain ⟨c, z, hz, rfl⟩ : ∃ c : K, ∃ z ∈ s, c • x + z = y := by
    simpa [mem_sup, mem_span_singleton] using hqp.le hyq
  rcases eq_or_ne c 0 with rfl | hc
  · simp [hz] at hyp
  · have : x ∈ q := by
      rwa [q.add_mem_iff_left (hpq.le hz), q.smul_mem_iff hc] at hyq
    simp [hpq.le, this]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
⊢ equivFunOnFinite (single x m) = Pi.single x m

Tactic:
by
  simp [Finsupp.single_eq_pi_single, equivFunOnFinite]

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
M : Type u_4
inst✝³ : CommMonoidWithZero M
inst✝² : LinearOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

Tactic:
by
  classical
  rcases lt_or_ge (f i) 0 with hf | hf
  · exact (hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le
  have : f i = ∏ j ∈ s, if i = j then f i else 1 := by
    rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
    simp
  exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind

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

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

Tactic:
refine prod_nonneg fun r hr ↦ ?_
  obtain ⟨a, ha, rfl⟩ := mem_map.mp hr
  exact h a ha

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
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ v₁ a = v₂ a

Tactic:
by_cases h : a ∈ v₁.support ∪ v₂.support

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ v₁ a = v₂ a

case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∉ v₁.support ∪ v₂.support
⊢ v₁ a = v₂ a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : Zero M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ (filter (fun a ↦ p a.1) f).curry = filter p f.curry

Tactic:
by
  ext a b
  simp [filter_apply, apply_ite (DFunLike.coe · b)]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : CommMonoid N
inst✝¹ : MulDistribMulAction M N
ι : Sort u_4
inst✝ : Finite ι
f : ι → N
r : M
⊢ r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x

Tactic:
cases nonempty_fintype (PLift ι)
  simp only [finprod_eq_prod_plift_of_mulSupport_subset (s := Finset.univ) (by simp),
    Finset.smul_prod']

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : SemilatticeSup α
inst✝³ : OrderBot α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t : Finset ι
⊢ f (t.sup s) ≤ ∑ i ∈ t, f (s i)

Tactic:
refine t.induction_on zero.le fun i t it h ↦ ?_

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : SemilatticeSup α
inst✝³ : OrderBot α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t✝ : Finset ι
i : ι
t : Finset ι
it : i ∉ t
h : f (t.sup s) ≤ ∑ i ∈ t, f (s i)
⊢ f ((insert i t).sup s) ≤ ∑ i ∈ insert i t, f (s i)
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 α
h : Codisjoint s t
⊢ Codisjoint (supported M R s) (supported M R t)

Tactic:
rw [codisjoint_iff, eq_top_iff, ← supported_union,
    show s ∪ t = .univ from codisjoint_iff.mp h, supported_univ]

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

Goal state before:
pp: ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j, (b.repr (b' j)) i * (b'.repr x) j = (b.repr (∑ i, (b'.repr x) i • b' i)) i

Tactic:
simp_rw [map_sum, map_smul, Finset.sum_apply']

Goal state after:
ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j, (b.repr (b' j)) i * (b'.repr x) j = ∑ k, ((b'.repr x) k • b.repr (b' k)) i
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ image (castAdd m) (Ici i) = Ico (castAdd m i) (natAdd n 0)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ image (castAdd m) (Ioi i) = Ioo (castAdd m i) (natAdd n 0)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ map (castAddEmb m) (Ioi i) = Ioo (castAdd m i) (natAdd n 0)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Icc i j) = Icc (Fin.cast h i) (Fin.cast h j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Ico i j) = Ico (Fin.cast h i) (Fin.cast h j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Ioc i j) = Ioc (Fin.cast h i) (Fin.cast h j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (Ioo i j) = Ioo (Fin.cast h i) (Fin.cast h j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i j : Fin n
⊢ image (Fin.cast h) (uIcc i j) = uIcc (Fin.cast h i) (Fin.cast h j)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Ici i) = Ici (Fin.cast h i)

Tactic:
by
  simp [← coe_inj]

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

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ image (Fin.cast h) (Ioi i) = Ioi (Fin.cast h i)

Tactic:
by
  simp [← coe_inj]

Goal state after: