mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
a : α
left✝ : a ∈ univ
hi : b a ∈ (image b univ).erase k
⊢ ∃ a_1 ∈ univ, b ↑a_1 = b a

Tactic:
exact ⟨⟨a, ne_of_mem_erase hi⟩, mem_univ _, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a✝ b a : α
s : Sym α n
⊢ (a ::ₘ ↑s).card = n.succ

Tactic:
by rw [Multiset.card_cons, s.2]

Goal state after:
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hmin : IsMin (sSup s)
⊢ sSup s ∈ s

Tactic:
have ⟨a, has⟩ := hne

Goal state after:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hmin : IsMin (sSup s)
a : α
has : a ∈ s
⊢ sSup s ∈ s
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a b : WithBot α
⊢ ((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) a ≤
      ((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) b ↔
    a ≤ b

Tactic:
simp only [Equiv.optionEquivSumPUnit, Option.elim, Equiv.trans_apply, Equiv.coe_fn_mk,
      Equiv.sumComm_apply, swap, Lex.toLex_le_toLex, le_refl]
    cases a <;> cases b
    · simp only [elim_inr, lex_inl_inl, bot_le]
    · simp only [elim_inr, elim_inl, Lex.sep, bot_le]
    · simp only [elim_inl, elim_inr, lex_inr_inl, false_iff]
      exact not_coe_le_bot _
    · simp only [elim_inl, lex_inr_inr, coe_le_coe]

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

Goal state before:
pp: case succ
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (⇑f)^[n + 1] (a₁ ⊔ a₂) ≤ (⇑f)^[n + 1] a₁ ⊔ a₂

Tactic:
calc
          f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (map f x).bind g = x.bind fun y ↦ g (f y)

Tactic:
← bind_some_eq_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (x.bind fun y ↦ some (f y)).bind g = x.bind fun y ↦ g (f y)
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ map g (x.bind f) = x.bind fun y ↦ map g (f y)

Tactic:
← bind_some_eq_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ ((x.bind f).bind fun y ↦ some (g y)) = x.bind fun y ↦ map g (f y)
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz'✝ : z ≤ y
hz' : z < y
⊢ f z ≤ f y

pp: case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz left✝ : z ∈ bot x f
hy : z ∈ {y | IsExtremePt x f y}
hzy : z < f z
hz' : z ≤ z
⊢ f z ≤ f z

Tactic:
· exact le_trans (hy.map_le_of_mem_of_lt hz hz') (le_map y)

Goal state after:
case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz left✝ : z ∈ bot x f
hy : z ∈ {y | IsExtremePt x f y}
hzy : z < f z
hz' : z ≤ z
⊢ f z ≤ f z
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
hy : y ∈ (c.map (f.partBind g)) i
⊢ y ∈ x

Tactic:
simp only [Part.mem_bind_iff, Chain.coe_map,
      Function.comp_apply, OrderHom.partBind_coe] at hy

Goal state after:
case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
hy : ∃ a ∈ f (c i), y ∈ g (c i) a
⊢ y ∈ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) ≤ ωSup (iterateChain (↑f) x h)

pp: case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
· apply ωSup_le
    intro n
    simp only [Chain.coe_map, OrderHomClass.coe_coe, comp_apply]
    have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
    rw [← this]
    apply le_ωSup

Goal state after:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
⊢ toNat #α = toNat #β

Tactic:
← toNat_lift,

Goal state after:
α : Type u
β : Type v
e : α ≃ β
⊢ toNat (lift.{?u.17, u} #α) = toNat #β
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ toNat a ≤ n ↔ a ≤ ↑n

Tactic:
nth_rw 1 [← Cardinal.toNat_natCast.{u} n,
    Cardinal.toNat_le_iff_le_of_lt_aleph0 lt (Cardinal.natCast_lt_aleph0)]

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

Goal state before:
pp: case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = lift.{u, v} (∏ i, f i)

Tactic:
rw [← e.prod_comp f, ← h]

Goal state after:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod fun i ↦ f (e i)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a • b)
⊢ IsSMulRegular M b

Tactic:
exact ab.of_smul _

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ #α = ↑n ↔ ∃ t, ↑t = univ ∧ t.card = n

Tactic:
rw [← mk_univ, mk_set_eq_nat_iff_finset]

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

Goal state before:
pp: α : Type u
⊢ 2 ≤ #α ↔ ∃ x y, x ≠ y

Tactic:
two_le_iff_one_lt,

Goal state after:
α : Type u
⊢ 1 < #α ↔ ∃ x y, x ≠ y
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R'
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁵ : Monoid S'
inst✝⁴ : DistribMulAction S' M
inst✝³ : SMulCommClass R S' M
inst✝² : Monoid T'
inst✝¹ : DistribMulAction T' M
inst✝ : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
c : R
x : M
⊢ (a • ⇑f) (c • x) = σ₁₂ c • (a • ⇑f) x

Tactic:
simp_rw [DomMulAct.smul_apply, ← smul_comm, f.map_smulₛₗ]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ (g₂ ∘ₗ g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)

Tactic:
LinearMap.comp_assoc,

Goal state after:
case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ g₂ ∘ₛₗ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ (f ∘ₛₗ g) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)

Tactic:
LinearMap.comp_assoc,

Goal state after:
case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ f ∘ₛₗ (g ∘ₗ g ^ k) = f ∘ₛₗ (g * g ^ k)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝ : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i

Tactic:
by
  change x ∈ ⋂ s ∈ Set.range p, s ↔ _
  simp

Goal state after:
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 : E
⊢ ∃ a, (algebraMap F E) a = x

Tactic:
obtain ⟨x, rfl⟩ := hb x

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 : F
⊢ ∃ a, (algebraMap F E) a = 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 : F
hy : b y = b 1 * b 1
⊢ ∃ a, (algebraMap F E) a = b x

Tactic:
refine ⟨x * y, ?_⟩

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 : F
hy : b y = b 1 * b 1
⊢ (algebraMap F E) (x * y) = b x
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
⊢ (List.map List.prod L).sum ∈ closure s

Tactic:
exact
      list_sum_mem fun r hr =>
        let ⟨t, ht1, ht2⟩ := List.mem_map.1 hr
        ht2 ▸ list_prod_mem _ fun y hy => subset_closure <| HL1 t ht1 y hy

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ ¬b ≤ a ∧ IsEmpty ↑(Ioo a (b ⊔ a)) → b ⊓ a < b ∧ IsEmpty ↑(Ioo (b ⊓ a) b)

Tactic:
inf_lt_left,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ ¬b ≤ a ∧ IsEmpty ↑(Ioo a (b ⊔ a)) → ¬b ≤ a ∧ IsEmpty ↑(Ioo (b ⊓ a) b)
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a ⊓ b < a ∧ IsEmpty ↑(Ioo (a ⊓ b) a) → ¬a ≤ b ∧ IsEmpty ↑(Ioo b (a ⊔ b))

Tactic:
inf_lt_left,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ ¬a ≤ b ∧ IsEmpty ↑(Ioo (a ⊓ b) a) → ¬a ≤ b ∧ IsEmpty ↑(Ioo b (a ⊔ b))
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (b ⊔ c) ≤ ⊥

Tactic:
← h.eq_bot,

Goal state after:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ span ℕ s ≤ AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s)

Tactic:
span_le

Goal state after:
M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ s ⊆ ↑(AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s))
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 (Set M)
⊢ span R (⋃₀ s) ≤ sSup (span R '' s)

Tactic:
span_le

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set M)
⊢ ⋃₀ s ⊆ ↑(sSup (span R '' s))
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
r : R
⊢ span R (r • s) ≤ span R s

Tactic:
span_le

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ r • s ⊆ ↑(span R s)
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬a ≤ f i
i : ι
x : α
hxa : x ≤ a
hxf : x ≤ f i
hx : ¬x = ⊥
⊢ ¬x = a

Tactic:
by rintro rfl; exact ha' _ hxf

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
⊢ IsCoatom (u b) ↔ IsCoatom b

Tactic:
by
  refine ⟨fun hb => gi.isCoatom_of_image hb, fun hb => ?_⟩
  obtain ⟨a, ha, hab⟩ :=
    (eq_top_or_exists_le_coatom (u b)).resolve_left fun h =>
      hb.1 <| (gi.gc.u_top ▸ gi.l_u_eq ⊤ : l ⊤ = ⊤) ▸ gi.l_u_eq b ▸ congr_arg l h
  have : l a = b :=
    (hb.le_iff.mp (gi.l_u_eq b ▸ gi.gc.monotone_l hab : b ≤ l a)).resolve_left fun hla =>
      ha.1 (gi.gc.u_top ▸ h_coatom a ha ▸ congr_arg u hla)
  exact this ▸ (h_coatom a ha).symm ▸ ha

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 g : M →ₛₗ[τ₁₂] M₂
⊢ f.eqLocus g = ⊤ ↔ f = g

Tactic:
simp [SetLike.ext_iff, DFunLike.ext_iff]

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

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
⊢ sSup s < k

Tactic:
rw [isCompactElement_iff_le_of_directed_sSup_le] at hk
  by_contra h
  have sSup' : sSup s ≤ k := sSup_le fun s hs => (hbelow s hs).le
  replace sSup : sSup s = k := eq_iff_le_not_lt.mpr ⟨sSup', h⟩
  obtain ⟨x, hxs, hkx⟩ := hk s hemp hdir sSup.symm.le
  obtain hxk := hbelow x hxs
  exact hxk.ne (hxk.le.antisymm hkx)

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
⊢ WellFoundedGT α

Tactic:
rw [wellFoundedGT_iff_monotone_chain_condition']

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
⊢ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

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

Tactic:
simp [Finset.prod_boole]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
rw [le_iff_compact_le_imp]
      intro c hc hcinf
      rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at hc
      rw [le_inf_iff] at hcinf
      rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩
      refine (le_inf hcinf.1 ht2).trans ?_
      exact le_iSup₂ (f := fun (t' : Finset α) (ht' : ↑t' ⊆ s) => a ⊓ t'.sup id) t ht1

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

Goal state before:
pp: case pos
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
hj : j ∈ ⋂ x ∈ s, f x
⊢ ∏ i ∈ s, (f i).indicator (g i) j = (∏ i ∈ s, g i) j

Tactic:
rw [Finset.prod_apply]
    congr! 1 with i hi
    simp only [Set.mem_iInter] at hj
    exact Set.indicator_of_mem (hj _ hi) _

Goal state after:
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
x : M
d : Set (Submodule R M)
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : R ∙ x ≤ sSup d
this : x ∈ sSup d
y : Submodule R M
hyd : y ∈ d
hxy : x ∈ y
⊢ R ∙ x ≤ y

Tactic:
by simpa only [span_le, singleton_subset_iff]

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

Goal state before:
pp: case pos
α : 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)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ∀ i_1 ∈ Finset.image (fun x ↦ x i) s, ({c ∈ s | c i = i_1}.sup fun k ↦ ⨅ i, f i (k i)) ≤ f i i_1

Tactic:
Finset.sup_le_iff,

Goal state after:
case pos
α : 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)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ ∀ i_1 ∈ Finset.image (fun x ↦ x i) s, ∀ b ∈ {c ∈ s | c i = i_1}, ⨅ i, f i (b i) ≤ f i i_1
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
⊢ (∃ y ∈ s, ∃ z, (z ∈ t ∧ z ∈ p) ∧ y + z = x) → (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p

Tactic:
· rintro ⟨y, hy, z, ⟨hz, hz'⟩, hyzx⟩
    refine ⟨⟨y, hy, z, hz, hyzx⟩, ?_⟩
    simpa [← hyzx] using p.add_mem (hsp hy) hz'

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

Tactic:
by_cases h : x ∈ s

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
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

case neg
α : 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
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g 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₂
hf : Surjective ⇑f
p : Submodule R₂ M₂
this : Injective (comap f)
x✝ : p ≠ ⊤
h : ∀ (b : Submodule R₂ M₂), p < b → b = ⊤
m : Submodule R M
hm : comap f p < m
⊢ m = comap f ⊤

Tactic:
rw [← h _ (lt_map_of_comap_lt_of_surjective hf hm),
    comap_map_eq_self ((comap_mono bot_le).trans hm.le)]

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, (fun a_1 x ↦ a_1 ∈ a) ∈ s.pi fun x ↦ {True, False}

Tactic:
by simp [Classical.em]

Goal state after:
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
a✝ : List α
hp₁ : {x | x ∈ ⟦a✝⟧ ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ ⟦a✝⟧ → (p₁ x ↔ p₂ x)
x : α
hx : x ∈ a✝
⊢ x ∈ ⟦a✝⟧

Tactic:
by simpa using hx

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✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ span R s ≤ f.eqLocus g ↔ Set.EqOn (⇑f) (⇑g) s

Tactic:
span_le

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ s ⊆ ↑(f.eqLocus g) ↔ Set.EqOn (⇑f) (⇑g) s
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : i ∈ (indicator s f).support
⊢ i ∈ s

Tactic:
rw [mem_support_iff] at hi

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : (indicator s f) i ≠ 0
⊢ i ∈ s
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
⊢ (indicator s f).support ⊆ s

Tactic:
intro i hi
  rw [mem_support_iff] at hi
  by_contra h
  exact hi (indicator_of_notMem h _)

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
⊢ (optionElim y f) none = 0 none

Tactic:
rw [c]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
⊢ (optionElim y f) (Option.some a) = 0 (Option.some a)

Tactic:
rw [c]

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
f : α →₀ M
y : α
g : α → M → N
hyf : y ∈ f.support
⊢ g y (f y) * ∏ a ∈ (erase y f).support, g a ((erase y f) a) = g y (f y) * ∏ x ∈ f.support.erase y, g x (f x)

Tactic:
Finsupp.support_erase,

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
⊢ g y (f y) * ∏ a ∈ f.support.erase y, g a ((erase y f) a) = g y (f y) * ∏ x ∈ f.support.erase y, g x (f x)
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
inst✝ : SemilatticeSup M
ι : Type u_3
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, (mulSupport (f i)).Finite
hs : s.Nonempty
a : α
ha : ∀ i ∈ s, f i a = 1
⊢ (s.sup' hs fun x ↦ f x a) = 1

Tactic:
exact Finset.sup'_eq_of_forall hs (fun x ↦ f x a) ha

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

Goal state before:
pp: case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support) →
        (∑ i ∈ insert a s, g i).support = (insert a s).biUnion fun i ↦ (g i).support

Tactic:
intro i s hi
    simp only [hi, sum_insert, not_false_iff, biUnion_insert]
    intro hs
    rw [Finsupp.support_add_eq, hs]
    rw [hs, Finset.disjoint_biUnion_right]
    intro j hj
    exact h _ _ (ne_of_mem_of_not_mem hj hi).symm

Goal state after: