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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤) ↔ ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤

Tactic:
constructor
  · rintro ⟨s, hps, hs⟩
    refine ⟨range s, countable_range s, forall_mem_range.2 hps, ?_⟩
    rwa [sSup_range]
  · rintro ⟨S, hSc, hps, hS⟩
    rcases eq_empty_or_nonempty S with (rfl | hne)
    · rw [sSup_empty] at hS
      have := subsingleton_of_bot_eq_top hS
      rcases h with ⟨x, hx⟩
      exact ⟨fun _ => x, fun _ => hx, Subsingleton.elim _ _⟩
    · rcases (Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩
      refine ⟨fun n => s n, fun n => hps _ (s n).coe_prop, ?_⟩
      rwa [hs.iSup_comp, ← sSup_eq_iSup']

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

Goal state before:
pp: case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ (↑⟨l, hl⟩).length

Tactic:
hl

Goal state after:
case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ n
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
c : γ
h : t c ((f.trans g.toRelEmbedding) a)
⊢ c ∈ Set.range ⇑(f.trans g.toRelEmbedding)

Tactic:
by
    simp only [RelEmbedding.coe_trans, coe_coe_fn, comp_apply] at h ⊢
    rcases g.2 _ _ h with ⟨b, rfl⟩; have h := g.map_rel_iff.1 h
    rcases f.2 _ _ h with ⟨a', rfl⟩; exact ⟨a', rfl⟩

Goal state after:
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.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b

Tactic:
← lift_lift.{u, w, v},

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
⊢ ωScottContinuous fun x ↦ (f x) (g x)

Tactic:
apply ωScottContinuous.of_monotone_map_ωSup ⟨?_, fun c ↦ ?_⟩
  · intro x y hxy
    exact OrderHom.apply_mono (hf.monotone hxy) (hg.monotone hxy)
  · rw [hf.map_ωSup, hg.map_ωSup]
    simp only [ωSup_def, ωSup_apply]
    apply le_antisymm
    · apply ωSup_le
      intro i
      dsimp
      rw [(f (c i)).continuous]
      apply ωSup_le
      intro j
      apply le_ωSup_of_le (i ⊔ j)
      apply apply_mono
      · apply hf.monotone (c.monotone le_sup_left)
      · apply hg.monotone (c.monotone le_sup_right)
    · simp only [ωSup_le_iff]
      intro i
      apply le_ωSup_of_le i
      apply (f (c i)).monotone
      apply le_ωSup_of_le i
      rfl

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

Goal state before:
pp: a : Cardinal.{u}
h✝ : succ (lift.{v, u} a) < lift.{v, u} (succ a)
b : Cardinal.{u}
h : b < succ a
hb : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False

Tactic:
lt_succ_iff,

Goal state after:
a : Cardinal.{u}
h✝ : succ (lift.{v, u} a) < lift.{v, u} (succ a)
b : Cardinal.{u}
h : b ≤ a
hb : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ₀ = lift.{v, u} c ↔ ℵ₀ = c

Tactic:
simpa using lift_inj (a := ℵ₀)

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

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ toNat a = n ↔ a = ↑n

Tactic:
nth_rw 2 [← Cardinal.cast_toNat_of_lt_aleph0 lt]
  exact Nat.cast_inj.symm

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

Goal state before:
pp: α : Type u
⊢ ¬#α ≤ ℵ₀ ↔ Uncountable α

Tactic:
← not_countable_iff,

Goal state after:
α : Type u
⊢ ¬#α ≤ ℵ₀ ↔ ¬Countable α
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #↑(image2 f s t) ≤ #↑s * #↑t

Tactic:
rw [← image_uncurry_prod, ← mk_setProd]
  exact mk_image_le

Goal state after:
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✝¹ : Monoid M
inst✝ : Monoid N
x✝ : MulAction (M × N) α
instM : MulAction M α := compHom α (MonoidHom.inl M N)
instN : MulAction N α := compHom α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ (m * 1, 1 * n) • a = (1 * m, n * 1) • a

Tactic:
mul_one,

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : MulAction (M × N) α
instM : MulAction M α := compHom α (MonoidHom.inl M N)
instN : MulAction N α := compHom α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ (m, 1 * n) • a = (1 * m, n) • a
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✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ (m * 1, 1 * n) • a = SMul.smul (m, n) a

Tactic:
mul_one,

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ (m, 1 * n) • a = SMul.smul (m, n) a
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
X : Type u_5
inst✝⁶ : SMul M' X
Y : Type u_6
inst✝⁵ : SMul M' Y
F : Type u_8
inst✝⁴ : FunLike F X Y
inst✝³ : MulOneClass X
inst✝² : SMul X Y
inst✝¹ : IsScalarTower M' X Y
inst✝ : MulActionHomClass F X X Y
f : F
m : M'
x : X
⊢ m • f (x * 1) = id m • f x

Tactic:
mul_one,

Goal state after:
M' : Type u_1
X : Type u_5
inst✝⁶ : SMul M' X
Y : Type u_6
inst✝⁵ : SMul M' Y
F : Type u_8
inst✝⁴ : FunLike F X Y
inst✝³ : MulOneClass X
inst✝² : SMul X Y
inst✝¹ : IsScalarTower M' X Y
inst✝ : MulActionHomClass F X X Y
f : F
m : M'
x : X
⊢ m • f x = id m • f x
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
⊢ (fun m ↦ { toFun := fun x ↦ x * MulOpposite.unop m, map_smul' := ⋯ }) ((fun f ↦ MulOpposite.op (f 1)) f) = f

Tactic:
by ext m; change m • f 1 = _; rw [← map_smul, smul_eq_mul, mul_one]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f * g) 1 = MulOpposite.unop (MulOpposite.op (g 1)) * MulOpposite.unop (MulOpposite.op (f 1))

Tactic:
by
    dsimp [← smul_eq_mul]; simp_rw [← map_smul, smul_eq_mul, mul_one]; rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn.1 • (mn.2 • a + mn.2 • a') = mn • a + mn • a'

Tactic:
smul_add

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn.1 • mn.2 • a + mn.1 • mn.2 • a' = mn • a + mn • a'
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ (m * 1, 1 * n) • a = SMul.smul (m, n) a

Tactic:
mul_one,

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ (m, 1 * n) • a = SMul.smul (m, n) a
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case add
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, ↑i
hy✝ : y✝ ∈ ⨆ i, ↑i
⊢ t • x✝ ∈ ⨆ a, ↑a → t • y✝ ∈ ⨆ a, ↑a → t • (x✝ + y✝) ∈ ⨆ a, ↑a

Tactic:
smul_add

Goal state after:
case add
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, ↑i
hy✝ : y✝ ∈ ⨆ i, ↑i
⊢ t • x✝ ∈ ⨆ a, ↑a → t • y✝ ∈ ⨆ a, ↑a → t • x✝ + t • y✝ ∈ ⨆ a, ↑a
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * (x✝ * ↑n) + x✝¹ * x✝ * 1 = x✝¹ * (x✝ * ↑n) + x✝¹ * (x✝ * 1)

Tactic:
mul_one,

Goal state after:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * (x✝ * ↑n) + x✝¹ * x✝ = x✝¹ * (x✝ * ↑n) + x✝¹ * (x✝ * 1)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * -1 + x✝¹ * x✝ * -↑n = x✝¹ * (x✝ * -1) + x✝¹ * (x✝ * -↑n)

Tactic:
mul_neg,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝ * 1) + x✝¹ * x✝ * -↑n = x✝¹ * (x✝ * -1) + x✝¹ * (x✝ * -↑n)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝ * 1) + x✝¹ * x✝ * -↑n = x✝¹ * (x✝ * -1) + x✝¹ * (x✝ * -↑n)

Tactic:
mul_one,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + x✝¹ * x✝ * -↑n = x✝¹ * (x✝ * -1) + x✝¹ * (x✝ * -↑n)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + x✝¹ * x✝ * -↑n = x✝¹ * (x✝ * -1) + x✝¹ * (x✝ * -↑n)

Tactic:
mul_neg,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * x✝ * ↑n) = x✝¹ * (x✝ * -1) + x✝¹ * (x✝ * -↑n)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * x✝ * ↑n) = x✝¹ * (x✝ * -1) + x✝¹ * (x✝ * -↑n)

Tactic:
mul_neg,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * x✝ * ↑n) = x✝¹ * -(x✝ * 1) + x✝¹ * (x✝ * -↑n)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * x✝ * ↑n) = x✝¹ * -(x✝ * 1) + x✝¹ * (x✝ * -↑n)

Tactic:
mul_one,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * x✝ * ↑n) = x✝¹ * -x✝ + x✝¹ * (x✝ * -↑n)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * x✝ * ↑n) = x✝¹ * -x✝ + x✝¹ * (x✝ * -↑n)

Tactic:
mul_neg,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * x✝ * ↑n) = -(x✝¹ * x✝) + x✝¹ * (x✝ * -↑n)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * (x✝ * ↑n)) = x✝¹ * (x✝ * -↑n)

Tactic:
mul_neg,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * (x✝ * ↑n)) = x✝¹ * -(x✝ * ↑n)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * -a = x✝¹ * (x✝ * -a)

Tactic:
mul_neg,

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(x✝¹ * x✝ * a) = x✝¹ * (x✝ * -a)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(x✝¹ * (x✝ * a)) = x✝¹ * (x✝ * -a)

Tactic:
mul_neg,

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(x✝¹ * (x✝ * a)) = x✝¹ * -(x✝ * a)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * -a = x✝¹ * (x✝ * -a)

Tactic:
by rw [mul_neg, ha.right_assoc, mul_neg, mul_neg]

Goal state after:
Module: Mathlib.Algebra.Ring.Centralizer

Goal state before:
pp: M : Type u_1
S : Set M
a : M
inst✝¹ : Mul M
inst✝ : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
⊢ c * -a = -a * c

Tactic:
mul_neg,

Goal state after:
M : Type u_1
S : Set M
a : M
inst✝¹ : Mul M
inst✝ : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
⊢ -(c * a) = -a * c
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
⊢ C x₁ hx₁

Tactic:
by
  refine Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc
  refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁
      (fun i x₂ hx₂ => ?_) fun x₃ y => ?_
  · exact ⟨_, mem _ _ hx₂⟩
  · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, mul _ _ _ _ Cx Cy⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
m : M
⊢ ((algebraMap R A) r * 1) • m = (algebraMap R A) r • 1 • m

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
m : M
⊢ (algebraMap R A) r • m = (algebraMap R A) r • 1 • m
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 : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • b (y * z) = x • (b (z * 1) * b 1)
⊢ (algebraMap F E) (x * y) = b x

Tactic:
mul_one,

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 : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • b (y * z) = x • (b z * b 1)
⊢ (algebraMap F E) (x * y) = b x
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 : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • y • 1 = b (x * 1)
⊢ (algebraMap F E) (x * y) = b x

Tactic:
mul_one,

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 : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • y • 1 = b x
⊢ (algebraMap F E) (x * y) = b x
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: case mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ algebraMapSubmonoid B M → x ∈ Submonoid.map f (algebraMapSubmonoid A M)

Tactic:
rintro ⟨r, hr, rfl⟩

Goal state after:
case mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R B) r ∈ Submonoid.map f (algebraMapSubmonoid A M)
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
⊢ a ∣ p * b → p ∣ a ∨ a ∣ b

Tactic:
rintro ⟨c, hc⟩

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b c : M
hc : p * b = a * c
⊢ p ∣ a ∨ a ∣ b
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r x : M₀
hr : r ∈ M₀⁰
⊢ r * x = 0 ↔ x = 0

Tactic:
rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
⊢ Prime (Associates.mk p) ↔ Prime p

Tactic:
Prime,

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a b : Associates M), Associates.mk p ∣ a * b → Associates.mk p ∣ a ∨ Associates.mk p ∣ b) ↔
    Prime p
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) → ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
rintro ⟨x, hx, u, rfl⟩

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
u : Mˣ
⊢ ∃ x_1, ¬IsUnit x_1 ∧ a * x * ↑u = a * x_1
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
hq : q ≠ 0
⊢ r = q * (x * ↑u)

Tactic:
mul_comm x,

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
hq : q ≠ 0
⊢ r = q * (↑u * x)
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
r : R
⊢ e.toRingEquiv.symm.toFun ((algebraMap R A₂) r) = (algebraMap R A₁) r

Tactic:
← e.toRingEquiv.symm_apply_apply (algebraMap R A₁ r)

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
r : R
⊢ e.toRingEquiv.symm.toFun ((algebraMap R A₂) r) = e.toRingEquiv.symm (e.toRingEquiv ((algebraMap R A₁) r))
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 : A
⊢ (algebraMap R A) (e.symm (e 1 * x)) = (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1 * 1)

Tactic:
mul_one,

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 : A
⊢ (algebraMap R A) (e.symm (e 1 * x)) = (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1)
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 : A
⊢ (algebraMap R A) (e.symm 1) * e (e.symm (e 1 * x) * 1) = x

Tactic:
mul_one,

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 : A
⊢ (algebraMap R A) (e.symm 1) * e (e.symm (e 1 * x)) = x
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 : A
⊢ e (e.symm 1 * 1) * x = x

Tactic:
mul_one,

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 : A
⊢ e (e.symm 1) * x = x
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
⊢ (N₁ ⊔ N₂).submoduleOf N = N₁.submoduleOf N ⊔ N₂.submoduleOf N

Tactic:
apply Submodule.map_injective_of_injective N.subtype_injective

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
⊢ map N.subtype ((N₁ ⊔ N₂).submoduleOf N) = map N.subtype (N₁.submoduleOf N ⊔ N₂.submoduleOf N)
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ (∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2) ↔ (∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2

Tactic:
exact ⟨fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩, by simp_all⟩

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
s : Submodule R M
f : R →ₗ[R] ↥s
hf : Surjective ⇑f
x : M
hx : x ∈ s
r : R
eq : f r = ⟨x, hx⟩
⊢ ↑(f (r * 1)) = x

Tactic:
mul_one,

Goal state after:
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
x : M
hx : x ∈ s
r : R
eq : f r = ⟨x, hx⟩
⊢ ↑(f r) = x
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
G : Type u_9
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
g : G
x : M
⊢ R ∙ g • x = R ∙ x

Tactic:
by
  refine le_antisymm (span_singleton_smul_le R g x) ?_
  convert! span_singleton_smul_le R g⁻¹ (g • x)
  exact (inv_smul_smul g x).symm

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
r : R
hr : IsUnit r
x : M
⊢ R ∙ r • x = R ∙ x

Tactic:
lift r to Rˣ using hr
  rw [← Units.smul_def]
  exact span_singleton_group_smul_eq R r x

Goal state after: