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

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
a✝ : y ≠ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y

Tactic:
rw [← bot_eq_of_le_or_map_le le_map hy] at hz

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
hz : z ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
a✝ : y ≠ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
i : ι
⊢ f i ≤ sum f

Tactic:
by
  simpa [← lift_umax] using lift_le_sum f i

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

Goal state before:
pp: α β : Type u
a b : ℕ
h : lift.{u_1, 0} #(Fin a) = lift.{u_1, 0} #(Fin b)
⊢ a = b

Tactic:
lift_inj,

Goal state after:
α β : Type u
a b : ℕ
h : #(Fin a) = #(Fin b)
⊢ a = b
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x * y).toENatAux = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
⊢ y.toENatAux * x.toENatAux = x.toENatAux * y.toENatAux

Tactic:
mul_comm

Goal state after:
case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x * y).toENatAux = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
⊢ x.toENatAux * y.toENatAux = x.toENatAux * y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: m : ℕ∞
hm : m ≠ 0
⊢ ℵ₀ * ↑m = ℵ₀

Tactic:
rw [mul_comm, ofENat_mul_aleph0 hm]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M (b * a)

Tactic:
mul_comm

Goal state after:
R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M (a * b)
Module: Mathlib.SetTheory.Cardinal.Basic

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

pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
· exact Or.inl ha

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
⊢ s.card ≤ n

Tactic:
let u : Finset α := s.image Subtype.val
  have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn
  grind

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

Goal state before:
pp: case inj'
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective (Subtype.coind (fun x ↦ f ↑x) ⋯)

Tactic:
apply Subtype.coind_injective

Goal state after:
case inj'
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective fun x ↦ f ↑x
Module: Mathlib.Algebra.GroupWithZero.Action.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
⊢ ∀ (r : (i : I) → f i) (x y : (i : I) → g i), r • (x * y) = r • x * r • y

Tactic:
intros
    ext x
    apply smul_mul'

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

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[id] Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : M
x : Y₁
⊢ g (m • f (g x)) = g (f (m • g x))

Tactic:
simp only [map_smul]

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

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p q : SubMulAction R M
h : p.carrier = q.carrier
⊢ p = q

Tactic:
cases p; cases q; congr

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : SubMulAction M α
⊢ Set.range ⇑s.inclusion = s.carrier

Tactic:
by
  rw [inclusion.coe_eq]
  exact Subtype.range_coe

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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 σ₂₁ σ₁₂
inst✝¹ : Subsingleton R
inst✝ : Subsingleton R₂
this✝ : Subsingleton M
this : Subsingleton M₂
⊢ Unique (M ≃ₛₗ[σ₁₂] M₂)

Tactic:
infer_instance

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

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 R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p q : Submodule R M
inst✝ : Subsingleton R
this : Subsingleton M
⊢ Unique (Submodule R M)

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ f.ker ≤ (g ∘ₛₗ f).ker

Tactic:
rw [ker_comp]; exact comap_mono bot_le

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n : ℕ
x : M
h : x ∈ (fun n ↦ (f ^ n).ker) n
c : ℕ
w : n ≤ n + c
⊢ x ∈ (fun n ↦ (f ^ n).ker) (n + c)

Tactic:
rw [LinearMap.mem_ker] at h

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n : ℕ
x : M
h : (f ^ n) x = 0
c : ℕ
w : n ≤ n + c
⊢ x ∈ (fun n ↦ (f ^ n).ker) (n + c)
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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ x ∈ map (↑e) p ↔ e.symm x ∈ p

Tactic:
rw [Submodule.mem_map]

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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y ∈ p, ↑e y = x) ↔ e.symm x ∈ p
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right
  tauto

Goal state after:
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
hb : b ∈ S
r s : R
hx✝ : r ∈ closure ↑S
hy✝ : s ∈ closure ↑S
hr : r * b ∈ closure ↑S
hs : s * b ∈ closure ↑S
⊢ (r + s) * b ∈ closure ↑S

Tactic:
simpa only [add_mul] using add_mem hr hs

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

Goal state before:
pp: 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
hy : y ∈ closure s
⊢ p x y hx hy

Tactic:
induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | neg _ _ h => exact neg_left _ _ _ _ h
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | neg _ _ h => exact neg_right _ _ _ _ h

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ a

Tactic:
mul_comm

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ b * a
⊢ p ^ n ∣ a
Module: Mathlib.Algebra.GroupWithZero.Associated

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

Tactic:
mul_comm

Goal state after:
N : Type u_2
inst✝ : CommMonoid N
a u : N
hu : IsUnit u
⊢ a * u ~ᵤ a
Module: Mathlib.Algebra.GroupWithZero.Associated

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

Tactic:
mul_comm

Goal state after:
N : Type u_2
inst✝ : CommMonoid N
u a b : N
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
r : M₀
⊢ r ∉ M₀⁰ ↔ {s | r * s = 0 ∧ s ≠ 0}.Nonempty ∨ {s | s * r = 0 ∧ s ≠ 0}.Nonempty

Tactic:
simp [-not_and, not_and_or, mem_nonZeroDivisors_iff, Set.nonempty_def]

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
⊢ ((∀ (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

Tactic:
h.symm.toEquiv_eq_coe,

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 a = 0 → ↑h.symm a = 0) ∧ ∀ (a : S), ↑h.symm a * h.symm x✝ = 0 → ↑h.symm a = 0) ↔
    (∀ (x : S), x✝ * x = 0 → x = 0) ∧ ∀ (x : S), x * x✝ = 0 → x = 0
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
infer_instance

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a' b' : Associates M
a b : M
⊢ ⟦a * b⟧ = ⟦b * a⟧

Tactic:
mul_comm

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a' b' : Associates M
a b : M
⊢ ⟦b * a⟧ = ⟦b * a⟧
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ b * a

Tactic:
mul_comm

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ a * b
Module: Mathlib.Algebra.GroupWithZero.Associated

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

Tactic:
infer_instance

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

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

Tactic:
change range ((-LinearMap.id : M₂ →ₗ[R₂] M₂).comp f) = _
  rw [range_comp, Submodule.map_neg, Submodule.map_id]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : R
⊢ e.symm (e 1 * (algebraMap R A) x) = e.symm ((algebraMap R A) x * e 1)

Tactic:
mul_comm

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : R
⊢ e.symm ((algebraMap R A) x * e 1) = e.symm ((algebraMap R A) x * e 1)
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: α : Type u_2
ι : Type u_5
κ : Type u_6
inst✝ : DistribLattice α
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → α
⊢ (s.sup' hs fun i ↦ f i ⊓ t.sup' ht g) = (s ×ˢ t).sup' ⋯ fun i ↦ f i.1 ⊓ g i.2

Tactic:
Finset.sup'_inf_distrib_left,

Goal state after:
α : Type u_2
ι : Type u_5
κ : Type u_6
inst✝ : DistribLattice α
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → α
⊢ (s.sup' ⋯ fun x ↦ t.sup' ht fun i ↦ f x ⊓ g i) = (s ×ˢ t).sup' ⋯ fun i ↦ f i.1 ⊓ g i.2
Module: Mathlib.LinearAlgebra.Span.Defs

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

Tactic:
by
  induction hb using span_induction with
  | mem z hz => induction ha using span_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h
  | zero => exact zero_right a ha
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | smul _ _ _ h => exact smul_right _ _ _ _ _ h

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderBot A
K : A
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥

Tactic:
IsAtom,

Goal state after:
A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderBot A
K : A
⊢ (K ≠ ⊥ ∧ ∀ b < K, b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
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
⊢ SupClosed (⇑f '' s)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
  rw [← map_sup]
  exact Set.mem_image_of_mem _ <| hs ha hb

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
⊢ upperBounds s ⊆ upperBounds (supClosure s)

Tactic:
rintro a ha _ ⟨t, ht, hts, rfl⟩

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
ha : a ∈ upperBounds s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
⊢ t.sup' ht id ≤ a
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✝ : PredOrder α
⊢ IsStronglyAtomic αᵒᵈ

Tactic:
infer_instance

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
a b c : R
⊢ ∃ b_1 c_1, a • x + b_1 • y + c_1 • z = a • x + (b • y + c • z)

Tactic:
exact ⟨b, c, by rw [add_assoc]⟩

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:
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 α
⊢ IsAtomic αᵒᵈ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : 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
⊢ f '' latticeClosure s = latticeClosure (f '' s)

Tactic:
simpa only [Set.image_comp, Equiv.image_symm_eq_preimage, ← ofDual_preimage_latticeClosure]
    using! image_latticeClosure s (ofDual.symm ∘ f) map_sup map_inf

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

Tactic:
cases nonempty_fintype (PLift ι)

Goal state after:
case intro
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val✝ : Fintype (PLift ι)
⊢ ⨆ i, f i ∈ s
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:
infer_instance

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

Goal state before:
pp: case refine_2.inr
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
hjk : j ≠ k
⊢ v k ∈ span R (range (update v j (v j + r • v i)))

Tactic:
· exact subset_span ⟨k, update_of_ne hjk.symm ..⟩

Goal state after: