mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝¹ : Type u_1
α✝ : Type u_2
β✝ : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
⊢ ∀ {a b : Lex (Lex (α × β) × γ)},
    (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.prodAssoc α β γ).trans (((Equiv.refl α).prodCongr toLex).trans toLex))))
          a ≤
        (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.prodAssoc α β γ).trans (((Equiv.refl α).prodCongr toLex).trans toLex))))
          b ↔
      a ≤ b

Tactic:
simp only [Prod.Lex.le_iff, Prod.Lex.lt_iff, Equiv.trans_apply, Equiv.prodCongr_apply,
      Equiv.prodAssoc_apply]
    grind [EmbeddingLike.apply_eq_iff_eq, ofLex_toLex]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x

Tactic:
exact h.isLUB_Iio.csSup_eq ⟨⊥, hx⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
⊢ ⨆ a, succ ↑a ≤ x

Tactic:
rw [ciSup_le_iff' H]
    exact fun a ↦ succ_le_of_lt a.2

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

Goal state before:
pp: case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ ((i : ι) × Quotient.out #(f i) → ULift α) ≃ ((i : ι) → Quotient.out #(f i → α))

Tactic:
refine (Equiv.piCurry fun _ _ => ULift α).trans ?_

Goal state after:
case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ ((a : ι) → Quotient.out #(f a) → ULift α) ≃ ((i : ι) → Quotient.out #(f i → α))
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ici a ⊆ s

Tactic:
simp [IsUpperSet, subset_def, @forall_comm (_ ∈ s)]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
⊢ b ∈ Set.range ⇑(ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯)

Tactic:
obtain ⟨m, hm, hm'⟩ := H.wf.has_min { a | ¬s _ b } ⟨_, asymm h⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
⊢ b ∈ Set.range ⇑(ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯)
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
a : α
ha : a ∈ o
hb : b ∈ f a
⊢ b ∈ f (o.get h)

Tactic:
rwa [Part.get_eq_of_mem ha]

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
· rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
    · exact ⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩
    · rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩
      exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
x : α
c : Chain (Part α)
⊢ x ∈ ωSup c ↔ some x ∈ c

Tactic:
simp only [ωSup, Part.ωSup]

Goal state after:
α : Type u_2
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none) ↔ some x ∈ c
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc' : cSup c ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ f y ≤ cSup c

Tactic:
apply hc'.2.resolve_left

Goal state after:
case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc' : cSup c ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ ¬cSup c ≤ y
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case refine_2
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
⊢ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g' y

Tactic:
· intro x hx y hy hxy
      obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _] at hxy
      exact hy' ⟨x, hx, hxy⟩

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

Goal state before:
pp: c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
⊢ toNat c = toNat d

Tactic:
have h' := forall_congr' h
  rw [← Cardinal.aleph0_le, ← Cardinal.aleph0_le] at h'
  rcases iff_iff_and_or_not_and_not.mp h' with ⟨hc, hd⟩ | ⟨hc, hd⟩
  · simp [Cardinal.toNat_apply_of_aleph0_le, hc, hd]
  · apply eq_of_forall_le_iff
    rw [← cast_toNat_of_lt_aleph0 (not_le.mp hc), ← cast_toNat_of_lt_aleph0 (not_le.mp hd)] at h
    simpa using h

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * (algebraMap R A) r * y = (algebraMap R A) r * (x * y)

Tactic:
← commutes,

Goal state after:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ (algebraMap R A) r * x * y = (algebraMap R A) r * (x * y)
Module: Mathlib.Algebra.Module.LinearMap.Basic

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b x✝ : A
⊢ (mulRight R (a * b)) x✝ = (mulRight R b ∘ₗ mulRight R a) x✝

Tactic:
simp only [mulRight_apply, comp_apply, mul_assoc]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
⊢ Commute (f.restrict hf) (g.restrict hg)

Tactic:
change (f ∘ₗ g).restrict (hf.comp hg) = (g ∘ₗ f).restrict (hg.comp hf)

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
⊢ (f ∘ₗ g).restrict ⋯ = (g ∘ₗ f).restrict ⋯
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa only [closure_iUnion, closure_eq (S _)] using this

Goal state after:
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : (0, 1) = 0 ∨ (1, 0) = 0
⊢ False

Tactic:
Prod.mk_eq_zero,

Goal state after:
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : 0 = 0 ∧ 1 = 0 ∨ (1, 0) = 0
⊢ False
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mp.right
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ s.prod t
⊢ map (snd M N) u ≤ t

Tactic:
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * x - x * (algebraMap R A) r = (x - (algebraMap R A) r) * x

Tactic:
← commutes,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * x - (algebraMap R A) r * x = (x - (algebraMap R A) r) * x
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ ↑M ⊆ ↑M.subsemiringClosure.toNonUnitalSubsemiring

pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
· simp [Submonoid.subsemiringClosure_coe]

Goal state after:
case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M
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✝² : G
x✝¹ x✝ : R
⊢ x✝² • (x✝¹ * x✝) = x✝² • x✝¹ * x✝² • x✝

Tactic:
apply FaithfulSMul.algebraMap_injective R A
    rw [algebraMap.smul', map_mul, map_mul, algebraMap.smul', algebraMap.smul',
      MulSemiringAction.smul_mul]

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

Goal state before:
pp: R✝ : Type u_1
inst✝¹¹ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Algebra R✝ A✝
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module A✝ M
inst✝⁶ : Module R✝ M
inst✝⁵ : IsScalarTower R✝ A✝ M
R : Type u_4
S : Type u_5
A : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Algebra S A
r : R
s : S
a : A
⊢ (algebraMap R A) r * s • a = s • r • a

Tactic:
mul_smul_comm,

Goal state after:
R✝ : Type u_1
inst✝¹¹ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Algebra R✝ A✝
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module A✝ M
inst✝⁶ : Module R✝ M
inst✝⁵ : IsScalarTower R✝ A✝ M
R : Type u_4
S : Type u_5
A : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Algebra S A
r : R
s : S
a : A
⊢ s • ((algebraMap R A) r * a) = s • r • a
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: N : Type u_2
inst✝ : CommMonoid N
a u : N
hu : IsUnit u
⊢ u * a ~ᵤ a

Tactic:
rw [mul_comm]
  exact associated_mul_unit_left _ _ hu

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
⊢ a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
mul_comm a,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a b c d : M
⊢ b * a ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ map (-id) f.range = f.range

Tactic:
Submodule.map_neg,

Goal state after:
R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ map id f.range = f.range
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
x y : α
hy : c.IsClosed y
⊢ c x ≤ c y ↔ x ≤ c y

Tactic:
← le_closure_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
x y : α
hy : c.IsClosed y
⊢ x ≤ c y ↔ x ≤ c y
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (x ⊔ c y) = c (x ⊔ y)

Tactic:
closure_sup_closure_right

Goal state after:
α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (x ⊔ y) = c (x ⊔ y)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case smul
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
s : Set M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
t : Set N
p : (x : M) → (y : N) → x ∈ span R s → y ∈ span R t → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : y ∈ span R t), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : x ∈ span R s), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : x ∈ span R s) (hy : y ∈ span R s) (hz : z ∈ span R t),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : x ∈ span R s) (hy : y ∈ span R t) (hz : z ∈ span R t),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : a ∈ span R s
a✝ : R
x✝ : N
hx✝ : x✝ ∈ span R t
h : p a x✝ ha hx✝
⊢ p a (a✝ • x✝) ha ⋯

Tactic:
exact smul_right _ _ _ _ _ h

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 : Set (Submodule R M)
z : M
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

Tactic:
have : Nonempty s := hs.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed _ hdir.directed_val, SetCoe.exists,
    exists_prop]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s

Tactic:
have ha' : ∀ b ∈ s, a ≤ b := fun _ a ↦ ha a

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
ha' : ∀ b ∈ s, a ≤ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsCoatomistic αᵒᵈ
b : α
⊢ ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a

Tactic:
apply h.isGLB_coatoms

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsCoatomistic α
b : αᵒᵈ
⊢ ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a

Tactic:
apply h.isGLB_coatoms

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ c → ⊤ ≤ c

pp: case inr.inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊤ → ⊤ ≤ c → ⊤ ≤ c

Tactic:
· rcases eq_bot_or_eq_top c with (rfl | rfl) <;> simp

Goal state after:
case inr.inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊤ → ⊤ ≤ c → ⊤ ≤ c
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : Subsingleton ι
t : ι → α
i : ι
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Tactic:
simp [← Subsingleton.elim i]

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : Algebra R A
h : ∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
x : R
y : S
z : A
⊢ (x • y) • z = x • y • z

Tactic:
by simp_rw [Algebra.smul_def, map_mul, mul_assoc, h]

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 : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
a : α
x✝ : ¬a = ⊥ ∧ a ∈ s
ha : ¬a = ⊥
has : a ∈ s
⊢ ∃ a_1, (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a

Tactic:
obtain ⟨j, hj, rfl⟩ := hs has

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)
j : ι
hj : j ∈ {j | j ≠ i}
x✝ : ¬f j = ⊥ ∧ f j ∈ s
ha : ¬f j = ⊥
has : f j ∈ s
⊢ ∃ a, (¬a = i ∧ ¬f a = ⊥ ∧ f a ∈ s) ∧ f a = f j
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inr.refine_2
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun x ↦ x ∈ Iio k) a
c : ↑(Iic k)
hck : ⟨a, ⋯⟩ < c
c₀ : ¬c = ⊤
⊢ False

Tactic:
cases h.eq_of_le (y := c.1) (lt_of_le_of_ne c.2 fun con ↦ c₀ (Subtype.ext con)) hck.le

Goal state after:
case inr.refine_2.refl
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
c : ↑(Iic k)
c₀ : ¬c = ⊤
ba : b ≤ ↑c
h : Maximal (fun x ↦ x ∈ Iio k) ↑c
hck : ⟨↑c, ⋯⟩ < c
⊢ False
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ (a :: l).prod = 0

Tactic:
prod_cons

Goal state after:
M₀ : Type u_4
inst✝ : MonoidWithZero M₀
a : M₀
l : List M₀
h : 0 ∈ a :: l
⊢ a * l.prod = 0
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
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
⊢ ⊥.prod ⊥ = ⊥

Tactic:
by ext ⟨x, y⟩; simp

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₂
hf : Surjective ⇑f
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ i, p i
| map f (comap f (⨅ x, map f (p x)))

Tactic:
comap_iInf

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
ι : Sort u_8
p : ι → Submodule R M
h : f.ker ≤ ⨅ i, p i
| map f (⨅ i, comap f (map f (p i)))
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ (f ∘ ⇑g) a ≠ 0 → a ∈ g.support

Tactic:
mem_support_iff,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ (f ∘ ⇑g) a ≠ 0 → g a ≠ 0
Module: Mathlib.Data.Finsupp.Defs

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

Tactic:
classical
    choose f h using h
    use onFinset g.support (fun x ↦ if x ∈ g.support then f x else 0) (by simp_all)
    grind

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ motive (single a (f a) + erase a f)

Tactic:
apply single_add

Goal state after:
case a
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ a ∉ (erase a f).support

case a
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ f a ≠ 0

case a
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ motive (erase a f)
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j

Tactic:
indicator,

Goal state after:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (if (i, j) ∈ s ×ˢ t then 1 (i, j) else 0) = (if i ∈ s then 1 i else 0) * if j ∈ t then 1 j else 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_1
d : α →₀ ℕ
⊢ (∃ a, d = single a 1) → (d.sum fun x n ↦ n) = 1

Tactic:
rintro ⟨a, rfl⟩
    rw [sum_eq_single a ?_ (fun _ ↦ rfl), single_eq_same]
    exact fun _ _ hba ↦ single_eq_of_ne hba

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

Goal state before:
pp: case inl
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
map_inv_natCast_smul _ R S

Goal state after:
case inl
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ (↑n)⁻¹ • f x = (↑n)⁻¹ • f x
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ -f ((↑n)⁻¹ • x) = -((↑n)⁻¹ • f x)

Tactic:
map_inv_natCast_smul _ R S

Goal state after: