mathlib-initiative/mathlib-tactics huggingface dataset:
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
H : ¬Module.Finite S M
⊢ ℵ₀ ≤ Module.rank S M

Tactic:
· rwa [← not_lt, Module.rank_lt_aleph0_iff]

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

Goal state before:
pp: R : Type u
inst✝¹¹ : Semiring R
inst✝¹⁰ : StrongRankCondition R
S : Type u_2
T : Type u_3
inst✝⁹ : Semiring S
inst✝⁸ : Semiring T
inst✝⁷ : Module R T
inst✝⁶ : Module S T
inst✝⁵ : Module R S
inst✝⁴ : IsScalarTower R S T
inst✝³ : IsScalarTower S T T
inst✝² : FaithfulSMul S T
inst✝¹ : Module.Finite S T
inst✝ : Free R S
H : ¬Module.Finite R S
⊢ ℵ₀ ≤ Module.rank R S

Tactic:
· 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 K : TwoSidedIdeal R
h1 : I ≤ K
h2 : J ≤ K
⊢ { ringCon := I.ringCon ⊔ J.ringCon } ≤ K

Tactic:
rw [ringCon_le_iff] at h1 h2 ⊢

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I.ringCon ≤ K.ringCon
h2 : J.ringCon ≤ K.ringCon
⊢ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon ≤ K.ringCon
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
⊢ ¬I = ⊥ → I = ⊤

Tactic:
← I.one_mem_iff

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
⊢ ¬I = ⊥ → 1 ∈ I
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I ≤ J
h2 : I ≤ K
⊢ I ≤ { ringCon := J.ringCon ⊓ K.ringCon }

Tactic:
rw [ringCon_le_iff] at h1 h2 ⊢

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I.ringCon ≤ J.ringCon
h2 : I.ringCon ≤ K.ringCon
⊢ I.ringCon ≤ { ringCon := J.ringCon ⊓ K.ringCon }.ringCon
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ hd.prod ∈ span R ↑(Submonoid.closure s)

Tactic:
suffices ∃ (z r : _) (_hr : r ∈ Submonoid.closure s), z • r = List.prod hd by
      rcases this with ⟨z, r, hr, hzr⟩
      rw [← hzr]
      exact smul_mem _ _ (subset_span hr)

Goal state after:
case a.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = hd.prod
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: R : Type u_11
A : Type u_12
A' : Type u_13
B : Type u_14
B' : Type u_15
C : Type u_16
C' : Type u_17
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A'
inst✝⁴ : AddCommMonoid B'
inst✝³ : AddCommMonoid C'
inst✝² : Module R A'
inst✝¹ : Module R B'
inst✝ : Module R C'
eA : A ≃ A'
eB : B ≃ B'
eC : C ≃ C'
x : A ⊗[R] B ⊗[R] C
⊢ (TensorProduct.assoc R A B C) x =
    (TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
        (TensorProduct.assoc R A' B' C' ≪≫ₗ
          TensorProduct.congr (linearEquiv R eA).symm
            (TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eC).symm)))
      x

Tactic:
induction x with
  | zero => simp
  | add => simp [*]
  | tmul x a => induction x <;> simp [*, add_tmul]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
x : M ⊗[R] N
⊢ ∃ c, (c.sum fun i n ↦ ℬ i ⊗ₜ[R] n) = x

Tactic:
by
  classical obtain ⟨c, rfl⟩ := (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.surjective x
  exact ⟨c, (TensorProduct.comm R M N).injective <| by simp [Finsupp.sum]⟩

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ Projective R (M ⊗[R₀] N)

Tactic:
fapply Projective.of_split (R := R) (M := (M ⊗[R₀] (N →₀ R₀)))

Goal state after:
case i
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ M ⊗[R₀] N →ₗ[R] M ⊗[R₀] (N →₀ R₀)

case s
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N

case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ ?s ∘ₗ ?i = LinearMap.id
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module ℚ M
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ n • a) x = (fun a ↦ n • a) y
⊢ x = y

Tactic:
simpa [← Nat.cast_smul_eq_nsmul ℚ n, *] using congr((n⁻¹ : ℚ) • $hxy)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ a * star a + star b * a + (star a * b + b * star b) = a * star a + b * star a + (a * star b + b * star b)

Tactic:
add_add_add_comm,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ a * star a + star a * b + (star b * a + b * star b) = a * star a + b * star a + (a * star b + b * star b)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
⊢ (diagonal d).toBlock p q ⟨i, hi⟩ ⟨j, hj⟩ = 0 ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
have : i ≠ j := fun heq => hpq.le_bot i ⟨hi, heq.symm ▸ hj⟩

Goal state after:
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
this : i ≠ j
⊢ (diagonal d).toBlock p q ⟨i, hi⟩ ⟨j, hj⟩ = 0 ⟨i, hi⟩ ⟨j, hj⟩
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
j' : o
hj' : j' ≠ k
⊢ (∑ x, (if h : k = j' then M k i (cast ⋯ x) else 0) * if h : j' = k' then N j' x (cast ⋯ j) else 0) = 0

Tactic:
exact Finset.sum_eq_zero fun _ _ => by rw [dif_neg hj'.symm, zero_mul]

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

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j✝ : n'
⊢ vecMulVec (vecCons x v) w 0 j✝ = vecCons (x • w) (vecMulVec v w) 0 j✝

Tactic:
simp [vecMulVec]

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

Goal state before:
pp: case refine_2
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j✝ : n'
⊢ ∀ (i : Fin m), vecMulVec (vecCons x v) w i.succ j✝ = vecCons (x • w) (vecMulVec v w) i.succ j✝

Tactic:
simp [vecMulVec]

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

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f : End A (ι → M)
i j : ι
x : A
y : M
⊢ f (Pi.single j (x • y)) i = (RingHom.id A) x • f (Pi.single j y) i

Tactic:
simp [Pi.single_smul]

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

Goal state before:
pp: case intro
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : Submodule R M
inst✝ : Finite ι
b : Basis ι R M
h : finrank R ↥N = finrank R M
val✝ : Fintype ι
bM : Basis ι R M
bN : Basis (Fin (Fintype.card ι)) R ↥N
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf : ∀ (i : Fin (Fintype.card ι)), ↑(bN i) = a i • bM (f i)
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i

Tactic:
let e : Fin (Fintype.card ι) ≃ ι :=
    Equiv.ofBijective f
      ((Fintype.bijective_iff_injective_and_card f).mpr ⟨f.injective, Fintype.card_fin _⟩)

Goal state after:
case intro
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : Submodule R M
inst✝ : Finite ι
b : Basis ι R M
h : finrank R ↥N = finrank R M
val✝ : Fintype ι
bM : Basis ι R M
bN : Basis (Fin (Fintype.card ι)) R ↥N
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf : ∀ (i : Fin (Fintype.card ι)), ↑(bN i) = a i • bM (f i)
e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective ⇑f ⋯
⊢ ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
hx : ⊤ = R ∙ 0
f : (R ⧸ (LinearMap.toSpanSingleton R (M ⧸ N) 0).ker) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) 0).quotKerEquivOfSurjective ⋯
e : (LinearMap.toSpanSingleton R (M ⧸ N) 0).ker = ⊤
⊢ Nontrivial (M ⧸ N)

Tactic:
Submodule.Quotient.nontrivial_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
hx : ⊤ = R ∙ 0
f : (R ⧸ (LinearMap.toSpanSingleton R (M ⧸ N) 0).ker) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) 0).quotKerEquivOfSurjective ⋯
e : (LinearMap.toSpanSingleton R (M ⧸ N) 0).ker = ⊤
⊢ N ≠ ⊤
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
⊢ Nontrivial (R ⧸ I)

Tactic:
Submodule.Quotient.nontrivial_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
⊢ I ≠ ⊤
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
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
⊢ NonUnitalCommRing α

Tactic:
apply e.injective.nonUnitalCommRing _

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ e 0 = 0

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x y : α), e (x + y) = e x + e y

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x : α), e (-x) = -e x

case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x y : α), e (x - y) = e x - e y

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (n : ℤ) (x : α), e (n • x) = n • e x
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case a.tmul
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✝ : A
y✝ : M
⊢ (liftBaseChange A l) (x✝ ⊗ₜ[R] y✝) ∈ Submodule.span A ↑l.range

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 [LinearMap.liftBaseChange_tmul]
      exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨_, rfl⟩)

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✝ + y✝) ∈ Submodule.span A ↑l.range
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = (Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range

Tactic:
by
  rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := B),
    ← centralizer_coe_map_includeRight_eq_center_tensorProduct R A B ⊤]
  ext
  simp [includeRight]

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

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

Tactic:
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⟩)

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e = 0

Tactic:
simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, add_neg_eq_zero]

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ (∑ x ∈ t.erase x₀, if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) = ∑ z ∈ t.erase x₀, g (z - x₀)
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

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

Tactic:
by_cases h1 : Module.rank F S = 1

Goal state after:
case pos
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : Module.rank F ↥S = 1
⊢ S = ⊥

case neg
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : ¬Module.rank F ↥S = 1
⊢ S = ⊥
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K✝ : Type u
V : Type v
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Ring K
inst✝² : IsDomain K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
x : K
hx : x ≠ 0
⊢ (x * if H : x = 0 then 0 else Classical.choose ⋯) = 1

Tactic:
rw [dif_neg hx]
    exact (Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx) :)

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

Goal state before:
pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ 1 ≤ finrank K ↥(K ∙ v)

Tactic:
Nat.succ_le_iff,

Goal state after:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ 0 < finrank K ↥(K ∙ v)
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Tactic:
rcases c.eq_empty_or_nonempty with rfl | cne
  · simp
  have hdir : DirectedOn (· ≤ ·) (domain '' c) :=
    directedOn_image.2 (hc.mono @(domain_mono.monotone))
  have P : ∀ x : ↥(sSup (domain '' c)), { p : c // (x : E) ∈ p.val.domain } := by
    rintro x
    apply Classical.indefiniteDescription
    have := (mem_sSup_of_directed (cne.image _) hdir).1 x.2
    rwa [Set.exists_mem_image, ← bex_def, SetCoe.exists'] at this
  set f : ↥(sSup (domain '' c)) → F := fun x => (P x).val.val ⟨x, (P x).property⟩
  have f_eq : ∀ (p : c) (x : ↥(sSup (domain '' c))) (y : p.1.1) (_hxy : (x : E) = y),
      f x = p.1 y := by
    intro p x y hxy
    rcases hc (P x).1.1 (P x).1.2 p.1 p.2 with ⟨q, _hqc, ⟨hxq1, hxq2⟩, ⟨hpq1, hpq2⟩⟩
    exact (hxq2 (y := ⟨y, hpq1 y.2⟩) hxy).trans (hpq2 rfl).symm
  use { toFun := f, map_add' := ?_, map_smul' := ?_ }, ?_
  · intro x y
    rcases hc (P x).1.1 (P x).1.2 (P y).1.1 (P y).1.2 with ⟨p, hpc, hpx, hpy⟩
    set x' := inclusion hpx.1 ⟨x, (P x).2⟩
    set y' := inclusion hpy.1 ⟨y, (P y).2⟩
    rw [f_eq ⟨p, hpc⟩ x x' rfl, f_eq ⟨p, hpc⟩ y y' rfl, f_eq ⟨p, hpc⟩ (x + y) (x' + y') rfl,
      map_add]
  · intro c x
    rw [f_eq (P x).1 (c • x) (c • ⟨x, (P x).2⟩) rfl, ← map_smulₛₗ]
  · intro p hpc
    refine ⟨le_sSup <| Set.mem_image_of_mem domain hpc, fun x y hxy => Eq.symm ?_⟩
    exact f_eq ⟨p, hpc⟩ _ _ hxy.symm

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

Goal state before:
pp: case mp
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
⊢ p ∣ c → a % p = (a + c) % p

pp: case mpr
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
⊢ a % p = (a + c) % p → p ∣ c

Tactic:
· simp +contextual [Nat.add_mod, Nat.dvd_iff_mod_eq_zero]

Goal state after:
case mpr
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
⊢ a % p = (a + c) % p → p ∣ c
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hc : CharP R p
hp : p = 1
⊢ 1 = 0

Tactic:
by simpa using (cast_eq_zero_iff R p 1).mpr (hp ▸ dvd_refl p)

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

Goal state before:
pp: case mp
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
this : Prime 1
⊢ False

Tactic:
exact not_prime_one this

Goal state after:
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (C x * X ^ k).coeff n = if n = k then x else 0

Tactic:
rw [C_mul_X_pow_eq_monomial, coeff_monomial]

Goal state after:
R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (if k = n then x else 0) = if n = k then x else 0