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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ (∀ (a : R), ¬a ^ 2 = r) ↔ ¬∃ r_1, r = r_1 ^ 2

Tactic:
← not_exists,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ (¬∃ x, x ^ 2 = r) ↔ ¬∃ r_1, r = r_1 ^ 2
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
⊢ p - q = 0

Tactic:
apply zero_of_eval_zero

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
⊢ ∀ (x : R), eval x (p - q) = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
⊢ p.prod ≤ q.prod ↔ p ≤ q

Tactic:
by
  refine ⟨?_, prod_le_prod⟩
  rintro ⟨c, eqc⟩
  refine Multiset.le_iff_exists_add.2 ⟨factors c, unique' hq (fun x hx ↦ ?_) ?_⟩
  · obtain h | h := Multiset.mem_add.1 hx
    · exact hp x h
    · exact irreducible_of_factor _ h
  · rw [eqc, Multiset.prod_add]
    congr
    refine associated_iff_eq.mp (factors_prod fun hc => ?_).symm
    refine not_irreducible_zero (hq _ ?_)
    rw [← prod_eq_zero_iff, eqc, hc, mul_zero]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

Tactic:
dif_neg h,

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
⊢ ↑(Classical.choose ⋯).card < ↑(Classical.choose ⋯).card
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ WellFounded DvdNotUnit

Tactic:
by
    refine RelHomClass.wellFounded
      (RelHom.mk ?_ ?_ : (DvdNotUnit : α → α → Prop) →r ((· < ·) : ℕ∞ → ℕ∞ → Prop)) wellFounded_lt
    · intro a
      by_cases h : a = 0
      · exact ⊤
      exact ↑(Multiset.card (Classical.choose (pf a h)))
    rintro a b ⟨ane0, ⟨c, hc, b_eq⟩⟩
    rw [dif_neg ane0]
    by_cases h : b = 0
    · simp [h, lt_top_iff_ne_top]
    · rw [dif_neg h, Nat.cast_lt]
      have cne0 : c ≠ 0 := by
        refine mt (fun con => ?_) h
        rw [b_eq, con, mul_zero]
      calc
        Multiset.card (Classical.choose (pf a ane0)) <
            _ + Multiset.card (Classical.choose (pf c cne0)) :=
          lt_add_of_pos_right _
            (Multiset.card_pos.mpr fun con => hc (associated_one_iff_isUnit.mp ?_))
        _ = Multiset.card (Classical.choose (pf a ane0) + Classical.choose (pf c cne0)) :=
          (Multiset.card_add _ _).symm
        _ = Multiset.card (Classical.choose (pf b h)) :=
          Multiset.card_eq_card_of_rel
          (prime_factors_unique ?_ (Classical.choose_spec (pf _ h)).1 ?_)
      · convert! (Classical.choose_spec (pf c cne0)).2.symm
        rw [con, Multiset.prod_zero]
      · intro x hadd
        rw [Multiset.mem_add] at hadd
        rcases hadd with h | h <;> apply (Classical.choose_spec (pf _ _)).1 _ h <;> assumption
      · rw [Multiset.prod_add]
        trans a * c
        · apply Associated.mul_mul <;> apply (Classical.choose_spec (pf _ _)).2 <;> assumption
        · rw [← b_eq]
          apply (Classical.choose_spec (pf _ _)).2.symm; assumption

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ ↑((-p).aroots S).toFinset = p.rootSet S

Tactic:
aroots_neg,

Goal state after:
T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ ↑(p.aroots S).toFinset = p.rootSet S
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
G : Type u_1
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G R
inst✝ : SMulCommClass G S R
f : S[X]
g : G
hg : IsUnit g
x : R
⊢ g • x ∈ f.rootSet R ↔ x ∈ f.rootSet R

Tactic:
refine ⟨?_, smul_mem_rootSet g⟩
  obtain ⟨g, rfl⟩ := hg
  exact fun hx ↦ inv_smul_smul g x ▸ smul_mem_rootSet _ hx

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

Goal state before:
pp: R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
⊢ eval₂ ϕ α g = 0

Tactic:
by
  obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_right f g
  rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ 1 / (↑u).coeff 0 = (↑u⁻¹).coeff 0

pp: case neg
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : ¬n = 0
⊢ 1 / 0 = 0

Tactic:
· rw [div_eq_iff_mul_eq (coeff_coe_units_zero_ne_zero u), coeff_zero_eq_eval_zero,
        coeff_zero_eq_eval_zero, ← eval_mul, ← Units.val_mul, inv_mul_cancel]
    simp

Goal state after:
case neg
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : ¬n = 0
⊢ 1 / 0 = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart

Tactic:
by
  constructor
  · rintro ⟨r, rfl⟩
    rw [(associated_content_mul ..).dvd_iff_dvd_right,
      p.isPrimitive_primPart.dvd_primPart_iff_dvd hq]
    exact ⟨dvd_mul_right .., dvd_mul_of_dvd_left p.primPart_dvd _⟩
  · rintro ⟨h₁, h₂⟩
    rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]
    gcongr

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
⊢ X - C a ∣ derivative f

Tactic:
have ⟨u,hu⟩ := hf

Goal state after:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ derivative f
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)
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
⊢ p.count (Associates.mk a0 * b).factors = p.count (Associates.mk a0).factors + p.count b.factors

Tactic:
obtain ⟨b0, nzb, rfl⟩ := exists_non_zero_rep hb

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
b0 : α
nzb : b0 ≠ 0
hb : Associates.mk b0 ≠ 0
⊢ p.count (Associates.mk a0 * Associates.mk b0).factors =
    p.count (Associates.mk a0).factors + p.count (Associates.mk b0).factors
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ q.leadingCoeff⁻¹ ≠ 0

Tactic:
simpa using hq

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ R⁰
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
h : (p.comp f).coeff (p.natDegree * f.natDegree) = 0
⊢ p = 0

Tactic:
rwa [coeff_comp_degree_mul_degree hf,
      mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
      leadingCoeff_eq_zero] at h

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : Transcendental R ((Polynomial.aeval r) f)
⊢ Transcendental R f

Tactic:
by
  rw [transcendental_iff] at H ⊢
  intro p hp
  exact H p (by rw [← aeval_comp, comp_eq_aeval, hp, map_zero])

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case refine_1.inl
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i : ↑s
j : ι
nmax : ¬IsMax j
ih : ∀ (h : j ∈ s), e₁ ⟨j, h⟩ = e₂ ⟨j, h⟩
hi : j⁺ ∈ s
x : F ↑⟨j⁺, hi⟩
hj : j ∈ Iio ↑⟨j⁺, hi⟩
⊢ (e₁ ⟨j⁺, hi⟩) x ⟨j, hj⟩ = (e₂ ⟨j⁺, hi⟩) x ⟨j, hj⟩

pp: case refine_1.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i✝ : ↑s
i : ι
nmax : ¬IsMax i
ih : ∀ (h : i ∈ s), e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩
hi : i⁺ ∈ s
x : F ↑⟨i⁺, hi⟩
j : ι
hj✝ : j ∈ Iio ↑⟨i⁺, hi⟩
hj : j < i
⊢ (e₁ ⟨i⁺, hi⟩) x ⟨j, hj✝⟩ = (e₂ ⟨i⁺, hi⟩) x ⟨j, hj✝⟩

Tactic:
· exact (compat₁ _ nmax x).trans (compat₂ _ nmax x).symm

Goal state after:
case refine_1.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i✝ : ↑s
i : ι
nmax : ¬IsMax i
ih : ∀ (h : i ∈ s), e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩
hi : i⁺ ∈ s
x : F ↑⟨i⁺, hi⟩
j : ι
hj✝ : j ∈ Iio ↑⟨i⁺, hi⟩
hj : j < i
⊢ (e₁ ⟨i⁺, hi⟩) x ⟨j, hj✝⟩ = (e₂ ⟨i⁺, hi⟩) x ⟨j, hj✝⟩
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ (lTensor Q g).ker = (lTensor Q f).range

Tactic:
← Submodule.ker_mkQ (p := range (lTensor Q f)),

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ (lTensor Q g).ker = (lTensor Q f).range.mkQ.ker
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_4.tmul.add
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x✝ : A ⊗[R] B
hx✝ : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
a : A
b : B
x y : ↥(Submodule.restrictScalars R I) ⊗[R] B
hx :
  ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
hy :
  ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y
⊢ ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x + y)

Tactic:
obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']

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

Goal state before:
pp: case a.refine_4.tmul.add
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx✝ : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
a : A
b : B
x y : A ⊗[R] ↥(Submodule.restrictScalars R I)
hx :
  ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
hy :
  ∃ y_1,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y
⊢ ∃ y_1,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x + y)

Tactic:
obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']

Goal state after:
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✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
exact1 : Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
rw [show g = ι.comp π from rfl, lTensor_comp]
    exact exact1.comp_injective _ (lTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)

Goal state after:
Module: Mathlib.Algebra.Azumaya.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ (mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n = LinearMap.id

Tactic:
by
  ext f : 1
  apply (Matrix.stdBasis _ _ _).ext
  intro ⟨i, j⟩
  simp only [LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, map_sum,
    map_smul, stdBasis_eq_single, LinearMap.coe_sum, Finset.sum_apply,
    LinearMap.smul_apply, LinearMap.id_coe, id_eq]
  ext k l
  simp [sum_apply, Matrix.mul_apply, single, Fintype.sum_prod_type, ite_and]

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

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f g : ι → G
⊢ balance (f - g) = balance f - balance g

Tactic:
simp only [balance, expect_sub_distrib, const_sub, sub_sub_sub_comm, Pi.sub_apply]

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

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [MOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α)) l)).prod ≡ (Multiset.map g (Quot.mk (⇑(List.isSetoid α)) l)).prod [MOD
    n]

Tactic:
simpa using listProd_map (l := l) h

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

Goal state before:
pp: case mk
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α)) l)).prod ≡ (Multiset.map g (Quot.mk (⇑(List.isSetoid α)) l)).prod [ZMOD
    n]

Tactic:
simpa using listProd_map (l := l) h

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
| f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i +
    (∑ x ∈ Ico m (n - 1), f x • ∑ i ∈ range (x + 1), g i - ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i)

Tactic:
← sum_sub_distrib

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
| f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i +
    ∑ x ∈ Ico m (n - 1), (f x • ∑ i ∈ range (x + 1), g i - f (x + 1) • ∑ i ∈ range (x + 1), g i)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ b ∈ xs

Tactic:
rw [Sym2.eq_swap] at h
  exact left_mem_of_mk_mem_sym2 h

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

Goal state before:
pp: α : Type u_1
xs ys : List α
h : xs <+ ys
⊢ xs.sym2 <+ ys.sym2

Tactic:
induction h with
  | slnil => apply slnil
  | cons a h ih =>
    simp only [List.sym2]
    exact Sublist.append (nil_sublist _) ih
  | cons_cons a h ih =>
    simp only [List.sym2, map_cons, cons_append]
    exact cons_cons _ (append (Sublist.map _ h) ih)

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
x : M
⊢ (↑ULift.moduleEquiv.symm (f'' (↑ULift.moduleEquiv (↑ULift.moduleEquiv.symm (((mk R S M) 1) x))))).down =
    (↑ULift.moduleEquiv.symm (f x)).down

Tactic:
apply one_smul

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

Goal state before:
pp: α : Type u_1
x y z : α × α
a : Rel α x y
b : Rel α y z
⊢ Rel α x z

Tactic:
by
  aesop (rule_sets := [Sym2])

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

Goal state before:
pp: α : Type u_1
p q : α × α
⊢ Rel α p q ↔ p = q ∨ p = q.swap

Tactic:
by
  aesop (rule_sets := [Sym2])

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'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
⊢ f = g

Tactic:
by
  ext x
  refine H.1.inductionOn x _ ?_ ?_ ?_ ?_
  · simp only [map_zero]
  · exact AlgHom.congr_fun h₁
  · intro s s' e
    rw [Algebra.smul_def, map_mul, map_mul, e]
    congr 1
    exact (AlgHom.congr_fun h₂ s :)
  · intro s₁ s₂ e₁ e₂
    rw [map_add, map_add, e₁, e₂]

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

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
inst✝ : P.Is X
⊢ P X

Tactic:
by rwa [← P.is_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 (Opposite.unop (G.obj X))

Tactic:
by
  rw [← unop_comp, inv_hom_id_app, unop_id]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 (Opposite.unop (F.obj X))

Tactic:
by
  rw [← unop_comp, hom_inv_id_app, unop_id]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ Arrow.mk (f i) ∈ (ofHoms f).toSet

Tactic:
arrow_mk_mem_toSet_iff

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f (f i)
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
h : Epi (f ≫ g)
⊢ Epi f

Tactic:
simpa using (inferInstance : Epi ((f ≫ g) ≫ inv g))

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
by
  simp [← ofHom_mono_iff_injective]

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 : CoreHomEquivUnitCounit F G
Y : D
⊢ adj.counit.app Y = (adj.homEquiv (G.obj Y) Y).symm (𝟙 (G.obj Y))

Tactic:
adj.homEquiv_counit

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquivUnitCounit F G
Y : D
⊢ adj.counit.app Y = F.map (𝟙 (G.obj Y)) ≫ adj.counit.app Y