harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Quiver/Symmetric.lean
theorem Path.reverse_comp [HasReverse V] {a b c : V} (p : Path a b) (q : Path b c) :
    (p.comp q).reverse = q.reverse.comp p.reverse

Proof state:
V : Type u_2
inst✝¹ : Quiver V
inst✝ : HasReverse V
a b c : V
p : Path a b
q : Path b c
⊢ (p.comp q).reverse = q.reverse.comp p.reverse

Tactic:
induction q with
| nil => simp
| cons _ _ h => simp [h]

Result:
no goals

Proof state:
case cons
V : Type u_2
inst✝¹ : Quiver V
inst✝ : HasReverse V
a b c : V
p : Path a b
b✝ c✝ : V
a✝¹ : Path b b✝
a✝ : b✝ ⟶ c✝
h : (p.comp a✝¹).reverse = a✝¹.reverse.comp p.reverse
⊢ (p.comp (a✝¹.cons a✝)).reverse = (a✝¹.cons a✝).reverse.comp p.reverse

Tactic:
simp [h]

Result:
no goals

Proof state:
case nil
V : Type u_2
inst✝¹ : Quiver V
inst✝ : HasReverse V
a b c : V
p : Path a b
⊢ (p.comp nil).reverse = nil.reverse.comp p.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_append {as : Vector α n} {bs : Vector α m} {i : Nat} :
    (as ++ bs)[i]? = if i < n then as[i]? else bs[i - n]?

Proof state:
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
⊢ (as ++ bs)[i]? = if i < n then as[i]? else bs[i - n]?

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
h : i < n
⊢ (as ++ bs)[i]? = as[i]?

case isFalse
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
h : ¬i < n
⊢ (as ++ bs)[i]? = bs[i - n]?

Proof state:
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
h : ¬i < n
⊢ n ≤ i

Tactic:
simpa using h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
h : i < n
⊢ (as ++ bs)[i]? = as[i]?

Tactic:
exact getElem?_append_left h

Result:
no goals

Proof state:
case isFalse
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
h : ¬i < n
⊢ (as ++ bs)[i]? = bs[i - n]?

Tactic:
exact getElem?_append_right (by simpa using h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k a : α}
    {v : β k} :
    (m.insertIfNew k v).getKey! a =
      if k == a ∧ m.contains k = false then k else m.getKey! a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ m.contains k = false then k else m.getKey! a

Tactic:
simp_to_model [insertIfNew] using List.getKey!_insertEntryIfNew

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extend_nhds_of_boundaryless [I.Boundaryless] {x : M} (hx : x ∈ f.source) :
    map (f.extend I) (𝓝 x) = 𝓝 (f.extend I x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
⊢ map (↑(f.extend I)) (𝓝 x) = 𝓝 (↑(f.extend I) x)

Tactic:
rw [f.map_extend_nhds hx, I.range_eq_univ, nhdsWithin_univ]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive (attr := simp)] lemma antivary_inv_left : Antivary f⁻¹ g ↔ Monovary f g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
f : ι → α
g : ι → β
⊢ Antivary f⁻¹ g ↔ Monovary f g

Tactic:
simp [Monovary, Antivary]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.reverse.map Inv.inv).prod
  | [] => by rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]
  | A::Xs => by
    rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
      mul_inv_rev, list_prod_inv_reverse Xs]

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
⊢ [].prod⁻¹ = (List.map Inv.inv [].reverse).prod

Tactic:
rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]

Result:
no goals

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
Xs : List (Matrix n n α)
⊢ (A :: Xs).prod⁻¹ = (List.map Inv.inv (A :: Xs).reverse).prod

Tactic:
rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
  mul_inv_rev, list_prod_inv_reverse Xs]

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
lemma isOpen_iff_isUpperSet_and_dirSupInaccOn [IsScott α D] :
    IsOpen s ↔ IsUpperSet s ∧ DirSupInaccOn D s

Proof state:
case intro.intro
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
h : IsUpperSet s
h' : DirSupInaccOn D s
d : Set α
d₀ : d ∈ D
d₁ : d.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
x✝ : α
d₃ : IsLUB d x✝
ha : x✝ ∈ s
b : α
hbd : b ∈ d
hbu : b ∈ s
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
exact ⟨b, hbd, Subset.trans inter_subset_left (h.Ici_subset hbu)⟩

Result:
no goals

Proof state:
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
h : IsUpperSet s
h' : DirSupInaccOn D s
d : Set α
d₀ : d ∈ D
d₁ : d.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
x✝ : α
d₃ : IsLUB d x✝
ha : x✝ ∈ s
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
obtain ⟨b, hbd, hbu⟩ := h' d₀ d₁ d₂ d₃ ha

Result:
case intro.intro
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
h : IsUpperSet s
h' : DirSupInaccOn D s
d : Set α
d₀ : d ∈ D
d₁ : d.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
x✝ : α
d₃ : IsLUB d x✝
ha : x✝ ∈ s
b : α
hbd : b ∈ d
hbu : b ∈ s
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s

Proof state:
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsUpperSet s ∧ IsOpen s ↔ IsUpperSet s ∧ DirSupInaccOn D s

Tactic:
refine and_congr_right fun h ↦
  ⟨@IsScottHausdorff.dirSupInaccOn_of_isOpen _ _ _ (scottHausdorff α D) _ _,
    fun h' d d₀ d₁ d₂ _ d₃ ha ↦ ?_⟩

Result:
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
h : IsUpperSet s
h' : DirSupInaccOn D s
d : Set α
d₀ : d ∈ D
d₁ : d.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
x✝ : α
d₃ : IsLUB d x✝
ha : x✝ ∈ s
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s

Proof state:
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsOpen s ↔ IsUpperSet s ∧ DirSupInaccOn D s

Tactic:
rw [isOpen_iff_isUpperSet_and_scottHausdorff_open (D := D)]

Result:
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsUpperSet s ∧ IsOpen s ↔ IsUpperSet s ∧ DirSupInaccOn D s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.countP_congr {l₁ l₂ : List α} (s : l₁ ~ l₂) {p p' : α → Bool}
    (hp : ∀ x ∈ l₁, p x = p' x) : l₁.countP p = l₂.countP p'

Proof state:
case nil
α : Type u_1
l₂ : List α
p p' : α → Bool
hp : ∀ (x : α), x ∈ [] → p x = p' x
⊢ countP p [] = countP p' []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
l₂ : List α
p p' : α → Bool
y : α
s : List α
hs : (∀ (x : α), x ∈ s → p x = p' x) → countP p s = countP p' s
hp : ∀ (x : α), x ∈ y :: s → p x = p' x
⊢ countP p (y :: s) = countP p' (y :: s)

Tactic:
simp only [mem_cons, forall_eq_or_imp] at hp

Result:
case cons
α : Type u_1
l₂ : List α
p p' : α → Bool
y : α
s : List α
hs : (∀ (x : α), x ∈ s → p x = p' x) → countP p s = countP p' s
hp : p y = p' y ∧ ∀ (a : α), a ∈ s → p a = p' a
⊢ countP p (y :: s) = countP p' (y :: s)

Proof state:
α : Type u_1
l₁ l₂ : List α
s : l₁ ~ l₂
p p' : α → Bool
hp : ∀ (x : α), x ∈ l₁ → p x = p' x
⊢ countP p l₁ = countP p' l₁

Tactic:
clear s

Result:
α : Type u_1
l₁ l₂ : List α
p p' : α → Bool
hp : ∀ (x : α), x ∈ l₁ → p x = p' x
⊢ countP p l₁ = countP p' l₁

Proof state:
α : Type u_1
l₁ l₂ : List α
s : l₁ ~ l₂
p p' : α → Bool
hp : ∀ (x : α), x ∈ l₁ → p x = p' x
⊢ countP p l₁ = countP p' l₂

Tactic:
rw [← s.countP_eq p']

Result:
α : Type u_1
l₁ l₂ : List α
s : l₁ ~ l₂
p p' : α → Bool
hp : ∀ (x : α), x ∈ l₁ → p x = p' x
⊢ countP p l₁ = countP p' l₁

Proof state:
case cons
α : Type u_1
l₂ : List α
p p' : α → Bool
y : α
s : List α
hs : (∀ (x : α), x ∈ s → p x = p' x) → countP p s = countP p' s
hp : p y = p' y ∧ ∀ (a : α), a ∈ s → p a = p' a
⊢ countP p (y :: s) = countP p' (y :: s)

Tactic:
simp only [countP_cons, hs hp.2, hp.1]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
p p' : α → Bool
hp : ∀ (x : α), x ∈ l₁ → p x = p' x
⊢ countP p l₁ = countP p' l₁

Tactic:
induction l₁ with
| nil => rfl
| cons y s hs =>
  simp only [mem_cons, forall_eq_or_imp] at hp
  simp only [countP_cons, hs hp.2, hp.1]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem volumeForm_map {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    [Fact (finrank ℝ F = n)] (φ : E ≃ₗᵢ[ℝ] F) (x : Fin n → F) :
    (Orientation.map (Fin n) φ.toLinearEquiv o).volumeForm x = o.volumeForm (φ.symm ∘ x)

Proof state:
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst✝ : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
he : e.toBasis.orientation = o
⊢ ((map (Fin (n + 1)) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

Tactic:
have heφ : (e.map φ).toBasis.orientation = Orientation.map (Fin n.succ) φ.toLinearEquiv o := by
  rw [← he]
  exact e.toBasis.orientation_map φ.toLinearEquiv

Result:
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst✝ : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
he : e.toBasis.orientation = o
heφ : (e.map φ).toBasis.orientation = (map (Fin n.succ) φ.toLinearEquiv) o
⊢ ((map (Fin (n + 1)) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

Proof state:
case zero
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
inst✝ : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ ((map (Fin 0) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : Fact (finrank ℝ F = n)
φ : E ≃ₗᵢ[ℝ] F
x : Fin n → F
⊢ ((map (Fin n) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

Tactic:
rcases n with - | n

Result:
case zero
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
inst✝ : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ ((map (Fin 0) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst✝ : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
⊢ ((map (Fin (n + 1)) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma quasiIso_map_iff_of_preservesRightHomology
    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂]
    [F.ReflectsIsomorphisms] :
    QuasiIso (F.mapShortComplex.map φ) ↔ QuasiIso φ

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{u_3, u_1} C
inst✝¹⁰ : Category.{u_4, u_2} D
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesRightHomologyOf S₁
inst✝¹ : F.PreservesRightHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
a✝ : IsIso γ.φH
⊢ IsIso (F.map γ.φH)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean
theorem natTrans_eq {F G : Karoubi C ⥤ D} (φ : F ⟶ G) (P : Karoubi C) :
    φ.app P = F.map (decompId_i P) ≫ φ.app P.X ≫ G.map (decompId_p P)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_5, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P

Tactic:
conv_lhs => rw [← id_comp (φ.app P), ← F.map_id]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_5, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ F.map (𝟙 P) ≫ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_5, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ F.map (𝟙 P) ≫ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P

Tactic:
congr

Result:
case e_a.e_a
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_5, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ 𝟙 P = P.decompId_i ≫ P.decompId_p

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_5, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ φ.app P = F.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ G.map P.decompId_p

Tactic:
rw [← φ.naturality, ← assoc, ← F.map_comp]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_5, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P

Proof state:
case e_a.e_a
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_5, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ 𝟙 P = P.decompId_i ≫ P.decompId_p

Tactic:
apply decompId

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem quotient_mul_add_remainder_eq_aux (p q : R[X]) : q * div p q + mod p q = p

Proof state:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
h : ¬q = 0
⊢ q * p.div q + p.mod q = p

Tactic:
conv =>
  rhs
  rw [← modByMonic_add_div p (monic_mul_leadingCoeff_inv h)]

Result:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
h : ¬q = 0
⊢ q * p.div q + p.mod q = p %ₘ (q * C q.leadingCoeff⁻¹) + q * C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))

Proof state:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
h : ¬q = 0
⊢ q * p.div q + p.mod q = p %ₘ (q * C q.leadingCoeff⁻¹) + q * C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))

Tactic:
rw [div, mod, add_comm, mul_assoc]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
⊢ q * p.div q + p.mod q = p

Tactic:
by_cases h : q = 0

Result:
case pos
R : Type u
inst✝ : Field R
p q : R[X]
h : q = 0
⊢ q * p.div q + p.mod q = p

case neg
R : Type u
inst✝ : Field R
p q : R[X]
h : ¬q = 0
⊢ q * p.div q + p.mod q = p

Proof state:
case pos
R : Type u
inst✝ : Field R
p q : R[X]
h : q = 0
⊢ q * p.div q + p.mod q = p

Tactic:
simp only [h, zero_mul, mod, modByMonic_zero, zero_add]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem extendDomain_eq_embDomain_subtype (f : Subtype P →₀ M) :
    extendDomain f = embDomain (.subtype _) f

Proof state:
case h
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a

Tactic:
by_cases h : P a

Result:
case pos
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : P a
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a

case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a

Proof state:
case pos
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : P a
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a

Tactic:
refine Eq.trans ?_ (embDomain_apply (.subtype P) f (Subtype.mk a h)).symm

Result:
case pos
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : P a
⊢ f.extendDomain a = f ⟨a, h⟩

Proof state:
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
⊢ f.extendDomain = embDomain (Embedding.subtype P) f

Tactic:
ext a

Result:
case h
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a

Proof state:
case neg.h
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ a ∉ Set.range ⇑(Embedding.subtype P)

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : P a
⊢ f.extendDomain a = f ⟨a, h⟩

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a

Tactic:
rw [embDomain_notin_range, extendDomain_toFun, dif_neg h]

Result:
case neg.h
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ a ∉ Set.range ⇑(Embedding.subtype P)
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem Monic.degree_mul (hq : Monic q) : degree (p * q) = degree p + degree q :=
  letI := Classical.decEq R
  if hp : p = 0 then by simp [hp]
  else degree_mul' <| by rwa [hq.leadingCoeff, mul_one, Ne, leadingCoeff_eq_zero]

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rwa [hq.leadingCoeff, mul_one, Ne, leadingCoeff_eq_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : p = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem wittZero_eq_zero (n : ℕ) : wittZero p n = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittZero p n = 0

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (map (Int.castRingHom ℚ)) (wittZero p n) = (map (Int.castRingHom ℚ)) 0

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (map (Int.castRingHom ℚ)) (wittZero p n) = (map (Int.castRingHom ℚ)) 0

Tactic:
simp only [wittZero, wittStructureRat, bind₁, aeval_zero', constantCoeff_xInTermsOfW, map_zero,
  map_wittStructureInt]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
theorem comp_symmCompOfNondegenerate_apply (B₁ : BilinForm K V) {B₂ : BilinForm K V}
    (b₂ : B₂.Nondegenerate) (v : V) :
    B₂ (B₁.symmCompOfNondegenerate B₂ b₂ v) = B₁ v

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ B₂ ((B₂.toDual b₂).symm (B₁ v)) = B₁ v

Tactic:
erw [LinearEquiv.apply_symm_apply (B₂.toDual b₂)]

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ B₂ ((↑(B₂.toDual b₂).symm ∘ₗ B₁) v) = B₁ v

Tactic:
simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, DFunLike.coe_fn_eq]

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ B₂ ((B₂.toDual b₂).symm (B₁ v)) = B₁ v

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) v) = B₁ v

Tactic:
rw [symmCompOfNondegenerate]

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v : V
⊢ B₂ ((↑(B₂.toDual b₂).symm ∘ₗ B₁) v) = B₁ v
-- Mathlib/Topology/Homeomorph.lean
theorem locallyConnectedSpace [i : LocallyConnectedSpace Y] (h : X ≃ₜ Y) :
    LocallyConnectedSpace X

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
x : X
⊢ (𝓝 x).HasBasis (fun s => IsOpen s ∧ h x ∈ s ∧ IsConnected s) fun x => ⇑h.symm '' x

Tactic:
rw [← h.symm_map_nhds_eq]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
x : X
⊢ (map (⇑h.symm) (𝓝 (h x))).HasBasis (fun s => IsOpen s ∧ h x ∈ s ∧ IsConnected s) fun x => ⇑h.symm '' x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
this : ∀ (x : X), (𝓝 x).HasBasis (fun s => IsOpen s ∧ h x ∈ s ∧ IsConnected s) fun x => ⇑h.symm '' x
x✝¹ : X
x✝ : Set Y
hs : IsOpen x✝ ∧ h x✝¹ ∈ x✝ ∧ IsConnected x✝
⊢ IsPreconnected (⇑h.symm '' x✝)

Tactic:
exact hs.2.2.2.image _ h.symm.continuous.continuousOn

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
this : ∀ (x : X), (𝓝 x).HasBasis (fun s => IsOpen s ∧ h x ∈ s ∧ IsConnected s) fun x => ⇑h.symm '' x
⊢ LocallyConnectedSpace X

Tactic:
refine locallyConnectedSpace_of_connected_bases _ _ this fun _ _ hs ↦ ?_

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
this : ∀ (x : X), (𝓝 x).HasBasis (fun s => IsOpen s ∧ h x ∈ s ∧ IsConnected s) fun x => ⇑h.symm '' x
x✝¹ : X
x✝ : Set Y
hs : IsOpen x✝ ∧ h x✝¹ ∈ x✝ ∧ IsConnected x✝
⊢ IsPreconnected (⇑h.symm '' x✝)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
x : X
⊢ (map (⇑h.symm) (𝓝 (h x))).HasBasis (fun s => IsOpen s ∧ h x ∈ s ∧ IsConnected s) fun x => ⇑h.symm '' x

Tactic:
exact (i.1 _).map _

Result:
no goals