mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
⊢ ∀ (a b : Cardinal.{u}), a ≤ b ∨ b ≤ a

Tactic:
rintro ⟨α⟩ ⟨β⟩
      apply Embedding.total

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

Goal state before:
pp: α : Type u
⊢ ∃ x, WellFoundedLT α

Tactic:
classical
  exact ⟨linearOrderOfSTO WellOrderingRel, ⟨WellOrderingRel.isWellOrder.wf⟩⟩

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
· rintro ⟨ha, hb⟩
    exact ⟨ha.mul hb, hb.mul ha⟩

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

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m + ↑n < ℵ₀

Tactic:
← Nat.cast_add

Goal state after:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m + n) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ Infinite α ↔ ℵ₀ ≤ #α

Tactic:
← not_lt,

Goal state after:
α : Type u
⊢ Infinite α ↔ ¬#α < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ #α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
  constructor
  · rintro ⟨t, ht, x, y, hne, rfl⟩
    exact ⟨x, y, hne, by simpa using ht⟩
  · rintro ⟨x, y, hne, h⟩
    exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ Function.RightInverse
    (fun _insts ↦
      have this := ⋯;
      prodOfSMulCommClass M N α)
    fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩

Tactic:
rintro ⟨hM, hN, -⟩
    dsimp only; congr 1
    · ext m a; (conv_rhs => rw [← hN.one_smul a]); rfl
    congr 1
    · funext; congr; ext m a; (conv_rhs => rw [← hN.one_smul a]); rfl
    · ext n a; (conv_rhs => rw [← hM.one_smul (SMul.smul n a)]); rfl
    · exact proof_irrel_heq ..

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic

Goal state before:
pp: M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : x ≠ y
⊢ mk.symm c₁ • a = mk.symm c₂ • a

Tactic:
contrapose! hne

Goal state after:
M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : mk.symm c₁ • a ≠ mk.symm c₂ • a
⊢ x = y
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f * g) 1 = MulOpposite.unop (MulOpposite.op (g 1)) * MulOpposite.unop (MulOpposite.op (f 1))

Tactic:
dsimp [← smul_eq_mul]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f • g) 1 = g 1 • f 1
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
x✝ : R
⊢ x✝ ∈ MulAction.stabilizerSubmonoid R m ↔ x✝ ∈ MulAction.stabilizerSubmonoid R ↑m

Tactic:
simp only [MulAction.mem_stabilizerSubmonoid_iff, ← SubMulAction.val_smul, SetLike.coe_eq_coe]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ ↑⟨p.toAddSubmonoid, ⋯⟩
this : p.toAddSubmonoid ≤ ⨆ q, ↑q
⊢ t • x ∈ ⨆ a, ↑a

Tactic:
by
            exact this (smul_mem p t hx)

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

Goal state before:
pp: R : Type u_1
R₂✝ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁✝ : Type u_6
M₂✝ : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst✝¹⁹ : Semiring R₁
inst✝¹⁸ : Semiring R₂
inst✝¹⁷ : Semiring R₁'
inst✝¹⁶ : Semiring R₂'
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₁'
inst✝¹² : AddCommMonoid M₂'
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : Module R₂ M₂
inst✝⁹ : Module R₁' M₁'
inst✝⁸ : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁵ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝⁴ : RingHomInvPair σ₂'₁' σ₁'₂'
inst✝³ : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst✝² : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst✝¹ : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst✝ : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₁ →ₛₗ[σ₁₁'] M₁'
⊢ (fun f ↦ (↑e₂.symm ∘ₛₗ f) ∘ₛₗ ↑e₁) ((fun f ↦ (↑e₂ ∘ₛₗ f) ∘ₛₗ ↑e₁.symm) f) = f

Tactic:
by
    ext x
    simp only [symm_apply_apply, Function.comp_apply, coe_comp, coe_coe]

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup s ≤ p

Tactic:
exact sSup_le fun q hq ↦ le_sSup <| Set.mem_image_of_mem toAddSubmonoid hq

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
⊢ f ⊥ = ⊥

Tactic:
by
      rw [← sSup_empty, map_sSup, Set.image_empty, sSup_empty]

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
s : Set α
⊢ id (sSup s) = sSup (id '' s)

Tactic:
by rw [id, Set.image_id]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
r : R
⊢ (↑↑(algebraMap S A)).toFun ((algebraMap R S) r) = (algebraMap R A) r

Tactic:
by simpa [Algebra.smul_def] using smul_assoc r (1 : S) (1 : A)

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
x : M
ha : Irreducible x
⊢ ¬IsSquare x

Tactic:
rw [isSquare_iff_exists_sq]
  rintro ⟨y, rfl⟩
  exact not_irreducible_pow (by decide) ha

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ a * (b * ↑(u * v)) = a * d

Tactic:
rw [← hv, mul_assoc c (v : M) d, mul_left_comm c, ← hu]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * ↑u = c * d
v : Mˣ
hv : c * ↑v = a
⊢ c * ↑v * (b * ↑(u * v)) = ↑v * (a * b * ↑u)
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
a : M
t : Finset M
hat : a ∉ t
IH : ↑t ⊆ ↑(span R s) → ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)
ht : ↑(insert a t) ⊆ ↑(span R s)
⊢ ↑t ⊆ ↑(span R s)

Tactic:
simp_all [Set.insert_subset_iff]

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.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ IsAtom ⊤ ↔ IsAtom ⊤

Tactic:
← f.isAtom_iff ⊤,

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ IsAtom (f ⊤) ↔ IsAtom ⊤
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι
x✝² : u ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ u
this : Disjoint ((image (fun x ↦ (i, x)) t).sup f) ((u ×ˢ t).sup f)
⊢ Disjoint ((fun i ↦ t.sup fun i' ↦ f (i, i')) i) (u.sup fun i ↦ t.sup fun i' ↦ f (i, i'))

Tactic:
simpa only [sup_image, sup_product_left]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : Set.EqOn ⇑f ⇑g ↑S
hT : Set.EqOn ⇑f ⇑g ↑T
⊢ Set.EqOn ⇑f ⇑g ↑(S ⊔ T)

Tactic:
rw [← LinearMap.coe_coe (f := f), ← LinearMap.coe_coe (f := g), ← le_eqLocus] at hS hT ⊢

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f g : F
S T : Submodule R M
hS : S ≤ (↑f).eqLocus ↑g
hT : T ≤ (↑f).eqLocus ↑g
⊢ S ⊔ T ≤ (↑f).eqLocus ↑g
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ (s ∩ mulSupport f).mulIndicator f = s.mulIndicator f

Tactic:
← mulIndicator_mulIndicator,

Goal state after:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ s.mulIndicator ((mulSupport f).mulIndicator f) = s.mulIndicator f
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ sSupIndep (⋃₀ s)

Tactic:
rw [Set.sUnion_eq_iUnion]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ sSupIndep (⋃ i, ↑i)
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_8
α : Type u_9
β : Type u_10
inst✝ : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
⊢ Set.EqOn (fun b ↦ ∏ i ∈ v, f i b) (fun b ↦ ∏ i ∈ v, f' i b) s

Tactic:
convert! eqOn_finsetProd h v <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
induction s using Finset.strongInduction with

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ Disjoint b (sSup (⋃₀ c))

Tactic:
sSup_sUnion,

Goal state after:
case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ Disjoint b (⨆ t ∈ c, sSup t)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2.refine_2
α : 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)
⊢ a ∈ s

Tactic:
s_max ⟨fun x hx => ?_, ?_, fun x hx => ?_⟩ Set.subset_union_left

Goal state after:
case refine_2.refine_2
α : 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)
⊢ a ∈ s ∪ ?m.338

α : 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)
⊢ Set α

α : 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)
⊢ Disjoint b (sSup (s ∪ ?m.338))

α : 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 ∪ ?m.338
⊢ Disjoint x (sSup ((s ∪ ?m.338) \ {x}))

α : 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 ∪ ?m.338
⊢ IsAtom x ∧ x ≤ c
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
N : Submodule R M
x : M
hx : x ∈ N
⊢ (R ∙ x).submoduleOf N = R ∙ ⟨x, hx⟩

Tactic:
ext y
  simp_rw [submoduleOf, mem_comap, subtype_apply, mem_span_singleton]
  aesop

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

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

Tactic:
rw [← update_eq_erase_add_single, update_self]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ (embDomain Embedding.some f).some = f

Tactic:
ext; rw [some_apply]; exact embDomain_apply_self _ _ _

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:
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.Ring.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ (∀ (a : α), a ∈ 0 → p a) → f (prod 0) ≤ (map f 0).prod

Tactic:
simp [h_one]

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_one : f 1 ≤ 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
hs : ∀ i ∈ ∅, p (g i)
⊢ f (∏ i ∈ ∅, g i) ≤ ∏ i ∈ ∅, f (g i)

Tactic:
simp [h_one]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ((subtypeDomain p v).prod fun a b ↦ h (↑a) b) = v.prod h

Tactic:
refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_ <;> aesop

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

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ l.support = l.splitSupport.sigma fun i ↦ (l.split i).support

Tactic:
by
  simp_rw [Finset.ext_iff, splitSupport, split, comapDomain, Sigma.forall, mem_sigma, mem_image,
    mem_preimage]
  tauto

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : ↑(single a 1).support ⊆ s
⊢ a ∈ s

Tactic:
Finsupp.support_single _ (one_ne_zero' R)

Goal state after:
α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : ↑{a} ⊆ s
⊢ a ∈ s
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
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))
i : δ
hi : x ∈ s i
⊢ single x a ∈ ⨆ i, supported M R (s i)

Tactic:
exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi)

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✝² : SMul R M
inst✝¹ : SMulZeroClass R N
inst✝ : CompatibleSMul M N R S
f : M →ₗ[S] ι →₀ N
r : R
m : M
⊢ f (r • m) = r • f m

Tactic:
ext i; apply ((lapply i).comp f).map_smul_of_tower

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (b.repr (b i)) j = if i = j then 1 else 0

Tactic:
b.repr_self_apply

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (if i = j then 1 else 0) = if i = j then 1 else 0
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) '' Ici i = Ici (i.addNat m)

Tactic:
by
  rw [← preimage_addNat_Ici_addNat, image_preimage_eq_of_subset]
  intro j hj
  have : (i : ℕ) + m ≤ j := hj
  refine ⟨⟨j - m, by lia⟩, ?_⟩
  simp (disch := lia)

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Iic a) = Iic ↑a

Tactic:
← attachFin_Iic,

Goal state after:
n : ℕ
a : Fin n
⊢ map valEmbedding ((Iic ↑a).attachFin ⋯) = Iic ↑a
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inr
n i : ℕ
hi : i ≥ n
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)

Tactic:
finSumNatEquiv_symm_apply_of_ge hi,

Goal state after:
case inr
n i : ℕ
hi : i ≥ n
⊢ (Sum.inr (i - n)).isLeft = decide (i < n)
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isRight = decide (n ≤ i)

Tactic:
← not_lt,

Goal state after:
n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isRight = decide ¬i < n
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (i : Option α) (_ : i ∈ range some), f i

Tactic:
finprod_mem_range

Goal state after:
case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (j : α), f (some j)

case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ Injective some
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) 0 = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) 0

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne (Fin.succ_ne_zero i).symm (Fin.succ_ne_zero j).symm]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
⊢ (Finsupp.linearCombination R v) (∑ i ∈ s, Finsupp.single i (f i)) =
    (Finsupp.linearCombination R v) (∑ i ∈ s, Finsupp.single i (g i))

Tactic:
by
          simpa only [map_sum, Finsupp.linearCombination_single] using eq

Goal state after: