mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
⊢ ∃ y ∈ M,
    ∃ a,
      a • y ∈ N ∧
        ∃ M' ≤ M,
          ∃ N' ≤ N,
            N' ≤ M' ∧
              (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
                    ∃ bN,
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1),
                          ∃ bM,
                            ∀ (as : Fin n' → R),
                              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))

Tactic:
have : ∃ ϕ : M →ₗ[R] R, ∀ ψ : M →ₗ[R] R, ¬ϕ.submoduleImage N < ψ.submoduleImage N := by
    obtain ⟨P, P_eq, P_max⟩ :=
      set_has_maximal_iff_noetherian.mpr (inferInstance : IsNoetherian R R) _
        (show (Set.range fun ψ : M →ₗ[R] R ↦ ψ.submoduleImage N).Nonempty from
          ⟨_, Set.mem_range.mpr ⟨0, rfl⟩⟩)
    obtain ⟨ϕ, rfl⟩ := Set.mem_range.mp P_eq
    exact ⟨ϕ, fun ψ hψ ↦ P_max _ ⟨_, rfl⟩ hψ⟩

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
⊢ ∃ y ∈ M,
    ∃ a,
      a • y ∈ N ∧
        ∃ M' ≤ M,
          ∃ N' ≤ N,
            N' ≤ M' ∧
              (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
                    ∃ bN,
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1),
                          ∃ bM,
                            ∀ (as : Fin n' → R),
                              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ LinearEquiv.baseChange R A N M e.symm = (LinearEquiv.baseChange R A M N e).symm

Tactic:
by
  ext x
  rw [LinearEquiv.eq_symm_apply]
  simp [← LinearEquiv.coe_toLinearMap, LinearEquiv.coe_baseChange,
    baseChange_eq_ltensor, ← lTensor_comp_apply]

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Mˣ
S : Set M
⊢ {p | p ∈ Submonoid.closure S ∧ Irreducible p} ⊆ S

Tactic:
refine fun x hx ↦
      Submonoid.closure_induction (s := S) (motive := fun x _ ↦ (Irreducible x → x ∈ S))
      (fun _ hx _ ↦ hx) (by simp) (fun a b _ _ ha hb h ↦ ?_) hx.1 hx.2
  obtain rfl | rfl := h.eq_one_or_eq_one <;> simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c✝ : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c✝ i
val✝ : Fintype ι
y' : O := ∑ i, c✝ i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c✝ i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
c : R
⊢ ∀ z ∈ N', c • a • y' + z = 0 → c = 0

Tactic:
z

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c✝ : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c✝ i
val✝ : Fintype ι
y' : O := ∑ i, c✝ i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c✝ i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
c : R
z : O
⊢ z ∈ N' → c • a • y' + z = 0 → c = 0
Module: Mathlib.Algebra.Field.Subfield.Defs

Goal state before:
pp: K : Type u
inst✝¹ : DivisionRing K
S : Type u_1
inst✝ : SetLike S K
h : SubfieldClass S K
x : K
s : S
q : ℚ
hx : x ∈ s
⊢ q • x ∈ s

Tactic:
by
  simpa only [Rat.smul_def] using mul_mem (ratCast_mem _ _) hx

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_1.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c✝ : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c✝ i
val✝ : Fintype ι
y' : O := ∑ i, c✝ i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c✝ i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
c : R
⊢ ∀ x ∈ N', c • y + x = 0 → c = 0

Tactic:
z

Goal state after:
case neg.intro.refine_1.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c✝ : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c✝ i
val✝ : Fintype ι
y' : O := ∑ i, c✝ i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c✝ i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
c : R
z : O
⊢ z ∈ N' → c • y + z = 0 → c = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
⊢ M.vecMulLinear.range = span R (Set.range M.row)

Tactic:
by
  let := Classical.decEq m
  simp_rw [range_eq_map, ← iSup_range_single, Submodule.map_iSup, range_eq_map, ←
    Ideal.span_singleton_one, Ideal.span, Submodule.map_span, image_image, image_singleton,
    Matrix.vecMulLinear_apply, iSup_span, range_eq_iUnion, iUnion_singleton_eq_range,
    LinearMap.single, LinearMap.coe_mk, AddHom.coe_mk, row_def]
  unfold vecMul
  simp_rw [single_dotProduct, one_mul]

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

Goal state before:
pp: K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
x : ↥f.fieldRange
⊢ f (f.rangeRestrictFieldEquiv.symm x) = ↑x

Tactic:
rw [← rangeRestrictFieldEquiv_apply_coe, RingEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
⊢ (toMatrix v₁ v₂) f *ᵥ ⇑(v₁.repr x) = ⇑(v₂.repr (f x))

Tactic:
by
  ext i
  rw [← Matrix.toLin'_apply, LinearMap.toMatrix, LinearEquiv.trans_apply, Matrix.toLin'_toMatrix',
    LinearEquiv.arrowCongr_apply, v₂.equivFun_apply]
  congr
  exact v₁.equivFun.symm_apply_apply x

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_2.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
as : Fin n' → R
⊢ (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
    ∃ as',
      ∀ (i : Fin (n' + 1)),
        ↑((Basis.mkFinConsOfLE y yN bN' N'_le_N ⋯ ⋯) i) =
          as' i • ↑((Basis.mkFinConsOfLE y' y'M bM' M'_le_M y'_ortho_M' ⋯) (Fin.castLE ⋯ i))

Tactic:
h

Goal state after:
case neg.intro.refine_2.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
as : Fin n' → R
h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))
⊢ ∃ as',
    ∀ (i : Fin (n' + 1)),
      ↑((Basis.mkFinConsOfLE y yN bN' N'_le_N ⋯ ⋯) i) =
        as' i • ↑((Basis.mkFinConsOfLE y' y'M bM' M'_le_M y'_ortho_M' ⋯) (Fin.castLE ⋯ i))
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (AlgEquiv.ofLinearEquiv (toMatrix v₁ v₁) ⋯ ⋯) id = 1

Tactic:
AlgEquiv.ofLinearEquiv_apply,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toMatrix v₁ v₁) id = 1
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ ((toLocalizationMap M S).lift hg) z * w + w' = v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v

Tactic:
rw [mul_comm, Submonoid.LocalizationMap.lift_apply, ← mul_assoc, mul_add_inv_left hg,
    mul_comm]
  rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx : z * (algebraMap ℤ ℚ) ↑(x1, x2).2 = (algebraMap ℤ ℚ) (x1, x2).1
⊢ ∃ x, z * (algebraMap ℤ ℚ) ↑x.2 = (algebraMap ℤ ℚ) x.1

Tactic:
obtain hx2 | hx2 := lt_or_gt_of_ne (show x2.val ≠ 0 by simp)

Goal state after:
case inl
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx : z * (algebraMap ℤ ℚ) ↑(x1, x2).2 = (algebraMap ℤ ℚ) (x1, x2).1
hx2 : ↑x2 < 0
⊢ ∃ x, z * (algebraMap ℤ ℚ) ↑x.2 = (algebraMap ℤ ℚ) x.1

case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx : z * (algebraMap ℤ ℚ) ↑(x1, x2).2 = (algebraMap ℤ ℚ) (x1, x2).1
hx2 : 0 < ↑x2
⊢ ∃ x, z * (algebraMap ℤ ℚ) ↑x.2 = (algebraMap ℤ ℚ) x.1
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f g : A ≃+* A
⊢ (ringEquivOfRingEquivHom A K) f = (ringEquivOfRingEquivHom A K) g → f = g

Tactic:
h

Goal state after:
A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f g : A ≃+* A
h : (ringEquivOfRingEquivHom A K) f = (ringEquivOfRingEquivHom A K) g
⊢ f = g
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
f g : B ≃ₐ[A] B
⊢ (fieldEquivOfAlgEquivHom K L) f = (fieldEquivOfAlgEquivHom K L) g → f = g

Tactic:
h

Goal state after:
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
f g : B ≃ₐ[A] B
h : (fieldEquivOfAlgEquivHom K L) f = (fieldEquivOfAlgEquivHom K L) g
⊢ f = g
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
u v : A
⊢ u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1

Tactic:
h

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
u v : A
⊢ u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1
Module: Mathlib.Algebra.Algebra.Rat

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : DivisionSemiring R
inst✝⁴ : CharZero R
inst✝³ : DivisionSemiring S
inst✝² : CharZero S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
q : ℚ≥0
a : R
⊢ f (q • a) = (RingHom.id ℚ≥0) q • f a

Tactic:
by simp [smul_def, cast_id]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : DivisionRing R
inst✝⁴ : CharZero R
inst✝³ : DivisionRing S
inst✝² : CharZero S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
q : ℚ
a : R
⊢ f (q • a) = (RingHom.id ℚ) q • f a

Tactic:
by simp [smul_def, cast_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
⊢ NonUnitalNonAssocSemiring α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
⊢ NonUnitalNonAssocSemiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
⊢ NonUnitalSemiring α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
⊢ NonUnitalSemiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
⊢ NonAssocSemiring α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
⊢ NonAssocSemiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
⊢ Semiring α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
⊢ Semiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
⊢ NonUnitalCommSemiring α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
⊢ NonUnitalCommSemiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
⊢ CommSemiring α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
⊢ CommSemiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
add : Add α := e.add
⊢ NonUnitalNonAssocRing α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
⊢ NonUnitalNonAssocRing α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := e.zero
add : Add α := e.add
⊢ NonUnitalRing α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
⊢ NonUnitalRing α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
⊢ NonAssocRing α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
mul : Mul α := e.mul
⊢ NonAssocRing α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
⊢ Ring α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
mul : Mul α := e.mul
⊢ Ring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
⊢ NonUnitalCommRing α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
⊢ NonUnitalCommRing α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
⊢ CommRing α

Tactic:
let mul := e.mul

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
⊢ CommRing α
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∈ σ a
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

Tactic:
rw [mem_iff] at h

Goal state after:
case pos
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : ¬IsUnit (↑ₐ s - a)
⊢ r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:

Tactic:
(1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
            1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]

Goal state after: