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

Goal state before:
pp: α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ assert p f = none

Tactic:
by
  ext
  simp_all

Goal state after:
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, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
rcases isEmpty_or_nonempty β with hβ | hβ

Goal state after:
case inl
α : 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β : IsEmpty β
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)

case inr
α : 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 β
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ∀ f_1 ∈ {f, g}, ωScottContinuous f_1

Tactic:
rintro f (rfl | rfl | _)

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
g : α → β
hg : ωScottContinuous g
f : α → β
hf : ωScottContinuous f
⊢ ωScottContinuous f

case inr
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous g
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case refine_1
α : 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
⊢ InjOn g' sᶜ

Tactic:
intro x hx y hy hxy

Goal state after:
case refine_1
α : 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 = 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

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

Goal state before:
pp: a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (?u.14 + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
⊢ False

Tactic:
let f : ι → Cardinal := Subtype.val

Goal state after:
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (?u.14 + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
f : ι → Cardinal.{?u.14} := Subtype.val
⊢ False
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))

Tactic:
rwa [← mk_out (f i), ← mk_out (g i)] at this

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ ¬IsSMulRegular M 0 ↔ Nontrivial M

Tactic:
rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]
  push Not
  exact Iff.rfl

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ Function.Injective fun a ↦ n • a

Tactic:
← Nat.cast_smul_eq_nsmul R

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsTorsionFree R M
inst✝¹ : IsCancelMulZero R
inst✝ : CharZero R
n : ℕ
hn : n ≠ 0
⊢ Function.Injective fun a ↦ ↑n • a
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: case mk
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
q : Submodule R M
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h : (fun s ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ } = (fun s ↦ s.carrier) q
⊢ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ } = q

Tactic:
cases q

Goal state after:
case mk.mk
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
toAddSubmonoid✝¹ : AddSubmonoid M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    (fun s ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
⊢ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: case mk
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
q : SubMulAction R M
carrier✝ : Set M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ carrier✝ → c • x ∈ carrier✝
h : { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, smul_mem' := smul_mem'✝ } = q

Tactic:
cases q

Goal state after:
case mk.mk
S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
carrier✝¹ : Set M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ carrier✝¹ → c • x ∈ carrier✝¹
carrier✝ : Set M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ carrier✝ → c • x ∈ carrier✝
h :
  { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ }.carrier = { carrier := carrier✝, smul_mem' := smul_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, smul_mem' := smul_mem'✝¹ } = { carrier := carrier✝, smul_mem' := smul_mem'✝ }
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ Disjoint p q ↔ comap p.subtype q = ⊥

Tactic:
rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff,
    map_comap_subtype, map_bot, disjoint_iff]

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

Goal state before:
pp: case mk
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
q : Subsemiring R
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ } =
    (fun s ↦ s.carrier) q
⊢ { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ } = q

Tactic:
cases q

Goal state after:
case mk.mk
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
toSubmonoid✝¹ : Submonoid R
add_mem'✝¹ : ∀ {a b : R}, a ∈ toSubmonoid✝¹.carrier → b ∈ toSubmonoid✝¹.carrier → a + b ∈ toSubmonoid✝¹.carrier
zero_mem'✝¹ : 0 ∈ toSubmonoid✝¹.carrier
toSubmonoid✝ : Submonoid R
add_mem'✝ : ∀ {a b : R}, a ∈ toSubmonoid✝.carrier → b ∈ toSubmonoid✝.carrier → a + b ∈ toSubmonoid✝.carrier
zero_mem'✝ : 0 ∈ toSubmonoid✝.carrier
h :
  (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
⊢ { toSubmonoid := toSubmonoid✝¹, add_mem' := add_mem'✝¹, zero_mem' := zero_mem'✝¹ } =
    { toSubmonoid := toSubmonoid✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }
Module: Mathlib.RingTheory.NonUnitalSubring.Defs

Goal state before:
pp: case mk
R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
q : NonUnitalSubring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } =
    (fun s ↦ s.carrier) q
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ } = q

Tactic:
cases q

Goal state after:
case mk.mk
R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
neg_mem'✝¹ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝¹.carrier → -x ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    (fun s ↦ s.carrier) { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, neg_mem' := neg_mem'✝¹ } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
by
  have : s ≤ sSup S := le_sSup hs
  tauto

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_5
inst✝ : Mul N
f : M →ₙ* N
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_top

Goal state after:
M : Type u_1
inst✝¹ : Mul M
N : Type u_5
inst✝ : Mul N
f : M →ₙ* N
⊢ Set.range ⇑f = Set.univ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_top

Goal state after:
R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Set.range ⇑f = Set.univ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_top

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ Set.range ⇑f = Set.univ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mp.mem.mem
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x : R
hx : x ∈ s
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x

Tactic:
exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_top

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
⊢ Set.range ⇑f = Set.univ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_top

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
⊢ Set.range ⇑f = Set.univ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
n : ℕ
h : a ~ᵤ b
⊢ a ^ n ~ᵤ b ^ n

Tactic:
induction n with
  | zero => simp [Associated.refl]
  | succ n ih => convert! h.mul_mul ih <;> rw [pow_succ']

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ y ∣ x → IsUnit y ∨ x ~ᵤ y

Tactic:
rintro ⟨z, hz⟩

Goal state after:
case mp
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
⊢ IsUnit y ∨ x ~ᵤ y
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ x ~ᵤ y

Tactic:
· rw [hz]
      exact Or.inr (associated_mul_unit_left _ _ h)

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ Associates.mk a ∣ Associates.mk b ↔ a ∣ b

Tactic:
by
  simp only [dvd_def, mk_surjective.exists, mk_mul_mk, mk_eq_mk_iff_associated,
    Associated.comm (x := b)]
  constructor
  · rintro ⟨x, u, rfl⟩
    exact ⟨_, mul_assoc ..⟩
  · rintro ⟨c, rfl⟩
    use c

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : Associates.mk a = Associates.mk (a₁ * a₂)
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : a = a₁ * a₂
⊢ ∃ x x_1, x ∣ b ∧ x_1 ∣ c ∧ Associates.mk a = Associates.mk (x * x_1)

Tactic:
· obtain ⟨u, rfl⟩ := mk_eq_mk_iff_associated.mp eq.symm
    exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : a = a₁ * a₂
⊢ ∃ x x_1, x ∣ b ∧ x_1 ∣ c ∧ Associates.mk a = Associates.mk (x * x_1)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∀ (a_1 : M), a_1 ∣ a → a_1 ∣ b → IsUnit (Associates.mk a_1)) ↔ ∀ ⦃d : M⦄, d ∣ a → d ∣ b → IsUnit d

Tactic:
isUnit_mk

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
⊢ (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates M), Irreducible a ↔ Prime a

Tactic:
simp_rw [forall_associated, irreducible_mk, prime_mk]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
⊢ f ∘ₗ (id - g ∘ₗ f) = 0

Tactic:
rw [comp_sub, comp_id, ← comp_assoc, h, id_comp, sub_self]

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

Goal state before:
pp: case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ g ^ (n + 1) • a

Tactic:
rw [pow_succ', mul_smul]

Goal state after:
case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
hn : a ≤ g ^ n • a
⊢ a ≤ g • g ^ n • a
Module: Mathlib.Algebra.Order.Group.Action

Goal state before:
pp: case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g ^ (n + 1) • a ≤ a

Tactic:
rw [pow_succ', mul_smul]

Goal state after:
case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g • g ^ n • a ≤ a
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 : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
⊢ {↑(f 1)} ⊆ ↑s

Tactic:
rintro _ rfl; exact (f 1).2

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
x : M
s : Set M
y : M
⊢ x ∈ span R (insert y s) ↔ ∃ a, ∃ z ∈ span R s, x = a • y + z

Tactic:
by
  simp [span_insert, mem_sup, mem_span_singleton, eq_comm (a := x)]

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
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ ∀ (i : α → Bool), (⨅ a, b ⊓ bif i a then a else aᶜ) ≤ sSup {a | IsAtom a ∧ a ≤ ⨆ g, ⨅ a, b ⊓ bif g a then a else aᶜ}

Tactic:
intro g

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
⊢ (⨅ a, b ⊓ bif g a then a else aᶜ) ≤ sSup {a | IsAtom a ∧ a ≤ ⨆ g, ⨅ a, b ⊓ bif g a then a else aᶜ}
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ ⇑e.symm ⁻¹' Iic a = Iic (e a)

Tactic:
e.symm.preimage_Iic,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ Iic (e.symm.symm a) = Iic (e a)
Module: Mathlib.Order.Atoms

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

Tactic:
simp only [← isAtomic_dual_iff_isCoatomic, f.dual.isAtomic_iff]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case h
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := ⋯
u : Finset ι := ⋯
⊢ Disjoint (u.sup f) (f b)

Tactic:
exact (supIndep_iff_disjoint_erase.mp (hg i' hi') b hb).symm

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
h_eq : ⨅ i, t i (b₁ i) = ⨅ i, t i (b₂ i)
h_ne : ¬b₁ = b₂
⊢ False

Tactic:
obtain ⟨i, hi⟩ : ∃ i, b₁ i ≠ b₂ i := Function.ne_iff.mp h_ne

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
h_eq : ⨅ i, t i (b₁ i) = ⨅ i, t i (b₂ i)
h_ne : ¬b₁ = b₂
i : ι
hi : b₁ i ≠ b₂ i
⊢ False
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
⊢ k ≤ iSup Subtype.val

Tactic:
delta iSup

Goal state after:
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
⊢ k ≤ sSup (range Subtype.val)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (f ∘ Subtype.val) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)

Tactic:
refine Subtype.forall.trans (forall₂_congr fun a b => ?_)

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) ⟨a, b⟩) (⨆ j, ⨆ (_ : j ≠ ⟨a, b⟩), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) ((s.erase a).sup f)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
⊢ ∀ (s_1 : Set α), s_1.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s_1 → s.sup f ≤ sSup s_1 → ∃ x ∈ s_1, s.sup f ≤ x

Tactic:
intro d hemp hdir hsup

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, s.sup f ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ t, ↑t ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : ↑t ⊆ s
ht2 : c ≤ t.sup id
⊢ a ⊓ t.sup id ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
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: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
j : κ
⊢ ∏ i ∈ s, (f i).indicator (g i) j = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j

Tactic:
by
  rw [Set.indicator]
  split_ifs with hj
  · rw [Finset.prod_apply]
    congr! 1 with i hi
    simp only [Set.mem_iInter] at hj
    exact Set.indicator_of_mem (hj _ hi) _
  · obtain ⟨i, hi, hj⟩ := by simpa using hj
    exact Finset.prod_eq_zero hi <| Set.indicator_of_notMem hj _

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

Goal state before:
pp: case neg
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : ¬S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
exact
      ⟨b, lt_of_le_of_ne hbk H, by
        simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const,
          forall_prop_of_false, not_false_iff]⟩

Goal state after: