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

Goal state before:
pp: case inl.inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : β
val✝ : γ
⊢ (Equiv.sumAssoc α β γ) (inl (inr val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inr val✝) ↔ inl (inr val✝¹) ≤ inr val✝

Tactic:
simp [Equiv.sumAssoc]

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : γ
val✝ : α
⊢ (Equiv.sumAssoc α β γ) (inr val✝¹) ≤ (Equiv.sumAssoc α β γ) (inl (inl val✝)) ↔ inr val✝¹ ≤ inl (inl val✝)

Tactic:
simp [Equiv.sumAssoc]

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : γ
val✝ : β
⊢ (Equiv.sumAssoc α β γ) (inr val✝¹) ≤ (Equiv.sumAssoc α β γ) (inl (inr val✝)) ↔ inr val✝¹ ≤ inl (inr val✝)

Tactic:
simp [Equiv.sumAssoc]

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ val✝ : γ
⊢ (Equiv.sumAssoc α β γ) (inr val✝¹) ≤ (Equiv.sumAssoc α β γ) (inr val✝) ↔ inr val✝¹ ≤ inr val✝

Tactic:
simp [Equiv.sumAssoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ ⇑e '' Ioi a = Ioi (e a)

Tactic:
← e.preimage_Ioi,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ ⇑e '' ⇑e ⁻¹' Ioi (e a) = Ioi (e a)
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ⇑(⨆ i, f i) = ⨆ i, ⇑(f i)

Tactic:
by
  funext x; simp [iSup_apply]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : IsLUB d (p₁, p₂)
⊢ IsLUB ((fun b ↦ b.1 ⊔ b.2) '' d) ((fun b ↦ b.1 ⊔ b.2) (p₁, p₂))

Tactic:
by
  simp only [IsLUB, IsLeast, upperBounds, Prod.forall, mem_ofPred_eq, Prod.mk_le_mk] at hdp
  simp only [IsLUB, IsLeast, upperBounds, mem_image, Prod.exists, forall_exists_index, and_imp]
  have e1 : (p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x} := hdp.2
  simp only [lowerBounds, mem_ofPred_eq, Prod.forall, Prod.mk_le_mk] at e1
  refine ⟨fun a b₁ b₂ hbd hba => ?_,fun b hb => ?_⟩
  · rw [← hba]
    exact sup_le_sup (hdp.1 _ _ hbd).1 (hdp.1 _ _ hbd).2
  · rw [sup_le_iff]
    exact e1 _ _ fun b₁ b₂ hb' => sup_le_iff.mp (hb b₁ b₂ hb' rfl)

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} = bot x f

Tactic:
← subset_bot_iff

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} ⊆ bot x f

α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ IsAdmissible x f {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inr
α : 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
y : α
hy : y ∈ c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
· 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.BourbakiWitt

Goal state before:
pp: case cSup_mem
α : 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
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
⊢ f y ≤ cSup c

Tactic:
have h : y ≤ z := by
      rw [← bot_eq_of_le_or_map_le le_map (hc hz)] at hy
      exact Or.resolve_right hy.2 hzy

Goal state after:
case cSup_mem
α : 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
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
h : y ≤ z
⊢ f y ≤ cSup c
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ {y | IsExtremePt x f y} = bot x f

Tactic:
← subset_bot_iff

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ {y | IsExtremePt x f y} ⊆ bot x f

α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsAdmissible x f {y | IsExtremePt x f y}
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : 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 : α
hx : x ∈ sᶜ
y : α
hy : y ∈ sᶜ
hxy : g' x = g' y
⊢ x ∈ g '' (f '' s)ᶜ

Tactic:
hns

Goal state after:
α : 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 : α
hx : x ∈ sᶜ
y : α
hy : y ∈ sᶜ
hxy : g' x = g' y
⊢ x ∈ sᶜ
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : 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
y : α
hy : y ∈ sᶜ
x' : β
left✝ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
⊢ y ∈ g '' (f '' s)ᶜ

Tactic:
hns

Goal state after:
α : 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
y : α
hy : y ∈ sᶜ
x' : β
left✝ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
⊢ y ∈ sᶜ
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ (f (c i)) (ωSup (c.map { toFun := g, monotone' := ⋯ })) ≤
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

Tactic:
rw [(f (c i)).continuous]

Goal state after:
case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ ωSup ((c.map { toFun := g, monotone' := ⋯ }).map ↑(f (c i))) ≤
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : 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 : α
hx : x ∈ s
y : α
hy : y ∉ s
hxy : f x = g' y
⊢ y ∈ g '' (f '' s)ᶜ

Tactic:
hns

Goal state after:
α : 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 : α
hx : x ∈ s
y : α
hy : y ∉ s
hxy : f x = g' y
⊢ y ∈ sᶜ
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
⊢ a < 2 ^ a

Tactic:
induction a using Cardinal.inductionOn with | _ α
   =>  _ 

Goal state after:
case mk
α : Type u
⊢ #α < 2 ^ #α
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
⊢ toENat c = 0 ∨ toENat c = ⊤ ↔ c = 0 ∨ ℵ₀ ≤ c

Tactic:
toENat_eq_zero,

Goal state after:
c : Cardinal.{u}
⊢ c = 0 ∨ toENat c = ⊤ ↔ c = 0 ∨ ℵ₀ ≤ c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ c ≠ 0

Tactic:
Cardinal.one_le_iff_pos,

Goal state after:
c : Cardinal.{u_1}
⊢ 0 < c ↔ c ≠ 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
A : Set (Set α)
⊢ #↑(⋃₀ A) ≤ #↑A * ⨆ s, #↑↑s

Tactic:
by
  rw [sUnion_eq_iUnion]
  apply mk_iUnion_le

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t} = lift.{v, u} #↑((fun x ↦ f ↑x) ⁻¹' t)

Tactic:
mk_sep

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ lift.{v, u} #↑{x | f ↑x ∈ t} = lift.{v, u} #↑((fun x ↦ f ↑x) ⁻¹' t)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑{x | x ∈ s ∧ f x ∈ t} = #↑((fun x ↦ f ↑x) ⁻¹' t)

Tactic:
mk_sep

Goal state after:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑{x | f ↑x ∈ t} = #↑((fun x ↦ f ↑x) ⁻¹' t)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
⊢ MulAction.orbitRel R ↥p = Setoid.comap Subtype.val (MulAction.orbitRel R M)

Tactic:
by
  refine Setoid.ext_iff.2 (fun x y ↦ ?_)
  rw [Setoid.comap_rel]
  exact mem_orbit_subMul_iff

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ x ∈ p, f x ∈ q
⊢ Injective ⇑(f.restrict hf) ↔ Disjoint p f.ker

Tactic:
simp [← ker_eq_bot, ker_restrict, disjoint_iff_comap_eq_bot]

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

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₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ False

Tactic:
refine h.2 ?_ (Submodule.comap_lt_of_lt_map_of_injective hf h₂)

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₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ p < comap f P
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f (a✝ * b✝) ∈ S

Tactic:
rw [map_mul]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f a✝ * f b✝ ∈ S
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ f (x * y) = f x * f y

Tactic:
rw [map_mul]

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
inst✝ : CharZero R
⊢ FaithfulSMul ℕ R

Tactic:
by
  simpa only [faithfulSMul_iff_algebraMap_injective] using (algebraMap ℕ R).injective_nat

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

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

Tactic:
by
  obtain ⟨u, rfl⟩ := h
  rw [← Units.eq_mul_inv_iff_mul_eq, zero_mul]

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

Goal state before:
pp: M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
x✝ : S
⊢ ((∀ (x : M₀), h.symm x✝ * x = 0 → x = 0) ∧ ∀ (x : M₀), x * h.symm x✝ = 0 → x = 0) ↔
    (∀ (x : S), x✝ * x = 0 → x = 0) ∧ ∀ (x : S), x * x✝ = 0 → x = 0

Tactic:
← h.symm.forall_congr_right,

Goal state after:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
x✝ : S
⊢ ((∀ (a : S), h.symm x✝ * h.symm.toEquiv a = 0 → h.symm.toEquiv a = 0) ∧
      ∀ (a : S), h.symm.toEquiv a * h.symm x✝ = 0 → h.symm.toEquiv a = 0) ↔
    (∀ (x : S), x✝ * x = 0 → x = 0) ∧ ∀ (x : S), x * x✝ = 0 → x = 0
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]
        simp [hv.symm, mul_comm, mul_left_comm]

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

Goal state before:
pp: case le
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
⊢ ∀ p ∈ {p | ∀ ⦃r_1 : S⦄ {n : M}, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ p}, (DistribSMul.toLinearMap R M r) m ∈ p

Tactic:
intro _ hp

Goal state after:
case le
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass S R M
r : S
m : M
hm : m ∈ ↑N
p✝ : Submodule R M
hp : p✝ ∈ {p | ∀ ⦃r_1 : S⦄ {n : M}, r_1 ∈ {r} → n ∈ N → r_1 • n ∈ p}
⊢ (DistribSMul.toLinearMap R M r) m ∈ p✝
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set M
hst : Disjoint (span R s) (span R t)
h0s : 0 ∉ s
⊢ Disjoint (s \ {0}) t

Tactic:
exact hst.of_span

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
⊢ SupClosed ∅

Tactic:
simp [SupClosed]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
a : α
⊢ SupClosed {a}

Tactic:
simp [SupClosed]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
⊢ SupClosed univ

Tactic:
simp [SupClosed]

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
hs : SupClosed s
ha : a ∈ upperBounds s
⊢ SupClosed (insert a s)

Tactic:
rw [SupClosed]
  aesop

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ t.sup' ht id ⊔ u.sup' hu id ∈ {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ s ∧ t.sup' ht id = a}

Tactic:
refine ⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩

Goal state after:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ↑(t ∪ u) ⊆ s
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝¹ : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α✝¹
α✝ : Type u_4
a✝ b : α✝
inst✝³ : Preorder α✝
α : Type u_5
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsStronglyAtomic α
a : α
hlt : ⊥ < a
x : α
hx : ⊥ ⋖ x
hxa : x ≤ a
⊢ ∃ a_1, IsAtom a_1 ∧ a_1 ≤ a

Tactic:
exact ⟨x, bot_covBy_iff.1 hx, hxa⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝³ : PartialOrder α✝
α : Type u_4
a b : α
inst✝² : Preorder α
inst✝¹ : IsStronglyAtomic α
s : Set α
inst✝ : s.OrdConnected
⊢ s.OrdConnected

Tactic:
by assumption

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : IsStronglyCoatomic α
s : Set α
h : s.OrdConnected
⊢ s.OrdConnected

Tactic:
by assumption

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : IsAtomistic α
inst✝ : OrderTop α
⊢ IsLUB {a | IsAtom a} ⊤

Tactic:
simpa using isLUB_atoms_le (⊤ : α)

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
ι : Sort u_9
p : ι → Submodule R M
h : ι → Prop
⊢ ⨆ i, ⨆ (_ : h i), p i = span R (⋃ i, ⋃ (_ : h i), ↑(p i))

Tactic:
← Submodule.iSup_span,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
h : ι → Prop
⊢ ⨆ i, ⨆ (_ : h i), p i = ⨆ i, ⨆ (_ : h i), span R ↑(p i)
Module: Mathlib.Order.Atoms

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

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

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

Goal state before:
pp: case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
a : R
x : M
T : Finset M
hT : ↑T ⊆ S
h2 : x ∈ span R ↑T
⊢ ∃ T, ↑T ⊆ S ∧ a • x ∈ span R ↑T

Tactic:
exact ⟨T, hT, smul_mem _ _ h2⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case right.mem
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ f '' s, a ∈ f '' latticeClosure s

Tactic:
exact Set.image_mono subset_latticeClosure

Goal state after:
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Iio b ↔ x ∈ Iio (e.symm b)

Tactic:
simp [← e.lt_iff_lt]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ i, s i
⊢ sSupIndep ↑t

Tactic:
obtain ⟨I, fi, hI⟩ := Set.finite_subset_iUnion t.finite_toSet ht

Goal state after:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
η : Type u_3
s : η → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), sSupIndep (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ i, s i
I : Set η
fi : I.Finite
hI : ↑t ⊆ ⋃ i ∈ I, s i
⊢ sSupIndep ↑t
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case neg
ι : 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 = 0

Tactic:
obtain ⟨i, hi, hj⟩ := by simpa using hj
    exact Finset.prod_eq_zero hi <| Set.indicator_of_notMem hj _

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 τ₁₂
p p' : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
hab : p ≤ p'
h : p ⊔ f.ker < p' ⊔ f.ker
⊢ map f p < map f p'

Tactic:
by
  simp_rw [← comap_map_eq] at h
  exact lt_of_le_of_ne (map_mono hab) (ne_of_apply_ne _ h.ne)

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

Goal state before:
pp: α : Type u_1
p₁ p₂ : α → Bool
l : List α
h : ∀ (x : α), x ∈ l → p₁ x = p₂ x
⊢ find? p₁ l = find? p₂ l

Tactic:
induction l with grind

Goal state after: