mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x : OreLocalization S X
⊢ ∀ (a b : X × ↥S), a ≈ b → add' a.fst a.snd x = add' b.fst b.snd x

Tactic:
rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨sb, rb, hb, hb'⟩

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x : OreLocalization S X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • (r₂, s₂).fst = rb • (r₁, s₁).fst
hb' : ↑sb * ↑(r₂, s₂).snd = rb * ↑(r₁, s₁).snd
⊢ add' (r₁, s₁).fst (r₁, s₁).snd x = add' (r₂, s₂).fst (r₂, s₂).snd x
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ r₁ /ₒ s₁ + r₂ /ₒ s₂ + z = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + z)

Tactic:
| _ r₂ s₂
   => 

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ r₁ /ₒ s₁ + r₂ /ₒ s₂ + z = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + z)
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ z • (r₁ /ₒ s₁ + r₂ /ₒ s₂) = z • (r₁ /ₒ s₁) + z • (r₂ /ₒ s₂)

Tactic:
| _ r₂ s₂
   => 

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ z • (r₁ /ₒ s₁ + r₂ /ₒ s₂) = z • (r₁ /ₒ s₁) + z • (r₂ /ₒ s₂)
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
x y : K
hy : y ∈ Subring.closure s
z : K
hz : z ∈ Subring.closure s
x_eq : y / z = x
⊢ x⁻¹ ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}

Tactic:
exact ⟨z, hz, y, hy, x_eq ▸ (inv_div _ _).symm⟩

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₂ /ₒ s₂ + z) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + z • (r₁ /ₒ s₁)

Tactic:
| _ r₂ s₂
   => 

Goal state after:
case c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₂ /ₒ s₂ + z) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + z • (r₁ /ₒ s₁)
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
⊢ ⟨n, b'⟩ = ⟨0, Basis.empty ↥⊥⟩

Tactic:
let e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty _ : Basis (Fin 0) R (⊥ : Submodule R M))

Goal state after:
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty ↥⊥)
⊢ ⟨n, b'⟩ = ⟨0, Basis.empty ↥⊥⟩
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ IsLocalization M S

Tactic:
convert! isLocalization_of_base_ringEquiv (Submonoid.map (h : R ≃* P) M) S h.symm

Goal state after:
case e'_3
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ M = Submonoid.map h.symm (Submonoid.map (↑h) M)

case e'_6
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ inst✝¹ = ((algebraMap P S).comp h.symm.symm.toRingHom).toAlgebra
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ mk ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m

Tactic:
mk_eq_mk',

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ mk' (Localization M) ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m
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
FA : Type u_12
FB : Type u_13
inst✝⁹ : Field FA
inst✝⁸ : Field FB
inst✝⁷ : Algebra A FA
inst✝⁶ : Algebra B FB
inst✝⁵ : IsFractionRing A FA
inst✝⁴ : IsFractionRing B FB
inst✝³ : Algebra A FB
inst✝² : IsScalarTower A B FB
inst✝¹ : Algebra FA FB
inst✝ : IsScalarTower A FA FB
⊢ fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl = AlgEquiv.refl

Tactic:
by
  ext x
  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective B x
  simp

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

Goal state before:
pp: A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
g : C ≃ₐ[A] D
⊢ fieldEquivOfAlgEquiv FA FB FD (f.trans g) = (fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g)

Tactic:
by
  ext x
  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective B x
  simp

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

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
inst✝ : IsLocalization M S
x : R
y : ↥M
⊢ (algEquiv M S) (mk x y) = mk' S x y

Tactic:
mk_eq_mk',

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
⊢ (algEquiv M S) (mk' (Localization M) x y) = mk' S x y
Module: Mathlib.RingTheory.Localization.Basic

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
inst✝ : IsLocalization M S
x : R
y : ↥M
⊢ (algEquiv M S).symm (mk' S x y) = mk x y

Tactic:
mk_eq_mk',

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
⊢ (algEquiv M S).symm (mk' S x y) = mk' (Localization M) x y
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
S : Type u_4
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
M : Submonoid R
inst✝⁶ : IsLocalization M S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f✝ : A →ₐ[R] B
f : S →ₐ[R] B := f✝.comp (IsScalarTower.toAlgHom R S A)
⊢ ∀ (r : S), (↑↑f✝.toRingHom).toFun ((algebraMap S A) r) = (algebraMap S B) r

Tactic:
let g := IsScalarTower.toAlgHom R S B

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
S : Type u_4
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
M : Submonoid R
inst✝⁶ : IsLocalization M S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f✝ : A →ₐ[R] B
f : S →ₐ[R] B := f✝.comp (IsScalarTower.toAlgHom R S A)
g : S →ₐ[R] B := IsScalarTower.toAlgHom R S B
⊢ ∀ (r : S), (↑↑f✝.toRingHom).toFun ((algebraMap S A) r) = (algebraMap S B) r
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := ⋯
h✝ : Nontrivial (A ⧸ R')
x y : A
⊢ 1 ⊗ₜ[R] (x * y) = x ⊗ₜ[R] 1 * 1 ⊗ₜ[R] y

pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := ⋯
h✝ : Nontrivial (A ⧸ R')
x y : A
⊢ x ⊗ₜ[R] 1 * 1 ⊗ₜ[R] y = x ⊗ₜ[R] y

Tactic:
· simp [(isEpi_iff_forall_one_tmul_eq R A).mp]

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := ⋯
h✝ : Nontrivial (A ⧸ R')
x y : A
⊢ x ⊗ₜ[R] 1 * 1 ⊗ₜ[R] y = x ⊗ₜ[R] y
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
⊢ let add := e.add;
  let mul := e.mul;
  α ≃+* β

Tactic:
intros
  exact
    { e with
      map_add' := fun x y => by
        simp [add_def]
      map_mul' := fun x y => by
        simp [mul_def] }

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
⊢ Sort ?u.14

Tactic:
letI := Equiv.add e

Goal state after:
α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
this : Add α := e.add
⊢ Sort ?u.14
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case a.add
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ y✝ : A ⊗[R] M
a✝¹ : (liftBaseChange A l) x✝ ∈ Submodule.span A ↑l.range
a✝ : (liftBaseChange A l) y✝ ∈ Submodule.span A ↑l.range
⊢ (liftBaseChange A l) (x✝ + y✝) ∈ Submodule.span A ↑l.range

Tactic:
rw [map_add]

Goal state after:
case a.add
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ y✝ : A ⊗[R] M
a✝¹ : (liftBaseChange A l) x✝ ∈ Submodule.span A ↑l.range
a✝ : (liftBaseChange A l) y✝ ∈ Submodule.span A ↑l.range
⊢ (liftBaseChange A l) x✝ + (liftBaseChange A l) y✝ ∈ Submodule.span A ↑l.range
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
b : B
x : A ⊗[R] B
⊢ LinearMap.mulLeft R (includeRight b) = LinearMap.mulRight R (includeRight b)

Tactic:
ext xa xb

Goal state after:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
b : B
x : A ⊗[R] B
xa : A
xb : B
⊢ ((AlgebraTensorModule.curry (LinearMap.mulLeft R (includeRight b))) xa) xb =
    ((AlgebraTensorModule.curry (LinearMap.mulRight R (includeRight b))) xa) xb
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a : A
b : B
z w : A ⊗[R] B
hz : (moduleAux (z * a ⊗ₜ[R] b)) m = (moduleAux z) ((moduleAux (a ⊗ₜ[R] b)) m)
hw : (moduleAux (w * a ⊗ₜ[R] b)) m = (moduleAux w) ((moduleAux (a ⊗ₜ[R] b)) m)
⊢ (moduleAux ((z + w) * a ⊗ₜ[R] b)) m = (moduleAux (z + w)) ((moduleAux (a ⊗ₜ[R] b)) m)

Tactic:
simp only [map_add, add_mul, LinearMap.add_apply, hz, hw]

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

Goal state before:
pp: R : Type u_1
Q : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
I : Submodule R R
⊢ map (↑(TensorProduct.lid R Q)) (rTensor Q I.subtype).range = I • ⊤

Tactic:
rw [← map_top, ← Submodule.map_comp, map_top]
  refine le_antisymm ?_ fun q h ↦ Submodule.smul_induction_on h
    (fun r hr q _ ↦ ⟨⟨r, hr⟩ ⊗ₜ q, by simp⟩) (by simp +contextual [add_mem])
  rintro _ ⟨t, rfl⟩
  exact t.induction_on (by simp) (by simp +contextual [Submodule.smul_mem_smul])
    (by simp +contextual [add_mem])

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S' : Type u_4
A : Type u_5
S : Type u_6
inst✝¹³ : Semifield R
inst✝¹² : Semifield S'
inst✝¹¹ : Field S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : Module R A
inst✝⁸ : Module S' A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower S' S A
inst✝ : IsScalarTower R S A
a : A
f : S' → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f

Tactic:
simp only [quasispectrumRestricts_iff, SpectrumRestricts, Unitization.quasispectrum_inr_eq]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
⊢ ↥T →ₐ[R] B

Tactic:
let compat :
      ∀ (i j) (x : A) (hxi : x ∈ (K i : Set A)) (hxj : x ∈ (K j : Set A)),
        f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩ := by
    intro i j x hxi hxj
    rcases dir i j with ⟨k, hik, hjk⟩
    simp [hf i k hik, hf j k hjk]

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ ↥T →ₐ[R] B
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ star c * a * c

Tactic:
rw [StarOrderedRing.nonneg_iff] at ha

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c : R
⊢ 0 ≤ star c * a * c
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : 0 ≤ a
r s : R
hrs : r ≤ s
⊢ r • a ≤ s • a

Tactic:
rw [StarOrderedRing.nonneg_iff] at ha

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r s : R
hrs : r ≤ s
⊢ r • a ≤ s • a
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
⊢ LinearIndepOn R f (s ∪ t) ↔ LinearIndepOn R f s ∧ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ h.1.union_of_quotient h.2⟩

Goal state after:
case refine_1
R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
h : LinearIndepOn R f (s ∪ t)
⊢ LinearIndepOn R f s

case refine_2
R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
h : LinearIndepOn R f (s ∪ t)
⊢ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S = 0 ↔ S = ⊥

Tactic:
by
  rw [← Submodule.rank_eq_zero, ← finrank_eq_rank, ← @Nat.cast_zero Cardinal, Nat.cast_inj]

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

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K V = Module.rank K (↥W' × ↥Q')

pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W < ℵ₀

Tactic:
Module.nonempty_linearEquiv_iff_rank_eq.mp ⟨eQ'⟩

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K V = Module.rank K V

K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W < ℵ₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type u_1
inst✝ : Unique ι
h✝ : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h✝
h : (b.repr v) default ≠ 0
f : ι →₀ K
⊢ (fun w ↦ Finsupp.single default ((b.repr w) default / (b.repr v) default)) ((fun f ↦ f default • v) f) = f

Tactic:
ext
        simp only [map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same,
          RingHom.id_apply, smul_eq_mul, Pi.smul_apply]
        exact mul_div_cancel_right₀ _ h

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ Module.rank F ↥⊥ ≤ 1

pp: case refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ 1 ≤ Module.rank F ↥⊥

Tactic:
· have := lift_rank_range_le (Algebra.linearMap F E)
    rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff,
      ← Algebra.toSubmodule_bot, rank_toSubmodule] at this

Goal state after:
case refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ 1 ≤ Module.rank F ↥⊥
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: E : Type u_4
inst✝⁵ : AddCommGroup E
F : Type u_5
inst✝⁴ : AddCommGroup F
K : Type u_7
L : Type u_8
inst✝³ : DivisionRing K
inst✝² : DivisionRing L
σ : K →+* L
inst✝¹ : Module K E
inst✝ : Module L F
f : E →ₛₗ.[σ] F
x : E
y : F
hx : x ∉ f.domain
c : K
⊢ ↑(f.supSpanSingleton x y hx) ⟨c • x, ⋯⟩ = σ c • y

Tactic:
simpa [(mk_eq_zero _ _).mpr rfl] using supSpanSingleton_apply_mk f x y hx 0 (zero_mem _) c

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : Pre R X
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) x) = F (Quot.mk (Rel R X) x)

Tactic:
induction x with
      | of =>
        change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
        simp only [Function.comp_apply, ι_def]
      | ofScalar x =>
        change algebraMap _ _ x = F (algebraMap _ _ x)
        rw [AlgHom.commutes F _]
      | add a b ha hb =>
        -- Porting note: it is necessary to declare fa and fb explicitly otherwise Lean refuses
        -- to consider `Quot.mk (Rel R X) ·` as element of FreeAlgebra R X
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
        grind
      | mul a b ha hb =>
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
        grind

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ (⇑((lift R) f) ∘ ι R) x✝ = f x✝

Tactic:
rw [Function.comp_apply, ι_def, lift]

Goal state after:
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ ({ toFun := liftAux R, invFun := fun F ↦ ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f)
      (Quot.mk (Rel R X) (Pre.of x✝)) =
    f x✝