mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ comap f (map f S) = S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
by
  apply le_antisymm
  · intro x hx
    rw [mem_comap, mem_map] at hx
    obtain ⟨y, hy, hxy⟩ := hx
    replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
    rw [← Algebra.adjoin_eq S, ← Algebra.adjoin_union, ← add_sub_cancel y x]
    exact Subalgebra.add_mem _
      (Algebra.subset_adjoin <| Or.inl hy) (Algebra.subset_adjoin <| Or.inr hxy)
  · rw [← map_le, Algebra.map_sup, f.map_adjoin]
    apply le_of_eq
    rw [sup_eq_left, Algebra.adjoin_le_iff]
    exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (S.map f).zero_mem)

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
⊢ Projective R (P × Q)

Tactic:
refine .of_lifting_property'' fun f hf ↦ ?_

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ⇑f
⊢ ∃ h, f ∘ₗ h = LinearMap.id
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : DecidableEq ι
v : ι → M
⊢ ↑R (linearCombination S fun x ↦ 1 ⊗ₜ[R] v x) = lTensor S (linearCombination R v) ∘ₗ ↑(finsuppScalarRight R R S ι).symm

Tactic:
ext; simp [smul_tmul']

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1

Tactic:
← mul_one r

Goal state after:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (r * 1)) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ selfAdjoint R ↔ star x = x

Tactic:
by
  rw [← AddSubgroup.mem_carrier]
  exact Iff.rfl

Goal state after:
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
⊢ x ∈ skewAdjoint R ↔ star x = -x

Tactic:
by
  rw [← AddSubgroup.mem_carrier]
  exact Iff.rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearEquiv.baseChange R A M M 1 = 1

Tactic:
ext x
  simp [← LinearEquiv.coe_toLinearMap]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
s : ↥S
⊢ f.mk' m s = 0 ↔ ∃ s, ↑s * m = 0

Tactic:
← (f.map_units s).mul_left_inj,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
s : ↥S
⊢ f.mk' m s * f ↑s = 0 * f ↑s ↔ ∃ s, ↑s * m = 0
Module: Mathlib.Algebra.Star.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
⊢ (congr ((starLinearEquiv R).trans (starLinearEquiv R)) ((starLinearEquiv R).trans (starLinearEquiv R))) x = x

Tactic:
convert! congr($congr_refl_refl x) <;> ext <;> simp

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 : ℚ
⊢ ∃ x, z * (algebraMap ℤ ℚ) ↑x.2 = (algebraMap ℤ ℚ) x.1

Tactic:
by
    obtain ⟨⟨x1, x2⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors ℤ) z
    obtain hx2 | hx2 := lt_or_gt_of_ne (show x2.val ≠ 0 by simp)
    · exact ⟨⟨-x1, ⟨-x2.val, by simpa using hx2⟩⟩, by simpa using hx⟩
    · exact ⟨⟨x1, ⟨x2.val, hx2⟩⟩, hx⟩

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

Goal state before:
pp: case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ l.support.sup n₁
⊢ (r ^ n • l.sum fun i c ↦ c • ↑i) ∈ B'

Tactic:
Finsupp.smul_sum

Goal state after:
case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ l.support.sup n₁
⊢ (l.sum fun a b ↦ r ^ n • b • ↑a) ∈ B'
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁶ : CommSemiring E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : CommSemiring F
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F E K
L : Subalgebra F K
ι : Type u_4
bL : Basis ι F ↥L
⊢ toSubmodule L = span F (Set.range fun i ↦ ↑(bL i))

Tactic:
by
    simpa only [← L.range_val, Submodule.map_span, Submodule.map_top, ← Set.range_comp]
      using! congr_arg (Submodule.map (L.val : L →ₗ[F] K)) bL.span_eq.symm

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

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

Tactic:
by
  rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
⊢ (Algebra.TensorProduct.map f g).Finite

Tactic:
convert!
    RingHom.Finite.tensorProductMap_id (T := T') Hf |>.comp <|
      (Algebra.TensorProduct.comm _ _ _).toRingEquiv.finite |>.comp <|
        RingHom.Finite.tensorProductMap_id (T := S) Hg |>.comp <|
          (Algebra.TensorProduct.comm _ _ _).toRingEquiv.finite

Goal state after:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
⊢ (Algebra.TensorProduct.map f g).toRingHom =
    (Algebra.TensorProduct.map f (AlgHom.id R T')).comp
      ((Algebra.TensorProduct.comm R T' S).toRingEquiv.toRingHom.comp
        ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp (Algebra.TensorProduct.comm R S T).toRingEquiv.toRingHom))
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ (p * q = p ∧ q * p = p) ∧ IsSelfAdjoint (q - p) ↔ p * q = p

Tactic:
hq.isSelfAdjoint.sub hp.isSelfAdjoint,

Goal state after:
R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ (p * q = p ∧ q * p = p) ∧ True ↔ p * q = p
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✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass R S A
r : S
x y : A ⊗[R] B
⊢ (r • x) • y = r • x • y

Tactic:
change r • x * y = r • (x * y)
    induction y with
    | zero => simp [smul_zero]
    | tmul a b => induction x with
      | zero => simp [smul_zero]
      | tmul a' b' =>
        dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
      | add x y hx hy => simp [smul_add, add_mul _, *]
    | add x y hx hy => simp [smul_add, mul_add _, *]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x = 1

Tactic:
simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x : R
hx : IsQuasiregular x
⊢ IsQuasiregular (f x)

Tactic:
by
  rw [isQuasiregular_iff] at hx ⊢
  obtain ⟨y, hy₁, hy₂⟩ := hx
  exact ⟨f y, by simpa using And.intro congr(f $(hy₁)) congr(f $(hy₂))⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective ⇑φ
⊢ Function.Injective ⇑(starMap φ)

Tactic:
intro x y h
  ext
  · simpa using! congr($(h).fst)
  · exact hφ <| by simpa [algebraMap_eq_inl] using! congr($(h).snd)

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

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : PartialOrder A
inst✝⁴ : ZeroLEOneClass A
inst✝³ : Semifield 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
⊢ IsStrictlyPositive ((algebraMap 𝕜 A) c)

Tactic:
rw [Algebra.algebraMap_eq_smul_one]
  exact IsStrictlyPositive.smul hc isStrictlyPositive_one

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
hle : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
z s : R
hs : s ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + s
⊢ s ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y + z = x + z + s

Tactic:
hs.2,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
hle : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
z s : R
hs : s ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + s
⊢ s ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ x + s + z = x + z + s
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
⊢ ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
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:
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
    rw [StarOrderedRing.le_iff] at hrs ⊢
    obtain ⟨r, hr, rfl⟩ := hrs
    exact ⟨r • a, smul_mem_closure_star_mul hr ha, add_smul ..⟩

Goal state after:
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✝ : Nontrivial R
s : Submodule R M
h : 0 < Module.rank R ↥⊥
eq : s = ⊥
⊢ False

Tactic:
rank_bot

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Submodule R M
h : 0 < 0
eq : s = ⊥
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
ι : Type u_1
inst✝ : Fintype ι
b : ι → M
h : LinearIndependent R b
⊢ Fintype.card ι ≤ finrank R M

Tactic:
by
  simpa using h.cardinalMk_le_finrank

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

Goal state before:
pp: case hli.hf
R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := ⋯
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ LinearIndependent R ⇑bW

Tactic:
exact bW.linearIndependent

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

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
⊢ lift.{v, w} #{ i // V i ≠ ⊥ } ≤ lift.{w, v} (Module.rank R M)

Tactic:
set I := { i : ι // V i ≠ ⊥ }
  have hI : ∀ i : I, ∃ v ∈ V i, v ≠ (0 : M) := by
    intro i
    rw [← Submodule.ne_bot_iff]
    exact i.prop
  choose v hvV hv using hI
  have : LinearIndependent R v := (hV.comp Subtype.coe_injective).linearIndependent _ hvV hv
  exact this.cardinal_lift_le_rank

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ IsAtom (K ∙ v)

Tactic:
by
  constructor
  · rw [Submodule.ne_bot_iff]
    exact ⟨v, ⟨mem_span_singleton_self v, hv⟩⟩
  · intro T hT
    by_contra h
    apply hT.2
    change span K {v} ≤ T
    simp_rw [span_singleton_le_iff_mem, ← Ne.eq_def, Submodule.ne_bot_iff] at *
    rcases h with ⟨s, ⟨hs, hz⟩⟩
    rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩
    rcases eq_or_ne a 0 with rfl | h
    · simp only [zero_smul, ne_eq, not_true] at hz
    · rwa [T.smul_mem_iff h] at hs

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
⊢ IsAtom W ↔ ∃ v, v ≠ 0 ∧ W = K ∙ v

Tactic:
by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · obtain ⟨hbot, h⟩ := h
    rcases (Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩
    refine ⟨v, ⟨hv, ?_⟩⟩
    by_contra heq
    specialize h (span K {v})
    rw [span_singleton_eq_bot, lt_iff_le_and_ne] at h
    exact hv (h ⟨(span_singleton_le_iff_mem v W).2 hW, Ne.symm heq⟩)
  · rcases h with ⟨v, ⟨hv, rfl⟩⟩
    exact nonzero_span_atom v hv

Goal state after:
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
S : Submodule R M
h : S = ⊥
⊢ Module.rank R ↥⊥ = 0

Tactic:
rank_bot

Goal state after:
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
S : Submodule R M
h : S = ⊥
⊢ 0 = 0
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
inst✝ : FiniteDimensional K V
n : ℕ
⊢ finrank K V < n ↔ Module.rank K V < ↑n

Tactic:
by
  simp [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0 (rank_lt_aleph0 K V), finrank]

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : IsEmpty ι
hV : Module.rank K V = 0
⊢ Subsingleton V

Tactic:
obtain ⟨_, b⟩ := Module.Free.exists_basis (R := K) (M := V)

Goal state after:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : IsEmpty ι
hV : Module.rank K V = 0
fst✝ : Type v
b : Basis fst✝ K V
⊢ Subsingleton V
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ fg (⟨z₁, hz₁⟩ + ⟨z₂, hz₂⟩) = ↑f (⟨x ⟨z₁, hz₁⟩, ⋯⟩ + ⟨x ⟨z₂, hz₂⟩, ⋯⟩) + ↑g ⟨y ⟨z₁, hz₁⟩, ⋯⟩ + ↑g ⟨y ⟨z₂, hz₂⟩, ⋯⟩

Tactic:
add_assoc,

Goal state after:
case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ fg (⟨z₁, hz₁⟩ + ⟨z₂, hz₂⟩) = ↑f (⟨x ⟨z₁, hz₁⟩, ⋯⟩ + ⟨x ⟨z₂, hz₂⟩, ⋯⟩) + (↑g ⟨y ⟨z₁, hz₁⟩, ⋯⟩ + ↑g ⟨y ⟨z₂, hz₂⟩, ⋯⟩)
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ ↑⟨z₁, hz₁⟩ + x ⟨z₂, hz₂⟩ + y ⟨z₂, hz₂⟩ = z₁ + z₂

Tactic:
add_assoc,

Goal state after:
case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ ↑⟨z₁, hz₁⟩ + (x ⟨z₂, hz₂⟩ + y ⟨z₂, hz₂⟩) = z₁ + z₂
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type ?u.7
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x✝ : R
⊢ ∀ (x : FreeAlgebra A X),
    ({ toFun := fun r ↦ Quot.mk (Rel A X) (Pre.ofScalar r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ }.comp
            (algebraMap R A))
          x✝ *
        x =
      x *
        ({ toFun := fun r ↦ Quot.mk (Rel A X) (Pre.ofScalar r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ }.comp
            (algebraMap R A))
          x✝

Tactic:
by
    rintro ⟨⟩
    exact Quot.sound Rel.central_scalar

Goal state after:
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
x' : E
hx' : x' ∈ f.domain
c : K
⊢ c • x ∈ (mkSpanSingleton x y ⋯).domain

Tactic:
exact mem_span_singleton.2 ⟨c, rfl⟩

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
hab : a = a * b
⊢ b = 1

Tactic:
rw [← mul_right_inj' (Nat.ne_zero_of_lt h1), ← hab, ← hab, mul_one]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ n.minFacProp n.minFac

pp: case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ n.minFacProp n.minFac

Tactic:
· simp [n0, minFacProp]

Goal state after:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ n.minFacProp n.minFac
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ x = 0

Tactic:
exact ⟨H x, by rintro rfl; simp⟩

Goal state after: