mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s t : ↥S
⊢ (1 /ₒ t) • (r /ₒ s) = r /ₒ (s * t)

Tactic:
simp [oreDiv_smul_char 1 r t s 1 s (by simp)]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₂ : α
h₂ : r ≤ v₂
n : ℕ
h₁ : r ≤ succ^[n] r
⊢ succ^[n] r ≤ v₂ ∨ v₂ ≤ succ^[n] r

Tactic:
obtain ⟨m, rfl⟩ := h₂.exists_succ_iterate

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n : ℕ
h₁ : r ≤ succ^[n] r
m : ℕ
h₂ : r ≤ succ^[m] r
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
h : IsSuccPrelimit a
b : α
⊢ succ b ≠ a

Tactic:
by
  rintro rfl
  exact not_isMax _ h.isMax

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y
⊢ x + 1 ≤ y

Tactic:
rw [← succ_eq_add_one]
  exact succ_le_of_lt h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf (Ioi a) = sInf {x | x > a}

Tactic:
Ioi

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf {x | a < x} = sInf {x | x > a}
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f a ≤ f (a - 1)) → Antitone f

Tactic:
by
  simpa [Order.pred_eq_sub_one] using antitone_of_le_pred (f := f)

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ StrictMono f

Tactic:
by
  simpa using strictMonoOn_of_lt_succ Set.ordConnected_univ (by simpa using hf)

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : ⟨b, hb⟩ < ⟨c, hc⟩
⊢ ⟨b, hb⟩ ≤ if h : pred ↑⟨c, hc⟩ ∈ s then ⟨pred ↑⟨c, hc⟩, h⟩ else ⟨c, hc⟩

Tactic:
by
    rw [Subtype.mk_lt_mk] at h
    dsimp only
    split
    · exact h.le_pred
    · exact h.le

Goal state after:
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
⊢ s.piecewise f f = f

Tactic:
ext i
  by_cases h : i ∈ s <;> simp [h]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
x : γ
y : α
⊢ ((x, y) ∈ s.biUnion fun x ↦ map (Embedding.sectR x α) (t x)) ↔ (x, y).1 ∈ s ∧ (x, y).2 ∈ t (x, y).1

Tactic:
simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
        exists_eq_right, ← and_assoc]

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (ofFn f).toList = List.ofFn f

Tactic:
by rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]

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

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map (fun x ↦ x) s) = ↑s

Tactic:
simp only [map, Multiset.map_id', ← val_eq_coe]

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
rcases have : v₂ < succ v := lt_succ_of_le h
      denumerable_list_aux v₂ with
      ⟨a, h₁, h₂⟩

Goal state after:
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : a ∈ decodeList v₂
h₂ : encodeList a = v₂
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
⊢ sInf s ∈ s

Tactic:
obtain ⟨y, hy⟩ := not_forall_not.mp hlim
  obtain ⟨i, his, hi⟩ := sInf_lt_iff.mp hy.lt
  exact eq_of_le_of_not_lt (sInf_le his) (hy.2 · hi) ▸ his

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Part α), none ≤ a

Tactic:
rintro x _ ⟨⟨_⟩, _⟩

Goal state after:
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 j : ℕ
⊢ ((c.map { toFun := g, monotone' := ⋯ }).map ↑(f (c i))) j ≤
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

Tactic:
apply le_ωSup_of_le (i ⊔ j)

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 j : ℕ
⊢ ((c.map { toFun := g, monotone' := ⋯ }).map ↑(f (c i))) j ≤
    (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ }) (max i j)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
b : Cardinal.{v}
⊢ lift.{w, max v u} (lift.{v, u} a) = lift.{w, max u v} (lift.{u, v} b) ↔ lift.{v, u} a = lift.{u, v} b

Tactic:
lift_inj

Goal state after:
a : Cardinal.{u}
b : Cardinal.{v}
⊢ lift.{v, u} a = lift.{u, v} b ↔ lift.{v, u} a = lift.{u, v} b
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: n : ℕ
a : Cardinal.{u}
⊢ lift.{v, u} ↑n = lift.{v, u} a ↔ ↑n = a

Tactic:
lift_inj

Goal state after:
n : ℕ
a : Cardinal.{u}
⊢ ↑n = a ↔ ↑n = a
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x = lift.{u, v} ↑m ↔ x = ↑m

Tactic:
lift_inj

Goal state after:
x : Cardinal.{v}
m : ℕ∞
⊢ x = ↑m ↔ x = ↑m
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} ↑m = lift.{u, v} x ↔ ↑m = x

Tactic:
lift_inj

Goal state after:
x : Cardinal.{v}
m : ℕ∞
⊢ ↑m = x ↔ ↑m = x
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case refine_1
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 * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b

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 ⟨ab, ba⟩
    exact ⟨ba.of_mul, ab.of_mul⟩

Goal state after:
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)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : AddGroup M
inst✝ : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ r • m₁ - r • m₂ = 0

Tactic:
eq,

Goal state after:
R : Type u_1
M : Type u_3
inst✝¹ : AddGroup M
inst✝ : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ r • m₂ - r • m₂ = 0
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
rw [Cardinal.one_le_iff_pos, pos_iff_ne_zero]

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

Goal state before:
pp: α : Type u
s : Set α
a : α
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
by_cases h : a ∈ s
  · simp only [insert_eq_of_mem h, self_le_add_right]
  · rw [mk_insert h]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝² : SetLike S M
inst✝¹ : SMul R M
inst✝ : SMulMemClass S R M
r : R
s : S
⊢ r • ↑s ⊆ ↑s

Tactic:
rintro _ ⟨x, hx, rfl⟩
  simpa using SMulMemClass.smul_mem (r : R) hx

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' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
h' : ∀ x ∈ p, (f' ^ n) x ∈ p
⊢ f'.restrict h ^ n = (f' ^ n).restrict h'

Tactic:
ext x
  have : Semiconj (↑) (f'.restrict h) f' := fun _ ↦ coe_restrict_apply _ _
  simp [Module.End.coe_pow, this.iterate_right _ _]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S

Tactic:
have : S i ≤ iSup S := le_iSup _ _

Goal state after:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
this : S i ≤ iSup S
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S
Module: Mathlib.Algebra.Ring.Submonoid.Basic

Goal state before:
pp: case add
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
r s : R
hx✝ : r ∈ closure ↑S
hy✝ : s ∈ closure ↑S
hr : a * r ∈ closure ↑S
hs : a * s ∈ closure ↑S
⊢ a * (r + s) ∈ closure ↑S

Tactic:
simpa only [mul_add] using add_mem hr hs

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: case mul
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ * y✝) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ _ h₁ h₂

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ * y✝) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ _ h₁ h₂

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

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

Tactic:
by
    apply FaithfulSMul.algebraMap_injective R A
    rw [algebraMap.smul', algebraMap.smul', algebraMap.smul', mul_smul]

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

Goal state before:
pp: case mul
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ * y✝) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ _ h₁ h₂

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

Goal state before:
pp: case mul
R : Type u
inst✝ : NonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ * y✝) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ _ h₁ h₂

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
hp : DvdNotUnit p q
⊢ ¬IsUnit q

Tactic:
by
  obtain ⟨-, x, hx, rfl⟩ := hp
  exact fun hc => hx (isUnit_iff_dvd_one.mpr (dvd_of_mul_left_dvd (isUnit_iff_dvd_one.mp hc)))

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
n : ℕ
hp : Prime (p ^ n)
⊢ Prime p ∧ n = 1

Tactic:
suffices n = 1 by simp_all

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
n : ℕ
hp : Prime (p ^ n)
⊢ n = 1
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ M₀⁰ ∧ b ∈ M₀⁰

Tactic:
rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]
    constructor <;> intro x h' <;> apply h.2
    · rw [← mul_assoc, h', zero_mul]
    · rw [mul_comm a b, ← mul_assoc, h', zero_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ 0 * Associates.mk a = 0

Tactic:
← mk_zero,

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk 0 * Associates.mk a = Associates.mk 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk a * 0 = 0

Tactic:
← mk_zero,

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Associates.mk a * Associates.mk 0 = Associates.mk 0
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ s ⊔ closure (⇑f ⁻¹' {0}) ≤ comap f (map f s)

Tactic:
rw [← map_le_iff_le_comap, map_sup, f.map_closure]
    apply le_of_eq
    rw [sup_eq_left, closure_le]
    exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (s.map f).zero_mem)

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

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
hz : f z = 0
x : M
hx : f x = y
hx' : x ∈ p
hxz : z + x ∈ p
⊢ z + x - x ∈ p

Tactic:
exact p.sub_mem hxz hx'

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁸ : CommSemiring 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₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
x : M₁
y : M₂
⊢ i (((f.codRestrict₂ i hi hf) x) y) = (f x) y

Tactic:
simp [codRestrict₂]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo (a ⊓ b) a)
⊢ ↑((fun c ↦ ⟨a ⊓ ↑c, ⋯⟩) ((fun c ↦ ⟨↑c ⊔ b, ⋯⟩) c)) = ↑c

Tactic:
dsimp
      rw [sup_comm, ← inf_sup_assoc_of_le _ c.prop.2.le, sup_eq_right.2 c.prop.1.le]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ a ⊓ b ⋖ a → b ⋖ a ⊔ b

Tactic:
simp_rw [covBy_iff_Ioo_eq, ← isEmpty_coe_sort, right_lt_sup, inf_lt_left,
      (infIooOrderIsoIooSup a b).toEquiv.isEmpty_congr]

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ ¬a ≤ b ∧ IsEmpty ↑(Ioo b (a ⊔ b)) → ¬a ≤ b ∧ IsEmpty ↑(Ioo b (a ⊔ b))
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]

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

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

Tactic:
rw [SupClosed]

Goal state after:
α : 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
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case sup
α : 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 ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s

Tactic:
rintro _ - _ - ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩

Goal state after:
case sup
α : 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 : α
ha : a ∈ latticeClosure s
b : α
hb : b ∈ latticeClosure s
⊢ f a ⊔ f b ∈ f '' latticeClosure s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case right.inf
α : 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 ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s

Tactic:
rintro _ - _ - ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩

Goal state after:
case right.inf
α : 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 : α
ha : a ∈ latticeClosure s
b : α
hb : b ∈ latticeClosure s
⊢ f a ⊓ f b ∈ f '' latticeClosure s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
s t : Set α
hs : SupClosed s
ht : t.Finite
hbot : ⊥ ∈ s
hts : t ⊆ s
⊢ sSup t ∈ s

Tactic:
by
  have := ht.to_subtype
  rw [sSup_eq_iSup']
  exact hs.iSup_mem hbot (by simpa)

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case hg
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')
ht : t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')
⊢ ∀ i' ∈ s, (image (fun b ↦ (i', b)) t).SupIndep f

Tactic:
· exact fun i' hi' ↦ (ht.mono fun i hi ↦ Finset.le_sup (f := fun i' ↦ f (i', i)) hi').image

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
this : ∀ (s : Finset ι), Disjoint (↑s) t → Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
⊢ Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
specialize this hs.toFinset

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
this : Disjoint (↑hs.toFinset) t → Disjoint (⨆ i ∈ hs.toFinset, f i) (⨆ i ∈ t, f i)
⊢ Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ sSup s = t.sup id

Tactic:
by apply le_antisymm <;> assumption

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
r : M
s : Set α
f : α → M
⊢ r ∈ range (s.mulIndicator f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s

Tactic:
simp [mulIndicator, ite_eq_iff, exists_or, eq_univ_iff_forall, and_comm, or_comm,
    @eq_comm _ r 1]

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
α : ι → Type u_5
inst✝ : CommMonoidWithZero M₀
s : Finset ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ ((↑s).pi t).indicator 1 f = ∏ i ∈ s, (t i).indicator 1 (f i)

Tactic:
simp [Set.indicator, prod_boole]

Goal state after: