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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
r : R
x : loopAlgebra R A L
⊢ { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) (r • x)) (-a))) v, map_add' := ⋯,
      map_smul' := ⋯ } =
    (RingHom.id R) r •
      { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) x) (-a))) v, map_add' := ⋯,
        map_smul' := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup A
inst✝¹ : DistribSMul A R
inst✝ : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
r : R
x : loopAlgebra R A L
x✝¹ : A
x✝ : L
⊢ ((TensorProduct.AlgebraTensorModule.curry
            { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) (r • x)) (-a))) v,
              map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
          AddMonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((RingHom.id R) r •
              { toFun := fun g ↦ ((toFinsupp R A L) g).sum fun a v ↦ a • (Φ (((toFinsupp R A L) x) (-a))) v,
                map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
          AddMonoidAlgebra.lsingle x✝¹)
        1)
      x✝
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
⊢ x ∈ f.toCycle hf ↔ f x ≠ x

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
⊢ x ∈ f.toCycle hf → f x ≠ x

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
⊢ f x ≠ x → x ∈ f.toCycle hf
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x✝¹ : R
x✝ : L
⊢ ⟨s₁ (x✝¹ • x✝) - s₂ (x✝¹ • x✝), ⋯⟩ = x✝¹ • ⟨s₁ x✝ - s₂ x✝, ⋯⟩

Tactic:
SetLike.mk_smul_of_tower_mk,

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing M
inst✝ : LieAlgebra R M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x✝¹ : R
x✝ : L
⊢ ⟨s₁ (x✝¹ • x✝) - s₂ (x✝¹ • x✝), ⋯⟩ = ⟨x✝¹ • (s₁ x✝ - s₂ x✝), ⋯⟩
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case e_s
R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
⊢ Finset.Ico (↑i + 1) n = {x ∈ Finset.range n | ↑i < x}

Tactic:
ext

Goal state after:
case e_s
R : Type u_1
inst✝ : CommRing R
n : ℕ
i : Fin n
f : ℕ → R
a✝ : ℕ
⊢ a✝ ∈ Finset.Ico (↑i + 1) n ↔ a✝ ∈ {x ∈ Finset.range n | ↑i < x}
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: n : ℕ
i : Fin n
⊢ S 0 i = {![]}

Tactic:
ext

Goal state after:
n : ℕ
i : Fin n
a✝ : Fin 0 → Fin n
⊢ a✝ ∈ S 0 i ↔ a✝ ∈ {![]}
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: p : ℕ
⊢ S p 0 = {Fin.succ}

Tactic:
ext

Goal state after:
p : ℕ
a✝ : Fin p → Fin (p + 1)
⊢ a✝ ∈ S p 0 ↔ a✝ ∈ {Fin.succ}
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i : Fin n
hEq1 : Eq1 A p
⊢ -∑ k > i, (Spec.stepEntry A)^[p] A k k = (-1) ^ (p + 1) * ∑ k > i, ∑ α ∈ S p k, bminor A k k α

Tactic:
simp only [hEq1, Matrix.of_apply, ← Finset.mul_sum]
      ring

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² x✝¹ : Derivation R A₁ A₁
x✝ : A₁
⊢ ⁅x✝², x✝ • x✝¹⁆ = x✝ • ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆ • x✝¹

Tactic:
ext

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² x✝¹ : Derivation R A₁ A₁
x✝ a✝ : A₁
⊢ ⁅x✝², x✝ • x✝¹⁆ a✝ = (x✝ • ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆ • x✝¹) a✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ x✝ : L₁
⊢ Derivation.mk' ((LieModule.toEnd R L₁ A₁) (x✝¹ + x✝)) ⋯ =
    Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝¹) ⋯ + Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯

Tactic:
ext

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ x✝ : L₁
a✝ : A₁
⊢ (Derivation.mk' ((LieModule.toEnd R L₁ A₁) (x✝¹ + x✝)) ⋯) a✝ =
    (Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝¹) ⋯ + Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯) a✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : R
x✝ : L₁
⊢ Derivation.mk' ((LieModule.toEnd R L₁ A₁) (x✝¹ • x✝)) ⋯ =
    (RingHom.id R) x✝¹ • Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯

Tactic:
ext

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : R
x✝ : L₁
a✝ : A₁
⊢ (Derivation.mk' ((LieModule.toEnd R L₁ A₁) (x✝¹ • x✝)) ⋯) a✝ =
    ((RingHom.id R) x✝¹ • Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯) a✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ x✝ : L₁
⊢ Derivation.mk' ((LieModule.toEnd R L₁ A₁) ⁅x✝¹, x✝⁆) ⋯ =
    ⁅Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝¹) ⋯, Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯⁆

Tactic:
ext

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ x✝ : L₁
a✝ : A₁
⊢ (Derivation.mk' ((LieModule.toEnd R L₁ A₁) ⁅x✝¹, x✝⁆) ⋯) a✝ =
    ⁅Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝¹) ⋯, Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯⁆ a✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : A₁
x✝ : L₁
⊢ { toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
      (x✝¹ • x✝) =
    (AlgHom.id R A₁) x✝¹ •
      { toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
        x✝

Tactic:
ext

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : A₁
x✝ : L₁
a✝ : A₁
⊢ ({ toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
        (x✝¹ • x✝))
      a✝ =
    ((AlgHom.id R A₁) x✝¹ •
        { toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯,
            map_lie' := ⋯ }
          x✝)
      a✝
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
⊢ (A n).diag = 2

Tactic:
ext

Goal state after:
n : ℕ
x✝ : Fin n
⊢ (A n).diag x✝ = 2 x✝
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
⊢ (A n)ᵀ = A n

Tactic:
ext

Goal state after:
n : ℕ
i✝ j✝ : Fin n
⊢ (A n)ᵀ i✝ j✝ = A n i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
⊢ (B n)ᵀ = C n

Tactic:
ext

Goal state after:
n : ℕ
i✝ j✝ : Fin n
⊢ (B n)ᵀ i✝ j✝ = C n i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
⊢ (D n)ᵀ = D n

Tactic:
ext

Goal state after:
n : ℕ
i✝ j✝ : Fin n
⊢ (D n)ᵀ i✝ j✝ = D n i✝ j✝
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ↥E.solSpace
⊢ (fun x ↦ ↑(u + v) ↑x) = (fun x ↦ ↑u ↑x) + fun x ↦ ↑v ↑x

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ↥E.solSpace
x✝ : Fin E.order
⊢ ↑(u + v) ↑x✝ = ((fun x ↦ ↑u ↑x) + fun x ↦ ↑v ↑x) x✝
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
a : R
u : ↥E.solSpace
⊢ (fun x ↦ ↑(a • u) ↑x) = (RingHom.id R) a • fun x ↦ ↑u ↑x

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
a : R
u : ↥E.solSpace
x✝ : Fin E.order
⊢ ↑(a • u) ↑x✝ = ((RingHom.id R) a • fun x ↦ ↑u ↑x) x✝
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩ ↔ Set.EqOn u v ↑(range E.order)

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩ → Set.EqOn u v ↑(range E.order)

case mpr
R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ Set.EqOn u v ↑(range E.order) → E.basis.repr ⟨u, hu⟩ = E.basis.repr ⟨v, hv⟩
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) ↔ q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) → q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0

case mpr
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0 → E.IsSolution fun n ↦ q ^ n
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
α β : ↥LieSubalgebra.root
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
γ δ : ↥LieSubalgebra.root
hδ : rootSpace H ⇑↑δ ≤ LieSubmodule.restr I H
hp : ¬S.pairing δ γ = 0
hγ : rootSpace H ⇑(S.root' γ) ≤ LieSubmodule.restr I H
h_neg : S.pairing ((S.reflectionPerm γ) δ) γ ≠ 0
⊢ rootSpace H ⇑↑((S.reflectionPerm γ) δ) ≤ LieSubmodule.restr I H

Tactic:
exact I.rootSpace_le_of_apply_coroot_ne_zero hγ h_neg

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_2.inr.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
j : Fin (n + 1)
hp : Prime (c j.succ)
hp' : c j.succ ∣ r
hi : 1 < j.succ
⊢ DvdNotUnit (c j.castSucc) (c j.succ)

Tactic:
· refine Associates.dvdNotUnit_iff_lt.2 (h₁ ?_)
    simpa only [Fin.coe_eq_castSucc] using Fin.castSucc_lt_succ

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
p : FractionalIdeal S P
s : Set P
hs : s = ↑p
⊢ (↑p).copy s hs = ↑p

Tactic:
ext

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
p : FractionalIdeal S P
s : Set P
hs : s = ↑p
x✝ : P
⊢ x✝ ∈ (↑p).copy s hs ↔ x✝ ∈ ↑p
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
⊢ ↑(d ⟨c₁ 1, ⋯⟩) ^ s = ↑(d ⟨c₁ 1 ^ s, hs'⟩)

Tactic:
let c₂ : Fin (s + 1) → Associates N := fun t => d ⟨c₁ t, le_trans (hc₁''.2 ⟨t, by simp⟩) hs'⟩

Goal state after:
case neg
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
⊢ ↑(d ⟨c₁ 1, ⋯⟩) ^ s = ↑(d ⟨c₁ 1 ^ s, hs'⟩)
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
⊢ J ≤ 1 ↔ ∃ I, ↑I = J

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
⊢ J ≤ 1 → ∃ I, ↑I = J

case mpr
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
⊢ (∃ I, ↑I = J) → J ≤ 1
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case mp.refine_4
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } ↔ x ∈ J

Tactic:
constructor

Goal state after:
case mp.refine_4.mp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } → x ∈ J

case mp.refine_4.mpr
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
x : P
⊢ x ∈ J → x ∈ ↑{ carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
⊢ A.IsSimplyLaced ↔ ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
⊢ A.IsSimplyLaced → ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1

case mpr
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
⊢ (∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1) → A.IsSimplyLaced
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
⊢ I * I⁻¹ = 1 ↔ generator ↑I ≠ 0

Tactic:
constructor

Goal state after:
case mp
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
⊢ I * I⁻¹ = 1 → generator ↑I ≠ 0

case mpr
K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
⊢ generator ↑I ≠ 0 → I * I⁻¹ = 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
P' : Type u_3
inst✝⁶ : CommRing P'
inst✝⁵ : Algebra R P'
inst✝⁴ : IsLocalization S P
inst✝³ : IsLocalization S P'
P'' : Type u_5
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
inst✝ : IsLocalization S P''
I : FractionalIdeal S P
⊢ (canonicalEquiv S P' P'') ((canonicalEquiv S P P') I) = (canonicalEquiv S P P'') I

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
P' : Type u_3
inst✝⁶ : CommRing P'
inst✝⁵ : Algebra R P'
inst✝⁴ : IsLocalization S P
inst✝³ : IsLocalization S P'
P'' : Type u_5
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
inst✝ : IsLocalization S P''
I : FractionalIdeal S P
x✝ : P''
⊢ x✝ ∈ (canonicalEquiv S P' P'') ((canonicalEquiv S P P') I) ↔ x✝ ∈ (canonicalEquiv S P P'') I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : Ideal R
⊢ (canonicalEquiv S P P') ↑I = ↑I

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : Ideal R
x✝ : P'
⊢ x✝ ∈ (canonicalEquiv S P P') ↑I ↔ x✝ ∈ ↑I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
h : 0 = 1
⊢ 1 ∈ 0

Tactic:
by
        rw [← (algebraMap R₁ K).map_one]
        simpa only [h] using coe_mem_one R₁⁰ 1

Goal state after: