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

Goal state before:
pp: c d : ℕ
⊢ toNat (↑c + ↑d) = toNat ↑c + toNat ↑d

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ∞
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ
n : ℕ∞
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ 0 < ↑m ↔ 0 < m

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ 1 < ↑m ↔ 1 < m

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ∞
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ ↑m ≤ 1 ↔ m ≤ 1

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ
n : ℕ∞
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
norm_cast

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

Goal state before:
pp: n : ℕ∞
⊢ 1 ≤ ↑n ↔ 1 ≤ n

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ∞
n : ℕ
⊢ ↑m = ↑n ↔ m = ↑n

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ
n : ℕ∞
⊢ ↑m = ↑n ↔ ↑m = n

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ ↑m = 0 ↔ m = 0

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ 0 = ↑m ↔ m = 0

Tactic:
norm_cast

Goal state after:
m : ℕ∞
⊢ 0 = m ↔ m = 0
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: m : ℕ∞
⊢ ↑m = 1 ↔ m = 1

Tactic:
norm_cast

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

Goal state before:
pp: m : ℕ∞
⊢ 1 = ↑m ↔ m = 1

Tactic:
norm_cast

Goal state after:
m : ℕ∞
⊢ 1 = m ↔ m = 1
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: n : ℕ∞
x : Cardinal.{u_1}
⊢ ↑n ≤ x ↔ n ≤ x.toENatAux

Tactic:
by
  cases lt_or_ge x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]

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

Goal state before:
pp: case inl
c : Cardinal.{u}
ha : c ≤ ℵ₀
⊢ toENat (lift.{v, u} c) = toENat c

Tactic:
lift c to ℕ∞ using ha

Goal state after:
case inl
c : ℕ∞
⊢ toENat (lift.{v, u} ↑c) = toENat ↑c
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ua : IsUnit a
⊢ IsSMulRegular M a

Tactic:
rcases ua with ⟨a, rfl⟩

Goal state after:
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a : Rˣ
⊢ IsSMulRegular M ↑a
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case e'_1.e'_3
c : Cardinal.{u_1}
⊢ 2 = ↑1 + 1

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ succ 0 = 1

Tactic:
norm_cast

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

Goal state before:
pp: ⊢ 1 < 2

Tactic:
norm_cast

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

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

Tactic:
norm_cast

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

Goal state before:
pp: α : Type u_1
P Q : Set α
⊢ #↑(P ∪ Q) ≤ ℵ₀ ↔ #↑P ≤ ℵ₀ ∧ #↑Q ≤ ℵ₀

Tactic:
simp only [le_aleph0_iff_subtype_countable, ofPred_mem_eq, Set.union_def,
    ← countable_union]

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
h : f ∘ₛₗ ↑e₁₂ = g ∘ₛₗ ↑e₁₂
⊢ f = g

Tactic:
(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm,

Goal state after:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
h : f ∘ₛₗ ↑e₁₂ = g ∘ₛₗ ↑e₁₂
⊢ f = (f ∘ₛₗ ↑e₁₂) ∘ₛₗ ↑e₁₂.symm
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x✝ : M
⊢ (ofSubsingleton M M) x✝ = (refl R M) x✝

Tactic:
simp [eq_iff_true_of_subsingleton]

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₃
hg : g.ker = ⊥
⊢ (g ∘ₛₗ f).ker = f.ker

Tactic:
ker_comp,

Goal state after:
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₃
hg : g.ker = ⊥
⊢ Submodule.comap f g.ker = f.ker
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 σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x : ↥(map f p)
⊢ f ↑((equivMapOfInjective f i p).symm x) = ↑x

Tactic:
by
  rw [← LinearEquiv.apply_symm_apply (equivMapOfInjective f i p) x, coe_equivMapOfInjective_apply,
    i.eq_iff, LinearEquiv.apply_symm_apply]

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

Goal state before:
pp: case mk
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
fst✝ : R
snd✝ : S
⊢ (fun x ↦ (x, 0)) (fst✝, snd✝).1 = (fst✝, snd✝)

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case mk
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
fst✝ : S
snd✝ : R
⊢ (fun x ↦ (0, x)) (fst✝, snd✝).2 = (fst✝, snd✝)

Tactic:
simp [eq_iff_true_of_subsingleton]

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

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

Tactic:
apply FaithfulSMul.algebraMap_injective R A

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

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

Tactic:
rw [algebraMap.smul', algebraMap.smul', algebraMap.smul', mul_smul]

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

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

Tactic:
apply FaithfulSMul.algebraMap_injective R A

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : R
⊢ (algebraMap R A) (1 • x✝) = (algebraMap R A) x✝
Module: Mathlib.Algebra.Algebra.Basic

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

Tactic:
apply FaithfulSMul.algebraMap_injective R A

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : G
⊢ (algebraMap R A) (x✝ • 0) = (algebraMap R A) 0
Module: Mathlib.Algebra.Algebra.Basic

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

Tactic:
apply FaithfulSMul.algebraMap_injective R A

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ (algebraMap R A) (x✝² • (x✝¹ + x✝)) = (algebraMap R A) (x✝² • x✝¹ + x✝² • x✝)
Module: Mathlib.Algebra.Algebra.Basic

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

Tactic:
apply FaithfulSMul.algebraMap_injective R A

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : G
⊢ (algebraMap R A) (x✝ • 1) = (algebraMap R A) 1
Module: Mathlib.Algebra.Algebra.Basic

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

Tactic:
apply FaithfulSMul.algebraMap_injective R A

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ (algebraMap R A) (x✝² • (x✝¹ * x✝)) = (algebraMap R A) (x✝² • x✝¹ * x✝² • x✝)
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : DvdNotUnit p q
hq : Irreducible q
⊢ IsUnit p

Tactic:
obtain ⟨_, x, hx, hx'⟩ := h

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
hq : Irreducible q
left✝ : p ≠ 0
x : M
hx : ¬IsUnit x
hx' : q = p * x
⊢ IsUnit p
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
⊢ Function.Injective fun n ↦ q ^ n

Tactic:
by
  refine .of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩
  · exact not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')
  · exact (pow_mul_pow_sub q h.le).symm

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

Tactic:
map_eq_zero_iff _ h.symm.injective

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

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

Tactic:
mul_right_mem_nonZeroDivisors_eq_zero_iff hr

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r x : M₀
hr : r ∈ M₀⁰
⊢ x = 0 ↔ x = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
u : (Associates M)ˣ
⊢ ↑u = 1

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ b_1, ↑a * ↑↑b_1 = ↑b) ↔ ∃ u, a * ↑u = b

Tactic:
norm_cast

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.range = ⊤ ↔ Surjective ⇑f

Tactic:
rw [SetLike.ext'_iff, coe_range, top_coe, Set.range_eq_univ]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
a b : α
hab : Disjoint a b
⊢ ∃ a', a ≤ a' ∧ IsCompl a' b

Tactic:
obtain ⟨u, hu⟩ := ComplementedLattice.exists_isCompl (a ⊔ b)

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
a b : α
hab : Disjoint a b
u : α
hu : IsCompl (a ⊔ b) u
⊢ ∃ a', a ≤ a' ∧ IsCompl a' b
Module: Mathlib.LinearAlgebra.Span.Defs

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

Tactic:
rintro ⟨b, c, rfl⟩

Goal state after:
case refine_2
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
⊢ ∃ z_1, (∃ a b, a • y + b • z = z_1) ∧ a • x + b • y + c • z = a • x + z_1
Module: Mathlib.Order.Atoms

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder α → IsSimpleOrder αᵒᵈ

Tactic:
intro i

Goal state after:
case mp
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder α
⊢ IsSimpleOrder αᵒᵈ
Module: Mathlib.Order.Atoms

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder αᵒᵈ → IsSimpleOrder α

Tactic:
intro i

Goal state after:
case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α
Module: Mathlib.Order.Interval.Set.OrderIso

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

Tactic:
e.symm.preimage_Icc,

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

Goal state before:
pp: ι✝ : 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
⊢ ∀ (a : ι), IsLUB (Function.eval a '' {f | IsAtom f ∧ f ≤ s}) (s a)

Tactic:
intro i

Goal state after:
ι✝ : 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 : ι
⊢ IsLUB (Function.eval i '' {f | IsAtom f ∧ f ≤ s}) (s i)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (s.product t).SupIndep f
u : Finset ι'
x✝² : u ⊆ t
i : ι'
x✝¹ : i ∈ t
x✝ : i ∉ u
⊢ Disjoint ((fun i' ↦ s.sup fun i ↦ f (i, i')) i) (u.sup fun i' ↦ s.sup fun i ↦ f (i, i'))

Tactic:
suffices Disjoint ((s.image ((·, i))).sup f) ((s ×ˢ u).sup f) by
      simpa only [sup_image, sup_product_right]
    grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
⊢ iSupIndep t

Tactic:
intro i

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep (t ∘ f)
hf : Surjective f
i : ι
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
⊢ ∀ (i : ι), Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Tactic:
intro i

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
ht : iSupIndep (Subtype.val ∘ t)
⊢ iSupIndep t

Tactic:
intro i

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
ht : iSupIndep (Subtype.val ∘ t)
i : ι
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : Fintype ι
f : ι → α
⊢ iSupIndep f ↔ Finset.univ.SupIndep f

Tactic:
by
  classical
    simp [Finset.supIndep_iff_disjoint_erase, iSupIndep, Finset.sup_eq_iSup]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
⊢ (fun φ i ↦ φ.comp (MonoidHom.mulSingle M i)) ((fun φ ↦ ∏ i, (φ i).comp (evalMonoidHom M i)) φ) = φ

Tactic:
by
    ext i m
    simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
      MonoidHom.finsetProd_apply, evalMonoidHom_apply, ]
    let φ' i : M i → M' := ⇑(φ i)
    conv =>
      enter [1, 2, j]
      rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]
    rw [show φ' i = φ i from rfl]
    exact Fintype.prod_pi_mulSingle' ..

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : x ∈ ⨆ i, p i
⊢ motive x hx

Tactic:
by
  refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, p i) (hc : motive x hx) => hc
  refine iSup_induction p (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_
  · exact ⟨_, mem _ _ hx⟩
  · exact ⟨_, zero⟩
  · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, add _ _ _ _ Cx Cy⟩

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
h : ∀ (b : R), b ∈ s → Commute a b
⊢ Commute a s.sum

Tactic:
induction s using Quotient.inductionOn
  rw [quot_mk_to_coe, sum_coe]
  exact Commute.list_sum_right _ _ h

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

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ b = ⊥

Tactic:
rw [← sSup_compact_le_eq b, sSup_eq_bot]

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ ∀ a ∈ {c | IsCompactElement c ∧ c ≤ b}, a = ⊥
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ∀ i ∈ s, map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i

Tactic:
intro i

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
i : ι
⊢ i ∈ s → map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = 1 * 1

Tactic:
rw [mul_one]

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

Goal state before:
pp: α : Type u_1
G : Type u_6
inst✝ : Group G
s : Set α
f : α → G
⊢ sᶜ.mulIndicator f = f * (s.mulIndicator f)⁻¹

Tactic:
mulIndicator_compl

Goal state after:
α : Type u_1
G : Type u_6
inst✝ : Group G
s : Set α
f : α → G
⊢ f * (s.mulIndicator f)⁻¹ = f * (s.mulIndicator f)⁻¹
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case refine_1
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ {x | x ∈ ⟦l₁⟧ ∧ p x}.Subsingleton = {x | x ∈ ⟦l₂⟧ ∧ p x}.Subsingleton

Tactic:
congr!
      exact congrArg _ (Quotient.sound h)

Goal state after:
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
⊢ (indicator s f).support ⊆ s

Tactic:
intro i

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ i ∈ (indicator s f).support → i ∈ s
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint f.support (single a b).support

Tactic:
rwa [H, disjoint_singleton_right]

Goal state after: