mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

pp: case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

pp: case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
· subst x
              exact fun e => (hf i y hy e.symm).elim

Goal state after:
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y
Module: Mathlib.SetTheory.Cardinal.Order

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

Tactic:
induction n <;> simp [*]

Goal state after:
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: N : Type u_1
P : Type u_2
φ : N → N
inst✝ : IsId φ
ψ : N → P
⊢ ψ ∘ φ = ψ

Tactic:
simp only [IsId.eq_id, Function.comp_id]

Goal state after:
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
φ : M → N
ψ : N → N
inst✝ : IsId ψ
⊢ ψ ∘ φ = φ

Tactic:
by simp only [IsId.eq_id, Function.id_comp]

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

Goal state before:
pp: α : Type u
⊢ ¬Subsingleton α ↔ Nontrivial α

Tactic:
← not_nontrivial_iff_subsingleton,

Goal state after:
α : Type u
⊢ ¬¬Nontrivial α ↔ Nontrivial α
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
hb : succ 1 ≤ b
⊢ a < b ^ a

Tactic:
(by norm_cast : succ (1 : Cardinal) = 2)

Goal state after:
a b : Cardinal.{u_1}
hb : 2 ≤ b
⊢ a < b ^ a
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2
a b : Cardinal.{u_1}
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ → a * b < ℵ₀

Tactic:
rintro (rfl | rfl | ⟨ha, hb⟩)

Goal state after:
case refine_2.inl
b : Cardinal.{u_1}
⊢ 0 * b < ℵ₀

case refine_2.inr.inl
a : Cardinal.{u_1}
⊢ a * 0 < ℵ₀

case refine_2.inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b < ℵ₀
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ (x✝² • x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext <;> exact smul_assoc ..

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M₃ : Type u_11
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M₃
inst✝ : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
← mul_one x,

Goal state after:
R : Type u_1
S : Type u_5
M₃ : Type u_11
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M₃
inst✝ : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : f 1 = g 1
x : R
⊢ f (x * 1) = g (x * 1)
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ (f.inverse' g k₂ h₁ h₂).comp f = MulActionHom.id M

Tactic:
by
  ext
  simpa using h₁.eq _

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

Goal state before:
pp: R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
← mul_one x,

Goal state after:
R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ f (x * 1) = g (x * 1)
Module: Mathlib.Algebra.Module.Equiv.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
← one_mul x,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M
h : f 1 = g 1
x : R
⊢ f (1 * x) = g (1 * x)
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝² x✝¹ : S
x✝ : ↥t
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by ext; simp [mul_smul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
a : Rˣ
ha : (fun m ↦ m • ↑y) a = ↑x
⊢ (fun m ↦ m • y) a = x

Tactic:
ext; simpa

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Subsingleton (Submodule R M) ↔ Subsingleton (AddSubmonoid M)

Tactic:
rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_inj,
      bot_toAddSubmonoid, top_toAddSubmonoid]

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

Goal state before:
pp: case mp
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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y ∈ p, ↑e y = x) → e.symm x ∈ p

Tactic:
rintro ⟨y, hy, hx⟩
    simp [← hx, hy]

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

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n ∈ s

Tactic:
by
  rw [← Nat.cast_ofNat]; exact natCast_mem s n

Goal state after:
Module: Mathlib.Data.Nat.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).1 = ↑n

Tactic:
induction n <;> simp [*]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).2 = ↑n

Tactic:
induction n <;> simp [*]

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Injective ⇑b
x y : F
e : (algebraMap F E) x = (algebraMap F E) y
⊢ b x = b y

Tactic:
← mul_one x,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Injective ⇑b
x y : F
e : (algebraMap F E) x = (algebraMap F E) y
⊢ b (x * 1) = b y
Module: Mathlib.Algebra.Ring.Action.Group

Goal state before:
pp: G : Type u_1
inst✝² : Group G
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction G R
x y : G
⊢ (let __src := DistribMulAction.toAddEquiv R (x * y);
    let __src_1 := toRingHom G R (x * y);
    { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ }) =
    (let __src := DistribMulAction.toAddEquiv R x;
      let __src_1 := toRingHom G R x;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ }) *
      let __src := DistribMulAction.toAddEquiv R y;
      let __src_1 := toRingHom G R y;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ }

Tactic:
by ext; simp [mul_smul]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f a * f b

Tactic:
convert! map_dvd f h
              simp

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mpr.inl
M : Type u_2
inst✝ : Monoid M
x y : M
ha : Irreducible x
hb : IsUnit y
⊢ Irreducible (x * y)

Tactic:
irreducible_mul_isUnit hb

Goal state after:
case mpr.inl
M : Type u_2
inst✝ : Monoid M
x y : M
ha : Irreducible x
hb : IsUnit y
⊢ Irreducible x
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
x : M₀
⊢ x ∉ nonZeroDivisorsLeft M₀ ↔ {y | x * y = 0 ∧ y ≠ 0}.Nonempty

Tactic:
simpa [mem_nonZeroDivisorsLeft_iff] using! Set.nonempty_def.symm

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S✝
inst✝¹ : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝ : SMul R α
S : Subring R
⊢ SMul (↥S) α

Tactic:
by infer_instance

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝² : SMul R β
inst✝¹ : SMul α β
inst✝ : SMulCommClass R α β
S : Subring R
⊢ SMulCommClass (↥S) α β

Tactic:
by infer_instance

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝² : SMul α β
inst✝¹ : SMul R β
inst✝ : SMulCommClass α R β
S : Subring R
⊢ SMulCommClass α (↥S) β

Tactic:
by infer_instance

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝⁶ : NonAssocRing R
inst✝⁵ : NonAssocRing S✝
inst✝⁴ : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝³ : SMul α β
inst✝² : SMul R α
inst✝¹ : SMul R β
inst✝ : IsScalarTower R α β
S : Subring R
⊢ IsScalarTower (↥S) α β

Tactic:
by infer_instance

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝⁴ : NonAssocRing R
inst✝³ : NonAssocRing S✝
inst✝² : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝¹ : SMul R α
inst✝ : FaithfulSMul R α
S : Subring R
⊢ FaithfulSMul (↥S) α

Tactic:
by infer_instance

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁴ : NonAssocRing R✝
inst✝³ : NonAssocRing S✝
inst✝² : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝¹ : Ring R
inst✝ : MulAction R α
S : Subring R
⊢ MulAction (↥S) α

Tactic:
by infer_instance

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝² : Ring R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
S : Subring R
⊢ DistribMulAction (↥S) α

Tactic:
by infer_instance

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝² : Ring R
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction R α
S : Subring R
⊢ MulDistribMulAction (↥S) α

Tactic:
by infer_instance

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

Goal state before:
pp: R : Type u
S✝ : Type v
T : Type w
inst✝⁴ : NonAssocRing R
inst✝³ : NonAssocRing S✝
inst✝² : NonAssocRing T
α : Type u_1
β : Type u_2
inst✝¹ : Zero α
inst✝ : SMulWithZero R α
S : Subring R
⊢ SMulWithZero (↥S) α

Tactic:
by infer_instance

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝² : Ring R
inst✝¹ : Zero α
inst✝ : MulActionWithZero R α
S : Subring R
⊢ MulActionWithZero (↥S) α

Tactic:
by infer_instance

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝² : Ring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
S : Subring R
⊢ Module (↥S) α

Tactic:
by infer_instance

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁵ : NonAssocRing R✝
inst✝⁴ : NonAssocRing S✝
inst✝³ : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type ?u.14
inst✝² : Ring R
inst✝¹ : Semiring α
inst✝ : MulSemiringAction R α
S : Subring R
⊢ MulSemiringAction (↥S) α

Tactic:
by infer_instance

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ Associates.mk a = 1 ↔ a ~ᵤ 1

Tactic:
one_eq_mk_one,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ Associates.mk a = Associates.mk 1 ↔ a ~ᵤ 1
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰

Tactic:
by
  rw [mem_nonZeroDivisors_iff_right, mem_nonZeroDivisors_iff_right]
  contrapose!
  constructor
  · rintro ⟨⟨x⟩, hx₁, hx₂⟩
    refine ⟨x, ?_, ?_⟩
    · rwa [← Associates.mk_eq_zero, ← Associates.mk_mul_mk, ← Associates.quot_mk_eq_mk]
    · rwa [← Associates.mk_ne_zero, ← Associates.quot_mk_eq_mk]
  · refine fun ⟨b, hb₁, hb₂⟩ ↦ ⟨Associates.mk b, ?_, by rwa [Associates.mk_ne_zero]⟩
    rw [Associates.mk_mul_mk, hb₁, Associates.mk_zero]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
⊢ NoZeroDivisors (Associates M)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
hst : (s * t).Nonempty
H : (∃ a ∈ s, ¬a = 0) ∧ ∃ a ∈ t, ¬a = 0
⊢ False

Tactic:
obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
hst : (s * t).Nonempty
a : α
hs : a ∈ s
ha : ¬a = 0
b : α
ht : b ∈ t
hb : ¬b = 0
⊢ False
Module: Mathlib.Algebra.Order.Group.Action

Goal state before:
pp: 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 : ℕ
⊢ g ^ n • a ≤ a

Tactic:
induction n with
  | zero => rw [pow_zero, one_smul]
  | succ n hn =>
    rw [pow_succ', mul_smul]
    exact (smul_mono_right g hn).trans h

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

Goal state before:
pp: case mp
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
x✝ : M
hx : x✝ ∈ ∅ • N
⊢ x✝ ∈ ⊥

Tactic:
rw [mem_set_smul_def, Submodule.mem_sInf] at hx

Goal state after:
case mp
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
x✝ : M
hx : ∀ p ∈ {p | ∀ ⦃r : S⦄ {n : M}, r ∈ ∅ → n ∈ N → r • n ∈ p}, x✝ ∈ p
⊢ x✝ ∈ ⊥
Module: Mathlib.Order.SupClosed

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a ⊔ f b ∈ ⇑f '' s

Tactic:
← map_sup

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f (a ⊔ b) ∈ ⇑f '' 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 : α
⊢ a = ⊥ ∨ ∃ a_1, IsAtom a_1 ∧ a_1 ≤ a

Tactic:
rw [or_iff_not_imp_left, ← Ne, ← bot_lt_iff_ne_bot]

Goal state after:
ι : 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 : α
⊢ ⊥ < a → ∃ a_2, IsAtom a_2 ∧ a_2 ≤ a
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 : α
⊢ ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
by
    inhabit α
    refine ⟨{ a | IsAtom a ∧ a ≤ b }, ?_, fun a ha => ha.1⟩
    refine le_antisymm ?_ (sSup_le fun c hc => hc.2)
    have : (⨅ c : α, ⨆ x, b ⊓ cond x c (cᶜ)) = b := by simp [iSup_bool_eq]
    rw [← this]; clear this
    simp_rw [iInf_iSup_eq, iSup_le_iff]; intro g
    if h : (⨅ a, b ⊓ cond (g a) a (aᶜ)) = ⊥ then simp [h] else
    refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩; clear h
    have := lt_of_lt_of_le hc (le_trans (iInf_le _ c) inf_le_right)
    revert this
    nontriviality α
    cases g c <;> simp

Goal state after:
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_4
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ IsSimpleOrder α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

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

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ IsAtomic αᵒᵈ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : α
⊢ ⊤ ≤ x ⊔ if x = ⊥ then ⊤ else ⊥

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

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ x ∈ span R (insert y s) ↔ ∃ a, x + a • y ∈ span R s

Tactic:
by
  rw [mem_span_insert]; constructor
  · rintro ⟨a, z, hz, rfl⟩
    exact ⟨-a, by simp [hz, add_assoc]⟩
  · rintro ⟨a, h⟩
    exact ⟨-a, _, h, by simp [add_comm]⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x y : α
⊢ (if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = x ⊓ if y = ⊥ then ⊤ else ⊥

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

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ IsAtomistic αᵒᵈ

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
⊢ IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥

Tactic:
simp only [← bot_covBy_iff, Pi.covBy_iff, bot_apply, eq_comm]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ s i ∈ upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s})

pp: case refine_2
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ s i ∈ lowerBounds (upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s}))

Tactic:
· rintro _ ⟨_, ⟨⟨_, _, _, rfl⟩, hs⟩, rfl⟩
      exact hs i

Goal state after:
case refine_2
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ s i ∈ lowerBounds (upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s}))
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr.inr
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))

Tactic:
· convert! h.symm using 1
      simp [hab, sSup_singleton]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup (insert x y \ {x}))
⊢ Disjoint x (sSup y)

Tactic:
insert_sdiff_of_mem _ (mem_singleton _),

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup (y \ {x}))
⊢ Disjoint x (sSup y)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ ⨆ i ∈ Finset.univ, f i = f 0 ⊔ f 1 ⊔ f 2

Tactic:
← Finset.sup_eq_iSup,

Goal state after:
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ Finset.univ.sup f = f 0 ⊔ f 1 ⊔ f 2