mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: case intro
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
val✝ : Fintype ι
⊢ v i = v i

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
⊢ (e.repr (v j) + e.repr (w j)) i = e.toMatrix v i j + e.toMatrix w i j

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
⊢ (e.repr (v j) + e.repr (w j)) i = e.toMatrix v i j + e.toMatrix w i j
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
c : R
v : ι → M
i j : ι
⊢ (c • e.repr (v j)) i = ((RingHom.id R) c • e.toMatrix v) i j

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
c : R
v : ι → M
i j : ι
⊢ (c • e.repr (v j)) i = ((RingHom.id R) c • e.toMatrix v) i j
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝¹¹ : CommRing R₂
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
S : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : Algebra R₂ S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R₂ S M₂
inst✝¹ : IsDomain R₂
inst✝ : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range ⇑b))
i✝ j✝ : ι
⊢ (b.repr ↑(v j✝)) i✝ = (b.repr ↑(v j✝)) i✝

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ x * a + y * b

Tactic:
]

Goal state after:
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ x * a + y * b
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Finite κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
this : DecidableEq κ'
⊢ f = f

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
⊢ ∃ d, f i = d ^ n

Tactic:
]

Goal state after:
ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
⊢ ∃ d, f i = d ^ n
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ s.erase j
hij : i = j
⊢ False

Tactic:
]

Goal state after:
ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ s.erase j
hij : i = j
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Finite ι
inst✝ : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
this : b₁.toMatrix ⇑b₂ * A = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)
⊢ b₁.toMatrix ⇑b₂ * A = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Finite ι
inst✝ : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
this : b₁.toMatrix ⇑b₂ * A = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)
⊢ b₁.toMatrix ⇑b₂ * A = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁴ : Fintype ι'
inst✝³ : Fintype ι
inst✝² : Finite κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ f = f

Tactic:
]

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

Goal state before:
pp: case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Finite κ
inst✝³ : Fintype ι
inst✝² : Fintype κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
val✝ : Fintype κ
⊢ (toMatrix b c) f = (toMatrix b c) f

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
hg' : (algebraMap R[X] K) g ≠ 0
⊢ (algebraMap R[X] K) f = (algebraMap R[X] K) f

Tactic:
]

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

Goal state before:
pp: case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Fintype ι'
inst✝³ : Finite κ
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val✝ : Fintype κ
this : A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)
⊢ A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)

Tactic:
]

Goal state after:
case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Fintype ι'
inst✝³ : Finite κ
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val✝ : Fintype κ
this : A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)
⊢ A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
⊢ ↑↑x ≠ 1

Tactic:
]

Goal state after:
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
⊢ ↑↑x ≠ 1
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
⊢ (b.repr (A.col j)) i = (b.repr (A.col j)) i

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ↑↑x ^ orderOf x - 1 = 0

Tactic:
]

Goal state after:
case calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ↑↑x ^ orderOf x - 1 = 0
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
⊢ ∑ g, f g = 0

Tactic:
by
  classical
    obtain ⟨x, hx⟩ := IsCyclic.exists_monoid_generator (α := MonoidHom.range f.toHomUnits)
    have hx1 : (x.1 : R) - 1 ≠ 0 := by
      rw [sub_ne_zero]
      contrapose hf
      ext g
      obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩
      simpa [hf, Subtype.ext_iff, Units.ext_iff] using hn.symm
    let c := #{g | f.toHomUnits g = 1}
    calc
      ∑ g : G, f g = ∑ u ∈ univ.image f.toHomUnits, #{g | f.toHomUnits g = u} • (u : R) :=
        sum_comp ((↑) : Rˣ → R) f.toHomUnits
      _ = ∑ u ∈ univ.image f.toHomUnits, c • (u : R) :=
        (sum_congr rfl fun u hu => congr_arg₂ _ ?_ rfl)
      -- remaining goal 1, proven below
      _ = ∑ b : MonoidHom.range f.toHomUnits, c • (b.1 : R) :=
        (Finset.sum_subtype _ (by simp) _)
      _ = c • ∑ b : MonoidHom.range f.toHomUnits, (b.1 : R) := smul_sum.symm
      _ = c • 0 := congr_arg₂ _ rfl ?_
      -- remaining goal 2, proven below
      _ = 0 := smul_zero _
    · -- remaining goal 1
      apply MonoidHom.card_fiber_eq_of_mem_range f.toHomUnits
      · simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu
      · exact ⟨1, f.toHomUnits.map_one⟩
    -- remaining goal 2
    calc
      (∑ b : MonoidHom.range f.toHomUnits, (b.1 : R))
        = ∑ n ∈ range (orderOf x), (x.1 : R) ^ n :=
        Eq.symm <|
          sum_nbij (x ^ ·) (by simp)
            (by simpa using pow_injOn_Iio_orderOf)
            (fun b _ => let ⟨n, hn⟩ := hx b
              ⟨n % orderOf x, mem_range.2 (Nat.mod_lt _ (orderOf_pos _)), by simp [hn]⟩)
            (by simp)
      _ = 0 := ?_
    rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]
    norm_cast
    simp [pow_orderOf_eq_one]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g, f g = 0

Tactic:
]

Goal state after:
case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g, f g = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ : ℕ
x₁ : Ext S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : hS.extClass.comp x₁ hn₁ = 0
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
            X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₁), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
                X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
                g := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₁), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
                  X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
                  g := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₁), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₂, (mk₀ S.f).comp x₂ ⋯ = x₁

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ : ℕ
x₁ : Ext S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : hS.extClass.comp x₁ hn₁ = 0
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
            X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₁), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
                X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
                g := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₁), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
                  X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
                  g := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₁), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₂, (mk₀ S.f).comp x₂ ⋯ = x₁
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n),
            X₃ := AddCommGrpCat.of (Ext S.X₁ Y n), f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n),
                X₃ := AddCommGrpCat.of (Ext S.X₁ Y n), f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯),
                g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n),
                  X₃ := AddCommGrpCat.of (Ext S.X₁ Y n), f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯),
                  g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = x₂

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n),
            X₃ := AddCommGrpCat.of (Ext S.X₁ Y n), f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n),
                X₃ := AddCommGrpCat.of (Ext S.X₁ Y n), f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯),
                g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n),
                  X₃ := AddCommGrpCat.of (Ext S.X₁ Y n), f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯),
                  g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = x₂
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₁ : ℕ
x₃ : Ext S.X₃ Y n₁
hx₃ : (mk₀ S.g).comp x₃ ⋯ = 0
n₀ : ℕ
hn₀ : 1 + n₀ = n₁
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext S.X₁ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₃ Y n₁),
            X₃ := AddCommGrpCat.of (Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₀),
            g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext S.X₁ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₃ Y n₁),
                X₃ := AddCommGrpCat.of (Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₀),
                g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext S.X₁ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₃ Y n₁),
                  X₃ := AddCommGrpCat.of (Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₀),
                  g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₁ : ℕ
x₃ : Ext S.X₃ Y n₁
hx₃ : (mk₀ S.g).comp x₃ ⋯ = 0
n₀ : ℕ
hn₀ : 1 + n₀ = n₁
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext S.X₁ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₃ Y n₁),
            X₃ := AddCommGrpCat.of (Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₀),
            g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext S.X₁ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₃ Y n₁),
                X₃ := AddCommGrpCat.of (Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₀),
                g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext S.X₁ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₃ Y n₁),
                  X₃ := AddCommGrpCat.of (Ext S.X₂ Y n₁), f := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₀),
                  g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
g : M ⟶ N
hg : Epi g
⊢ ∀ x ∈ ((mk₀ g).precomp L ⋯).ker, x = 0

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
g : M ⟶ N
hg : Epi g
⊢ ∀ x ∈ ((mk₀ g).precomp L ⋯).ker, x = 0
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ^ k = 1 ↔ ↑ζ ^ k = 1

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ^ k = 1 ↔ ↑ζ ^ k = 1
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝ : CommMonoid R
ζ : ↥(rootsOfUnity k R)
m : ℕ
⊢ ↑↑ζ ^ m = ↑↑ζ ^ m

Tactic:
]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ ↑σ ↑1 = ↑1

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ ↑σ ↑1 = ↑1
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝¹ : CommMonoid R
inst✝ : NeZero k
x : R
x✝ : x ∈ val '' ↑(rootsOfUnity k R)
y : Rˣ
hy1 : y ∈ ↑(rootsOfUnity k R)
hy2 : ↑y = x
⊢ ↑y ∈ {z | z ^ k = 1}

Tactic:
]

Goal state after:
R : Type u_4
k : ℕ
inst✝¹ : CommMonoid R
inst✝ : NeZero k
x : R
x✝ : x ∈ val '' ↑(rootsOfUnity k R)
y : Rˣ
hy1 : y ∈ ↑(rootsOfUnity k R)
hy2 : ↑y = x
⊢ ↑y ∈ {z | z ^ k = 1}
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx✝ : x ∈ nthRoots k 1
hx : x ^ k = 1
⊢ ↑⟨x, hx✝⟩ * ↑⟨x, hx✝⟩ ^ (k - 1) = 1

Tactic:
]

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx✝ : x ∈ nthRoots k 1
hx : x ^ k = 1
⊢ ↑⟨x, hx✝⟩ * ↑⟨x, hx✝⟩ ^ (k - 1) = 1
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx✝ : x ∈ nthRoots k 1
hx : x ^ k = 1
⊢ ↑⟨x, hx✝⟩ ^ (k - 1) * ↑⟨x, hx✝⟩ = 1

Tactic:
]

Goal state after:
case refine_2
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx✝ : x ∈ nthRoots k 1
hx : x ^ k = 1
⊢ ↑⟨x, hx✝⟩ ^ (k - 1) * ↑⟨x, hx✝⟩ = 1