mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 2
app₀ : f.obj' 0 _proof_245 ⟶ g.obj' 0 _proof_245
app₁ : f.obj' 1 _proof_246 ⟶ g.obj' 1 _proof_246
app₂ : f.obj' 2 _proof_247 ⟶ g.obj' 2 _proof_247
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_246 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_246) _auto_266
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_247 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_247) _auto_268
⊢ 2 < 2 + 1

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297 ⟶ g.obj' 0 _proof_297
app₁ : f.obj' 1 _proof_298 ⟶ g.obj' 1 _proof_298
app₂ : f.obj' 2 _proof_299 ⟶ g.obj' 2 _proof_299
app₃ : f.obj' 3 _proof_300 ⟶ g.obj' 3 _proof_300
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_298 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_298) _auto_318
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_299 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_299) _auto_320
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_300 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_300) _auto_322
⊢ 2 < 3 + 1

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 _proof_297 ⟶ g.obj' 0 _proof_297
app₁ : f.obj' 1 _proof_298 ⟶ g.obj' 1 _proof_298
app₂ : f.obj' 2 _proof_299 ⟶ g.obj' 2 _proof_299
app₃ : f.obj' 3 _proof_300 ⟶ g.obj' 3 _proof_300
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_298 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_298) _auto_325
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_299 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_299) _auto_327
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_300 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_300) _auto_329
⊢ 3 < 3 + 1

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361 ⟶ g.obj' 0 _proof_361
app₁ : f.obj' 1 _proof_362 ⟶ g.obj' 1 _proof_362
app₂ : f.obj' 2 _proof_363 ⟶ g.obj' 2 _proof_363
app₃ : f.obj' 3 _proof_364 ⟶ g.obj' 3 _proof_364
app₄ : f.obj' 4 _proof_365 ⟶ g.obj' 4 _proof_365
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_362 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_362) _auto_387
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_363 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_363) _auto_389
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_364 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_364) _auto_391
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_365 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_365) _auto_393
⊢ 2 < 4 + 1

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361 ⟶ g.obj' 0 _proof_361
app₁ : f.obj' 1 _proof_362 ⟶ g.obj' 1 _proof_362
app₂ : f.obj' 2 _proof_363 ⟶ g.obj' 2 _proof_363
app₃ : f.obj' 3 _proof_364 ⟶ g.obj' 3 _proof_364
app₄ : f.obj' 4 _proof_365 ⟶ g.obj' 4 _proof_365
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_362 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_362) _auto_396
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_363 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_363) _auto_398
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_364 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_364) _auto_400
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_365 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_365) _auto_402
⊢ 3 < 4 + 1

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361 ⟶ g.obj' 0 _proof_361
app₁ : f.obj' 1 _proof_362 ⟶ g.obj' 1 _proof_362
app₂ : f.obj' 2 _proof_363 ⟶ g.obj' 2 _proof_363
app₃ : f.obj' 3 _proof_364 ⟶ g.obj' 3 _proof_364
app₄ : f.obj' 4 _proof_365 ⟶ g.obj' 4 _proof_365
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_362 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_362) _auto_405
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_363 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_363) _auto_407
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_364 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_364) _auto_409
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_365 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_365) _auto_411
⊢ 4 < 4 + 1

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ 0 + 1 ≤ 4

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ 1 + 1 ≤ 4

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ 2 + 1 ≤ 4

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ 3 + 1 ≤ 4

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_480
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_482
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_484
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_486
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_488
⊢ 2 < 5 + 1

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_491
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_493
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_495
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_497
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_499
⊢ 3 < 5 + 1

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_502
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_504
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_506
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_508
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_510
⊢ 4 < 5 + 1

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449 ⟶ g.obj' 0 _proof_449
app₁ : f.obj' 1 _proof_450 ⟶ g.obj' 1 _proof_450
app₂ : f.obj' 2 _proof_451 ⟶ g.obj' 2 _proof_451
app₃ : f.obj' 3 _proof_452 ⟶ g.obj' 3 _proof_452
app₄ : f.obj' 4 _proof_453 ⟶ g.obj' 4 _proof_453
app₅ : f.obj' 5 _proof_454 ⟶ g.obj' 5 _proof_454
w₀ : autoParam (f.map' 0 1 homMk₁._proof_4 _proof_450 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_4 _proof_450) _auto_513
w₁ : autoParam (f.map' 1 2 _proof_246 _proof_451 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_246 _proof_451) _auto_515
w₂ : autoParam (f.map' 2 3 _proof_299 _proof_452 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_299 _proof_452) _auto_517
w₃ : autoParam (f.map' 3 4 _proof_364 _proof_453 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_364 _proof_453) _auto_519
w₄ : autoParam (f.map' 4 5 _proof_453 _proof_454 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_453 _proof_454) _auto_521
⊢ 5 < 5 + 1

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 0 + 1 ≤ 5

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 1 + 1 ≤ 5

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 2 + 1 ≤ 5

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 3 + 1 ≤ 5

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ 4 + 1 ≤ 5

Tactic:
by valid

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
F : ComposableArrows C n
e : (i : Fin (n + 1)) → F.obj i ≅ obj i.succ
h : ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩.succ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
i : ℕ
hi : i + 1 < n + 1
⊢ i < n

Tactic:
by valid

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
⊢ Nonempty ↑I.minimalPrimes

Tactic:
obtain ⟨p, hp, -⟩ := Ideal.exists_minimalPrimes_le hle

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ Nonempty ↑I.minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
⊢ I = ⊤

Tactic:
by_contra h

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
⊢ False
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hnil : IsNilpotent f
⊢ IsNilpotent (f.restrict hf)

Tactic:
by
  obtain ⟨n, hn⟩ := hnil
  exact ⟨n, LinearMap.ext fun m ↦ by simp only [Module.End.pow_restrict n, hn,
    LinearMap.restrict_apply, LinearMap.zero_apply]; rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case neg.succ.zero
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ m < 0 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I = ⊥
⊢ P I

Tactic:
exact (hI' hI).elim

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : (algebraMap R S) a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0

Tactic:
simp only [← map_mul,
    (injective_iff_map_eq_zero' _).mp (FaithfulSMul.algebraMap_injective R S)] at H

Goal state after:
R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : a * x = 0
⊢ ∃ a ∈ M, a * x = 0
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : (mk' S rx sx + mk' S ry sy) * mk' S rz sz = 1
hrz : mk' S rz sz = z
⊢ False

Tactic:
← mk'_add,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S (rx * ↑sy + ry * ↑sx) (sx * sy) * mk' S rz sz = 1
hrz : mk' S rz sz = z
⊢ False
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ coeSubmodule S (Ideal.span {x}) = R ∙ (algebraMap R S) x

Tactic:
by
  rw [coeSubmodule_span, Set.image_singleton]

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y

Tactic:
refine (isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxz hyz ↦ ?_, fun h x y eq ↦ ?_⟩
  · simpa [mul_assoc, h hyz] using congr_arg (· * y) hxz
  have := h _ (1 - y * x + x) _ eq <| by
    rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
  rwa [right_eq_add, sub_eq_zero, eq_comm] at this

Goal state after: