mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⊤ ↔ InfiniteDimensionalOrder α

Tactic:
by
  refine ⟨fun h ↦ ?_, fun _ ↦ krullDim_eq_top⟩
  cases isEmpty_or_nonempty α
  · simp [krullDim_eq_bot] at h
  cases finiteDimensionalOrder_or_infiniteDimensionalOrder α
  · rw [krullDim_eq_length_of_finiteDimensionalOrder] at h
    cases h
  · infer_instance

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
h : IsEmpty α
⊢ krullDim α = ⨆ a, ↑(height a)

Tactic:
krullDim_eq_bot,

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
h : IsEmpty α
⊢ ⊥ = ⨆ a, ↑(height a)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
h : IsEmpty α
⊢ krullDim α = ⨆ a, ↑(coheight a)

Tactic:
krullDim_eq_bot,

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
h : IsEmpty α
⊢ ⊥ = ⨆ a, ↑(coheight a)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ height n ≤ ↑n

Tactic:
apply height_le_coe_iff.mpr

Goal state after:
case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ ∀ y < n, height y < ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
x✝ : Fin (p.length - 1 + 1)
i : ℕ
hi : i < p.length - 1 + 1
⊢ RelSeries.head p < p.toFun ⟨i + 1, ⋯⟩

Tactic:
apply p.strictMono

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
x✝ : Fin (p.length - 1 + 1)
i : ℕ
hi : i < p.length - 1 + 1
⊢ 0 < ⟨i + 1, ⋯⟩
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : Module R P
inst✝ : Module R Q
g✝ : P →ₗ[R] Q
f✝ f g : N →ₗ[R] P
⊢ rTensor M (f + g) = rTensor M f + rTensor M g

Tactic:
by
    ext x y
    simp only [compr₂ₛₗ_apply, mk_apply, add_apply, rTensor_tmul, add_tmul]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
x✝ : n + 2 ≠ 0
a : α
⊢ a + a = a

Tactic:
add_idem

Goal state after:
α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
x✝ : n + 2 ≠ 0
a : α
⊢ a = a
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c a b : α
⊢ b + (a + a) = b + a

Tactic:
add_idem

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c a b : α
⊢ b + a = b + a
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c a b : α
⊢ a + a + b = a + b

Tactic:
add_idem

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c a b : α
⊢ a + b = a + b
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ -m * n ∈ -x * y

Tactic:
· exact mul_mem_mul (neg_mem_neg.2 hm) hn

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z

Tactic:
isCoprime_comm,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime (y * z) x ↔ IsCoprime x y ∧ IsCoprime x z
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime y x ∧ IsCoprime z x ↔ IsCoprime x y ∧ IsCoprime x z

Tactic:
isCoprime_comm,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime x y ∧ IsCoprime z x ↔ IsCoprime x y ∧ IsCoprime x z
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
⊢ IsCoprime x |y| ↔ IsCoprime x y

Tactic:
isCoprime_comm,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
⊢ IsCoprime |y| x ↔ IsCoprime x y
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case succ.succ
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : n + 1 ≠ 0 → (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)
h : n + 1 + 1 ≠ 0
⊢ (M ^ (n + 1)).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid

Tactic:
rw [ih n.succ_ne_zero]

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x

Tactic:
IsRelPrime.mul_left_iff,

Goal state after:
α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
⊢ IsRelPrime (s b) x ∧ IsRelPrime (∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0

Tactic:
rw [mul_one, mul_zero, add_zero]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ lcm x 0 = 0

Tactic:
by rw [lcm, mul_zero, zero_div]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : annihilator R M = ⊤
m m' : M
⊢ 1 • m = 1 • m'

Tactic:
simp_rw [mem_annihilator.mp (h ▸ Submodule.mem_top)]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x = y * z / t ↔ t * x = y * z

Tactic:
eq_div_iff_mul_eq_of_dvd _ _ _ h2

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ t * x = y * z ↔ t * x = y * z

R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ t ∣ y * z
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ GCDMonoid.gcd a (fold GCDMonoid.gcd 0 (s.erase a)) = GCDMonoid.gcd (normalize a) (fold GCDMonoid.gcd 0 (s.erase a))

Tactic:
apply (associated_normalize _).gcd_eq_left

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a b : ℤ
⊢ Associated a.natAbs b.natAbs ↔ a.natAbs = b.natAbs

Tactic:
exact associated_iff_eq

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case cons
ι : Type u_1
s✝ : Finset ι
f : ι → ℤ
a : ι
s : Finset ι
has : a ∉ s
ih : 0 ≤ s.gcd f
⊢ 0 ≤ GCDMonoid.gcd (f a) (s.gcd f)

Tactic:
← Int.coe_gcd

Goal state after:
case cons
ι : Type u_1
s✝ : Finset ι
f : ι → ℤ
a : ι
s : Finset ι
has : a ∉ s
ih : 0 ≤ s.gcd f
⊢ 0 ≤ ↑((f a).gcd (s.gcd f))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
⊢ I ^ n ≤ P ↔ I ≤ P

Tactic:
by
  have h : (Multiset.replicate n I).prod ≤ P ↔ _ := hP.multiset_prod_le
  simp_rw [Multiset.prod_replicate, Multiset.mem_replicate, ne_eq, hn, not_false_eq_true,
    true_and, exists_eq_left] at h
  exact h

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
h : a = 0
⊢ b ∣ a

Tactic:
rw [h]
        apply dvd_zero

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
⊢ IsPrincipal ⊥

Tactic:
apply bot_isPrincipal

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : a = 0
⊢ normalize b ∣ a

Tactic:
rw [h]
        apply dvd_zero

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
S : Submodule R N
hI : (comap f S).IsPrincipal
⊢ (Submodule.map f (comap f S)).IsPrincipal

Tactic:
exact hI.map f

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝ : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I

Tactic:
by_cases H : c.Nonempty
  · obtain ⟨K, hKmem⟩ := Set.nonempty_def.1 H
    refine ⟨sSup c, fun ⟨x, hx⟩ ↦ ?_, fun _ ↦ le_sSup⟩
    have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x
    obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem
    have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)
    exact hs hJc ⟨hsSupJ ▸ ⟨x, hx⟩⟩
  · simpa [Set.not_nonempty_iff_eq_empty.1 H, isPrincipalIdealRing_iff] using hR

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
h : Basis ι R M
⊢ finrank R M = toNat (Module.rank R M)

Tactic:
finrank

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
h : Basis ι R M
⊢ toNat (Module.rank R M) = toNat (Module.rank R M)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
L M : Matrix l m α
N : Matrix m n α
i✝ : l
j✝ : n
⊢ ((L + M) * N) i✝ j✝ = (L * N + M * N) i✝ j✝

Tactic:
apply add_dotProduct

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
⊢ I ≠ ⊤

Tactic:
← or_iff_not_imp_left

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
hp : ∀ I ∈ S, I = a ∨ I = b ∨ I.IsPrime
⊢ I ≠ ⊤
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m✝ : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x y : Matrix m✝ n α
m : m✝
⊢ ((x + y) *ᵥ v) m = (x *ᵥ v + y *ᵥ v) m

Tactic:
apply add_dotProduct

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
x✝ : m
⊢ ((A + B) *ᵥ x) x✝ = (A *ᵥ x + B *ᵥ x) x✝

Tactic:
apply add_dotProduct

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
x✝ : n
⊢ ((x + y) ᵥ* A) x✝ = (x ᵥ* A + y ᵥ* A) x✝

Tactic:
apply add_dotProduct

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
A : Type u_3
ι : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
b : Basis ι R M
h : Function.Bijective ⇑(algebraMap R A)
m : M
⊢ (algebraMapCoeffs A b h).repr m = Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
⊢ v ᵥ* 1 = v

Tactic:
ext
  rw [← diagonal_one, vecMul_diagonal, mul_one]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
inst✝ : AddZeroClass α
i : m
j : n
⊢ entryAddMonoidHom α i j =
    ((Pi.evalAddMonoidHom (fun x ↦ α) j).comp (Pi.evalAddMonoidHom (fun i ↦ n → α) i)).comp ↑ofAddEquiv.symm

Tactic:
by
  rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type u_11
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
i : m
j : n
⊢ entryLinearMap R α i j = LinearMap.proj j ∘ₗ LinearMap.proj i ∘ₗ ↑(ofLinearEquiv R).symm

Tactic:
by
  rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module S β
σᵣₛ : R →+* S
σₛᵣ : S →+* R
inst✝¹ : RingHomInvPair σᵣₛ σₛᵣ
inst✝ : RingHomInvPair σₛᵣ σᵣₛ
f : α ≃ₛₗ[σᵣₛ] β
⊢ ↑f.mapMatrix = (↑f).mapMatrix

Tactic:
by
  rfl

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

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ finrank F K * finrank K A = finrank F A

Tactic:
finrank

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ toNat (Module.rank F K) * toNat (Module.rank K A) = toNat (Module.rank F A)
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N : Type v
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type v
v : ι → N
hv : LinearIndependent R v
cnd : Module.rank R M ≤ #ι
⊢ lift.{v, v} (Module.rank R M) ≤ lift.{v, v} #ι

Tactic:
by simpa using cnd

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N : Type v
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
cnd : Module.rank R M < Module.rank R N
⊢ lift.{v, v} (Module.rank R M) < lift.{v, v} (Module.rank R N)

Tactic:
by simpa using cnd

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

Goal state before:
pp: R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
⊢ finrank S M ≤ finrank R M

Tactic:
by
  by_cases H : Module.Finite S M
  · have := Module.Finite.trans (R := R) S M
    exact finrank_top_le_finrank_of_isScalarTower R S M
  · rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
    · exact zero_le
    · rwa [← not_lt, Module.rank_lt_aleph0_iff]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ r x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ r * (x + y) ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
exact ⟨_, ⟨mul_mem_left _ _ _ hx, ⟨_, ⟨mul_mem_left _ _ _ hy, mul_add _ _ _ |>.symm⟩⟩⟩⟩

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
⊢ (linearEquivFunOnFintype R ι M) ((lof R ι M i) m) = Pi.single i m

Tactic:
by
  rfl

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ IsInternal A ↔ IsCompl (A i) (A j)

Tactic:
isInternal_submodule_iff_iSupIndep_and_iSup_eq_top,

Goal state after:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep A ∧ iSup A = ⊤ ↔ IsCompl (A i) (A j)
Module: Mathlib.Algebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : DecidableEq ι
m : ι →₀ M
i : ι
⊢ ((finsuppLEquivDirectSum R M ι) m) i = m i

Tactic:
by
  rfl

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ ∀ {x : A}, x ∈ S → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]
  exact le_sup_left

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

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
t : Submodule R A
⊢ Subalgebra.toSubmodule (adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ ↑t

Tactic:
adjoin_eq_span,

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
t : Submodule R A
⊢ span R ↑(Submonoid.closure s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ ↑t
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case mem
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
a : A
ha : a ∈ s
⊢ f a ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
| mem a ha =>

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra 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 : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT).comp (inclusion h) = f i

Tactic:
ext
  simp only [NonUnitalAlgHom.comp_apply, iSupLift_inclusion]

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

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ Subalgebra.toSubmodule (adjoin R (s ∪ t)) = Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t)

Tactic:
adjoin_eq_span,

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ span R ↑(Submonoid.closure (s ∪ t)) = Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ span R ↑(Submonoid.closure (s ∪ t)) = Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t)

Tactic:
adjoin_eq_span,

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ span R ↑(Submonoid.closure (s ∪ t)) = span R ↑(Submonoid.closure s) * Subalgebra.toSubmodule (adjoin R t)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ span R ↑(Submonoid.closure (s ∪ t)) = span R ↑(Submonoid.closure s) * Subalgebra.toSubmodule (adjoin R t)

Tactic:
adjoin_eq_span,

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ span R ↑(Submonoid.closure (s ∪ t)) = span R ↑(Submonoid.closure s) * span R ↑(Submonoid.closure t)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

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✝² : Semiring F
inst✝¹ : Module F K
inst✝ : IsScalarTower F E K
L : Submonoid K
S : Set K
h : ↑L = ↑(span F S)
⊢ toSubmodule (adjoin E ↑L) = span E S

Tactic:
adjoin_eq_span,

Goal state after:
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✝² : Semiring F
inst✝¹ : Module F K
inst✝ : IsScalarTower F E K
L : Submonoid K
S : Set K
h : ↑L = ↑(span F S)
⊢ span E ↑(closure ↑L) = span E S