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

Goal state before:
pp: R A : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ #{ x // IsAlgebraic R x } ≤ #R[X] * ℵ₀

Tactic:
by
  rw [← lift_id #_, ← lift_id #R[X]]
  exact cardinalMk_lift_le_mul R A

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
⊢ q.count a.factors = q.count (p ^ p.count a.factors).factors

Tactic:
rw [count_pow hp.ne_zero hq]

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
⊢ q.count a.factors = p.count a.factors * q.count p.factors
Module: Mathlib.Algebra.Central.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
x : D
⊢ x ∈ Subalgebra.center k D → x ∈ ⊥

Tactic:
simp only [center_eq_bot, mem_bot, Set.mem_range, forall_exists_index]
      rintro x rfl
      exact ⟨algebraMap k K x, by simp [algebraMap_eq_smul_one, smul_assoc]⟩

Goal state after:
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), a * ↑(f ≪≫ₗ g.symm) = ↑(f ≪≫ₗ g.symm) * a) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
← Subalgebra.mem_center_iff (R := S),

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ ↑(f ≪≫ₗ g.symm) ∈ Subalgebra.center S (End R M) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∃ y, y • 1 = ↑g.symm ∘ₗ ↑f) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
eq_toLinearMap_symm_comp,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∃ y, ↑g ∘ₗ (y • 1) = ↑f) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
⊢ ∃ t ∈ R[s], ∃ r, r ≠ 0 ∧ s * t = (algebraMap R S) r

Tactic:
have ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
⊢ ∃ t ∈ R[s], ∃ r, r ≠ 0 ∧ s * t = (algebraMap R S) r
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
A : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
s : S
eq : (algebraMap S A) s = 0
ne✝ : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S) r
⊢ 0 ∣ (algebraMap R A) r

Tactic:
← eq,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
A : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
s : S
eq : (algebraMap S A) s = 0
ne✝ : ¬s = 0
r : R
ne : r ≠ 0
dvd : s ∣ (algebraMap R S) r
⊢ (algebraMap S A) s ∣ (algebraMap R A) r
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ g.rangeRestrict.range = ⊤

Tactic:
range_rangeRestrict

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ ⊤ = ⊤
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∃ S, x + y = S.sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
use Sx + Sy

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n ↦ m ⊗ₜ[R] n
⊢ x + y = (Sx + Sy).sum fun m n ↦ m ⊗ₜ[R] n
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝⁴ : Type u
x✝³ : AddCommMonoid x✝⁴
x✝² : Module R x✝⁴
x✝¹ : Module.Finite R x✝⁴
I : Submodule R x✝⁴
x✝ : I.FG
⊢ Injective ⇑(rTensor R I.subtype)

Tactic:
rw [← (TensorProduct.rid R I).symm.injective_comp, ← (TensorProduct.rid R _).comp_injective]

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝⁴ : Type u
x✝³ : AddCommMonoid x✝⁴
x✝² : Module R x✝⁴
x✝¹ : Module.Finite R x✝⁴
I : Submodule R x✝⁴
x✝ : I.FG
⊢ Injective
    (⇑(TensorProduct.rid R x✝⁴).toAddEquiv.toEquiv ∘
      ⇑(rTensor R I.subtype) ∘ ⇑(TensorProduct.rid R ↥I).symm.toAddEquiv.toEquiv)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ x ∈ Set.range ⇑0

Tactic:
by
    simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]
    exact (f.map_eq_zero_iff hf).trans eq_comm

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝⟩⟧ ^ 0 = 1

Tactic:
by
    simp_rw [HPow.hPow, Pow.pow, map_def, zpow_zero, one_def i]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Goal state before:
pp: ι : Type u_1
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → β
⊢ ∏ i ∈ s, (↑t).mulIndicator f i = ∏ i ∈ s ∩ t, f i

Tactic:
← filter_mem_eq_inter,

Goal state after:
ι : Type u_1
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → β
⊢ ∏ i ∈ s, (↑t).mulIndicator f i = ∏ i ∈ s with i ∈ t, f i
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝⟩⟧ ^ 0 = 1

Tactic:
by
    simp_rw [HPow.hPow, Pow.pow, map_def, zpow_zero, one_def i]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Field

Goal state before:
pp: ι : Type u_1
K : Type u_2
inst✝ : DivisionSemiring K
s : Finset ι
f : ι → K
a : K
⊢ (∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a

Tactic:
by simp only [div_eq_mul_inv, sum_mul]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f₁ f₂ g₁ g₂ : ι → M
⊢ 𝔼 i ∈ s, (f₁ i + f₂ i) + 𝔼 i ∈ s, (g₁ i + g₂ i) = 𝔼 i ∈ s, (f₁ i + g₁ i) + 𝔼 i ∈ s, (f₂ i + g₂ i)

Tactic:
simp_rw [expect_add_distrib, add_add_add_comm]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ ((∏ m ∈ range (N + 1), f ↑m) * f (↑N + 1)) ^ 2 / f 0 = ((∏ x ∈ range (N + 1), f ↑x) * f ↑(N + 1)) ^ 2 / f 0

Tactic:
Nat.cast_succ

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ ((∏ m ∈ range (N + 1), f ↑m) * f (↑N + 1)) ^ 2 / f 0 = ((∏ x ∈ range (N + 1), f ↑x) * f (↑N + 1)) ^ 2 / f 0
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
r : S
x : S ⊗[R] M
⊢ ∀ (x : S) (y : M), (IsTensorProduct.equiv h) (r • x ⊗ₜ[R] y) = r • (IsTensorProduct.equiv h) (x ⊗ₜ[R] y)

Tactic:
intro x y

Goal state after:
case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
r : S
x✝ : S ⊗[R] M
x : S
y : M
⊢ (IsTensorProduct.equiv h) (r • x ⊗ₜ[R] y) = r • (IsTensorProduct.equiv h) (x ⊗ₜ[R] y)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x
⊢ ∀ (x : S) (y : M),
    (LinearEquiv.restrictScalars R e) (x ⊗ₜ[R] y) = ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) x) y

Tactic:
intro x y

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x
x : S
y : M
⊢ (LinearEquiv.restrictScalars R e) (x ⊗ₜ[R] y) = ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) x) y
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.head
α : Type u_1
x : α
xs : List α
ih : x ∈ xs → map (fun y ↦ s(x, y)) xs <+ xs.sym2
⊢ s(x, x) :: map (fun y ↦ s(x, y)) xs <+ s(x, x) :: (map (fun y ↦ s(x, y)) xs ++ xs.sym2)

Tactic:
exact (sublist_append_left _ _).cons_cons _

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
P : Type u_2
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
A : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra S A
inst✝⁵ : IsScalarTower R S A
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module A N
inst✝¹ : IsScalarTower S A N
inst✝ : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (AlgebraTensorModule.assoc R S A A M P).symm ≪≫ₗ AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P)
x : M ⊗[R] P
⊢ e (1 ⊗ₜ[S] x) = (AlgebraTensorModule.map f LinearMap.id) x

Tactic:
induction x with
  | zero => simp
  | tmul => simp [e, IsBaseChange.equiv_tmul]
  | add _ _ h1 h2 => simp [tmul_add, h1, h2]

Goal state after:
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: α : Type ?u.3
inst✝ : LinearOrder α
a b : α
⊢ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = a ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = b ∨
    (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = b ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = a

Tactic:
by
    cases le_total a b with
    | inl h => simp [h]
    | inr h => simp [h]

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ List.sym (n + 1) (a :: l₁✝) <+ List.sym (n + 1) (a :: l₂✝)

Tactic:
rw [List.sym, List.sym]
    apply Sublist.append
    · exact ((cons_cons a h).sym n).map _
    · exact h.sym (n + 1)

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝¹⁰ : CommSemiring R'
inst✝⁹ : CommSemiring S'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra R' S'
inst✝⁵ : Algebra R S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsScalarTower R S S'
inst✝² : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H : ∀ (x : S) (y : R'), f x * g y = g y * f x
x : R'
⊢ (pushoutDesc S' f g H) ((algebraMap R' S') x) = g x

Tactic:
simp [Algebra.pushoutDesc_apply, Algebra.IsPushout.equiv_symm_algebraMap_right]

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ f True ∨ f False

Tactic:
by refine (em p).imp ?_ ?_ <;> intro H <;> convert! h <;> simp [H]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f : Arrow T
⊢ mk f.hom = f

Tactic:
by
  cases f
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ P.isoClosure.map F = P.map F

Tactic:
by
  apply le_antisymm
  · rw [map_eq_isoClosure, map_eq_isoClosure, isoClosure_le_iff]
    exact isoClosure_strictMap_le _ _
  · exact monotone_map _ (le_isoClosure P)

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    ((map α β).obj
          { left := F₁.objPreimage X.left, right := F₂.objPreimage X.right,
            hom :=
              F.preimage
                ((inv α).app (F₁.objPreimage X.left) ≫
                  L'.map (F₁.objObjPreimageIso X.left).hom ≫
                    X.hom ≫ R'.map (F₂.objObjPreimageIso X.right).inv ≫ (inv β).app (F₂.objPreimage X.right)) }).hom ≫
      R'.map (F₂.objObjPreimageIso X.right).hom

Tactic:
dsimp
            simp only [NatIso.isIso_inv_app, Functor.comp_obj, Functor.map_preimage, assoc,
              IsIso.inv_hom_id, comp_id, IsIso.hom_inv_id_assoc]
            rw [← R'.map_comp, Iso.inv_hom_id, R'.map_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
⊢ (mkOfHomEquiv adj).homEquiv = adj.homEquiv

Tactic:
by
  ext X Y g
  simp [mkOfHomEquiv, ← adj.homEquiv_naturality_right (𝟙 _) g]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ (e X' Y).symm (f ≫ g) = (leftAdjointOfEquiv e he).map f ≫ (e X Y).symm g

Tactic:
by
        have {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
            (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g := by
          rw [Equiv.symm_apply_eq, he]; simp
        simp [← this, ← he]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom

Tactic:
← whiskerLeft_iff,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 a ◁ (λ_ f).hom ▷ g = 𝟙 a ◁ ((α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom)
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
⊢ (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom

Tactic:
← whiskerLeft_iff,

Goal state after:
B : Type u
inst✝ : Bicategory B
a : B
⊢ 𝟙 a ◁ (λ_ (𝟙 a)).hom = 𝟙 a ◁ (ρ_ (𝟙 a)).hom
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ uliftCoyonedaEquiv (uliftCoyoneda.{w, v₁, u₁}.map f) = { down := f.unop }

Tactic:
simp [uliftCoyonedaEquiv, uliftYoneda]

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
⊢ x ⟶ y

Tactic:
have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert! h.unit.app x
      have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert! h.unitInv.app y
      exact hx ≫ hy

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : J
hX : IsTerminal X
⊢ IsIso (c.ι.app X)

Tactic:
change IsIso (coconePointUniqueUpToIso (colimitOfDiagramTerminal hX F) hc).hom

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : J
hX : IsTerminal X
⊢ IsIso ((colimitOfDiagramTerminal hX F).coconePointUniqueUpToIso hc).hom
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F✝ : J ⥤ C
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
j : J
⊢ (adj.homEquiv s.pt F) s.π ≫ (coneOfAdj adj F).π.app j = s.π.app j

Tactic:
have eq := NatTrans.congr_app (adj.counit.naturality s.π) j
    have eq' := NatTrans.congr_app (adj.left_triangle_components s.pt) j
    dsimp at eq eq' ⊢
    rw [adj.homEquiv_unit, assoc, eq, reassoc_of% eq']

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X Y : C
s : BinaryCofan X Y
⊢ inr ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone s)) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone s)).pt).hom =
    (map F s).inr

Tactic:
simp [inr]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan X Y
hc : IsLimit c
s : BinaryCofan (op X) (op Y)
m : op (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }) ⟶ s.pt
h₁ : c.fst.op ≫ m = s.inl
h₂ : c.snd.op ≫ m = s.inr
⊢ m.unop ≫ c.snd = (hc.lift s.unop).op.unop ≫ c.snd

Tactic:
by simp [← h₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan X Y
hc : IsColimit c
s : BinaryFan (op X) (op Y)
m : s.pt ⟶ op (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })
h₁ : m ≫ c.inl.op = s.fst
h₂ : m ≫ c.inr.op = s.snd
⊢ c.inr ≫ m.unop = c.inr ≫ (hc.desc s.unop).op.unop

Tactic:
by simp [← h₂]

Goal state after: