harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_eq_cons_iff : range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1)

Proof state:
case succ
xs : List Nat
n s : Nat
ih : ∀ {s_1 : Nat}, range' s_1 n = s :: xs ↔ s_1 = s ∧ 0 < n ∧ xs = range' (s + 1) (n - 1)
⊢ range' (s + 1) n = xs ↔ 0 < n + 1 ∧ xs = range' (s + 1) (n + 1 - 1)

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
case zero
a : Nat
xs : List Nat
s : Nat
⊢ range' s 0 = a :: xs ↔ s = a ∧ 0 < 0 ∧ xs = range' (a + 1) (0 - 1)

Tactic:
simp

Result:
no goals

Proof state:
case succ
a : Nat
xs : List Nat
n : Nat
ih : ∀ {s : Nat}, range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1)
s : Nat
⊢ s = a → (range' (s + 1) n = xs ↔ 0 < n + 1 ∧ xs = range' (a + 1) (n + 1 - 1))

Tactic:
rintro rfl

Result:
case succ
xs : List Nat
n s : Nat
ih : ∀ {s_1 : Nat}, range' s_1 n = s :: xs ↔ s_1 = s ∧ 0 < n ∧ xs = range' (s + 1) (n - 1)
⊢ range' (s + 1) n = xs ↔ 0 < n + 1 ∧ xs = range' (s + 1) (n + 1 - 1)

Proof state:
case succ
a : Nat
xs : List Nat
n : Nat
ih : ∀ {s : Nat}, range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1)
s : Nat
⊢ range' s (n + 1) = a :: xs ↔ s = a ∧ 0 < n + 1 ∧ xs = range' (a + 1) (n + 1 - 1)

Tactic:
simp only [range'_succ]

Result:
case succ
a : Nat
xs : List Nat
n : Nat
ih : ∀ {s : Nat}, range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1)
s : Nat
⊢ s :: range' (s + 1) n = a :: xs ↔ s = a ∧ 0 < n + 1 ∧ xs = range' (a + 1) (n + 1 - 1)

Proof state:
case succ
a : Nat
xs : List Nat
n : Nat
ih : ∀ {s : Nat}, range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1)
s : Nat
⊢ s :: range' (s + 1) n = a :: xs ↔ s = a ∧ 0 < n + 1 ∧ xs = range' (a + 1) (n + 1 - 1)

Tactic:
simp only [cons.injEq, and_congr_right_iff]

Result:
case succ
a : Nat
xs : List Nat
n : Nat
ih : ∀ {s : Nat}, range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1)
s : Nat
⊢ s = a → (range' (s + 1) n = xs ↔ 0 < n + 1 ∧ xs = range' (a + 1) (n + 1 - 1))

Proof state:
s n a : Nat
xs : List Nat
⊢ range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1)

Tactic:
induction n generalizing s with
| zero => simp
| succ n ih =>
  simp only [range'_succ]
  simp only [cons.injEq, and_congr_right_iff]
  rintro rfl
  simp [eq_comm]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem eq_mul_inv_iff_mul_eq {φ₁ φ₂ φ₃ : MvPowerSeries σ k}
    (h : constantCoeff σ k φ₃ ≠ 0) : φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂ :=
  ⟨fun k => by simp [k, mul_assoc, MvPowerSeries.inv_mul_cancel _ h], fun k => by
    simp [← k, mul_assoc, MvPowerSeries.mul_inv_cancel _ h]⟩

Proof state:
σ : Type u_1
k✝ : Type u_3
inst✝ : Field k✝
φ₁ φ₂ φ₃ : MvPowerSeries σ k✝
h : (constantCoeff σ k✝) φ₃ ≠ 0
k : φ₁ * φ₃ = φ₂
⊢ φ₁ = φ₂ * φ₃⁻¹

Tactic:
simp [← k, mul_assoc, MvPowerSeries.mul_inv_cancel _ h]

Result:
no goals

Proof state:
σ : Type u_1
k✝ : Type u_3
inst✝ : Field k✝
φ₁ φ₂ φ₃ : MvPowerSeries σ k✝
h : (constantCoeff σ k✝) φ₃ ≠ 0
k : φ₁ = φ₂ * φ₃⁻¹
⊢ φ₁ * φ₃ = φ₂

Tactic:
simp [k, mul_assoc, MvPowerSeries.inv_mul_cancel _ h]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem mul_ball_one : s * ball 1 δ = thickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = ⋃ x ∈ s, ball x δ

Tactic:
convert iUnion₂_mul (fun x (_ : x ∈ s) => {x}) (ball (1 : E) δ)

Result:
case h.e'_2.h.e'_5
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s = ⋃ i ∈ s, {i}

case h.e'_3.h.e'_3.h.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = thickening δ s

Tactic:
rw [thickening_eq_biUnion_ball]

Result:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = ⋃ x ∈ s, ball x δ

Proof state:
case h.e'_3.h.e'_3.h.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ

Tactic:
ext x

Result:
case h.e'_3.h.e'_3.h.f.h
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ {x✝¹} * ball 1 δ

Proof state:
case h.e'_3.h.e'_3.h.f.h
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ {x✝¹} * ball 1 δ

Tactic:
simp_rw [singleton_mul_ball, mul_one]

Result:
no goals

Proof state:
case h.e'_2.h.e'_5
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s = ⋃ i ∈ s, {i}

Tactic:
exact s.biUnion_of_singleton.symm

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem card_range_le {α β : Type*} (f : α → β) [Fintype α] [Fintype (Set.range f)] :
    Fintype.card (Set.range f) ≤ Fintype.card α :=
  Fintype.card_le_of_surjective (fun a => ⟨f a, by simp⟩) fun ⟨_, a, ha⟩ => ⟨a, by simpa using ha⟩

Proof state:
α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
a : α
⊢ f a ∈ Set.range f

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
x✝ : ↑(Set.range f)
val✝ : β
a : α
ha : f a = val✝
⊢ (fun a => ⟨f a, ⋯⟩) a = ⟨val✝, ⋯⟩

Tactic:
simpa using ha

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.exists_maximal_wrt [PartialOrder β] (f : α → β) (s : Set α) (h : s.Finite)
    (hs : s.Nonempty) : ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'

Proof state:
case neg
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
c : α
hc : c ∈ insert a s
hbc : f b ≤ f c
⊢ f b = f c

Tactic:
rcases Set.mem_insert_iff.1 hc with (rfl | hcs)

Result:
case neg.inl
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ s : Set α
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
c : α
hbc : f b ≤ f c
his : c ∉ s
hs : (insert c s).Nonempty
h : ¬f b ≤ f c
hc : c ∈ insert c s
⊢ f b = f c

case neg.inr
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
c : α
hc : c ∈ insert a s
hbc : f b ≤ f c
hcs : c ∈ s
⊢ f b = f c

Proof state:
case h
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h : s = ∅
⊢ a ∈ insert a s ∧ ∀ a' ∈ insert a s, f a ≤ f a' → f a = f a'

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos.inl
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ s : Set α
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
h✝ : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
c : α
his : c ∉ s
hs : (insert c s).Nonempty
h : f b ≤ f c
hc : c ∈ insert c s
hac : f c ≤ f c
⊢ f c ≤ f c

Tactic:
rfl

Result:
no goals

Proof state:
case insert.inr
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h : s.Nonempty
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'

Tactic:
rcases ih h with ⟨b, hb, ih⟩

Result:
case insert.inr.intro.intro
α : Type u
β : Type v
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
a : α
s : Set α
his : a ∉ s
hs✝ : s.Finite
ih✝ : s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
hs : (insert a s).Nonempty
h : s.Nonempty
b : α
hb : b ∈ s
ih : ∀ a' ∈ s, f b ≤ f a' → f b = f a'
⊢ ∃ a_1 ∈ insert a s, ∀ a' ∈ insert a s, f a_1 ≤ f a' → f a_1 = f a'
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
@[simp] lemma coord_vadd (v : V) (b : AffineBasis ι k P) :
    (v +ᵥ b).coord i = (b.coord i).comp (AffineEquiv.constVAdd k P v).symm

Proof state:
case h
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ ((v +ᵥ b).coord i) p = ((b.coord i).comp ↑(AffineEquiv.constVAdd k P v).symm) p

Tactic:
simp only [coord, ne_eq, basisOf_vadd, coe_vadd, Pi.vadd_apply, Basis.coe_sumCoords,
  AffineMap.coe_mk, AffineEquiv.constVAdd_symm, AffineMap.coe_comp, AffineEquiv.coe_toAffineMap,
  Function.comp_apply, AffineEquiv.constVAdd_apply, sub_right_inj]

Result:
case h
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ (((b.basisOf i).repr (p -ᵥ (v +ᵥ b i))).sum fun x => id) = ((b.basisOf i).repr ((-v +ᵥ p) -ᵥ b i)).sum fun x => id

Proof state:
case h
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ (((b.basisOf i).repr (p -ᵥ (v +ᵥ b i))).sum fun x => id) = ((b.basisOf i).repr ((-v +ᵥ p) -ᵥ b i)).sum fun x => id

Tactic:
congr! 1

Result:
case h.h.e'_6
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ (b.basisOf i).repr (p -ᵥ (v +ᵥ b i)) = (b.basisOf i).repr ((-v +ᵥ p) -ᵥ b i)

Proof state:
case h.h.e'_6
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ (b.basisOf i).repr (p -ᵥ (v +ᵥ b i)) = (b.basisOf i).repr ((-v +ᵥ p) -ᵥ b i)

Tactic:
rw [vadd_vsub_assoc, neg_add_eq_sub, vsub_vadd_eq_vsub_sub]

Result:
no goals

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
⊢ (v +ᵥ b).coord i = (b.coord i).comp ↑(AffineEquiv.constVAdd k P v).symm

Tactic:
ext p

Result:
case h
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ ((v +ᵥ b).coord i) p = ((b.coord i).comp ↑(AffineEquiv.constVAdd k P v).symm) p
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/If.lean
theorem denote_mkIfCached {aig : AIG α} {input : TernaryInput aig} :
    ⟦aig.mkIfCached input, assign⟧
      =
    if ⟦aig, input.discr, assign⟧ then ⟦aig, input.lhs, assign⟧ else ⟦aig, input.rhs, assign⟧

Proof state:
case e_y.e_y
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      {
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := input.rhs }⟧

Tactic:
rw [LawfulOperator.denote_mem_prefix]

Result:
case e_y.e_y
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦assign,
      { aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
        ref := { gate := input.rhs.gate, hgate := ?e_y.e_y } }⟧ =
    ⟦assign, { aig := aig, ref := input.rhs }⟧

case e_y.e_y
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ input.rhs.gate < (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.decls.size
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapCyclesIso_hom_naturality [S₁.HasLeftHomology] [S₂.HasLeftHomology]
    [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
    cyclesMap (F.mapShortComplex.map φ) ≫ (S₂.mapCyclesIso F).hom =
      (S₁.mapCyclesIso F).hom ≫ F.map (cyclesMap φ)

Proof state:
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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ cyclesMap (F.mapShortComplex.map φ) ≫ (S₂.mapCyclesIso F).hom = (S₁.mapCyclesIso F).hom ≫ F.map (cyclesMap φ)

Tactic:
dsimp only [cyclesMap, mapCyclesIso, LeftHomologyData.cyclesIso, cyclesMapIso', Iso.refl]

Result:
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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ cyclesMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).leftHomologyData
        (F.mapShortComplex.obj S₂).leftHomologyData ≫
      cyclesMap' (𝟙 (S₂.map F)) (S₂.map F).leftHomologyData (S₂.leftHomologyData.map F) =
    cyclesMap' (𝟙 (S₁.map F)) (S₁.map F).leftHomologyData (S₁.leftHomologyData.map F) ≫
      F.map (cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData)

Proof state:
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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ cyclesMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).leftHomologyData
        (F.mapShortComplex.obj S₂).leftHomologyData ≫
      cyclesMap' (𝟙 (S₂.map F)) (S₂.map F).leftHomologyData (S₂.leftHomologyData.map F) =
    cyclesMap' (𝟙 (S₁.map F)) (S₁.map F).leftHomologyData (S₁.leftHomologyData.map F) ≫
      F.map (cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData)

Tactic:
simp only [LeftHomologyData.map_cyclesMap', Functor.mapShortComplex_obj, ← cyclesMap'_comp,
  comp_id, id_comp]

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem mkInductiveAux₃ (i j : ℕ) (h : i + 1 = j) :
    (mkInductiveAux₂ e zero comm_zero one comm_one succ i).2.1 ≫ (Q.xPrevIso h).hom =
      (P.xNextIso h).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ j).1

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q ⋯).hom =
    (xNextIso P ⋯).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst

Tactic:
rcases i with (_ | _ | i) <;> simp [mkInductiveAux₂]

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
i j : ℕ
h : i + 1 = j
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom =
    (xNextIso P h).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst

Tactic:
subst j

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q ⋯).hom =
    (xNextIso P ⋯).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst
-- Mathlib/Data/Set/Prod.lean
theorem update_image [DecidableEq ι] (x : (i : ι) → β i) (i : ι) (s : Set (β i)) :
    update x i '' s = Set.univ.pi (update (fun j ↦ {x j}) i s)

Proof state:
case h
ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔ ∀ (i_1 : ι), y i_1 ∈ update (fun j => {x j}) i s i_1

Tactic:
rw [forall_update_iff (p := fun x s => y x ∈ s)]

Result:
case h
ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔ y i ∈ s ∧ ∀ (x_1 : ι), x_1 ≠ i → y x_1 ∈ {x x_1}

Proof state:
case h
ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ y ∈ update x i '' s ↔ y ∈ univ.pi (update (fun j => {x j}) i s)

Tactic:
simp only [mem_image, update_eq_iff, ne_eq, and_left_comm (a := _ ∈ s), exists_eq_left, mem_pi,
  mem_univ, true_implies]

Result:
case h
ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔ ∀ (i_1 : ι), y i_1 ∈ update (fun j => {x j}) i s i_1

Proof state:
ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
⊢ update x i '' s = univ.pi (update (fun j => {x j}) i s)

Tactic:
ext y

Result:
case h
ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ y ∈ update x i '' s ↔ y ∈ univ.pi (update (fun j => {x j}) i s)

Proof state:
case h
ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
y : (a : ι) → β a
⊢ (y i ∈ s ∧ ∀ (x_1 : ι), ¬x_1 = i → x x_1 = y x_1) ↔ y i ∈ s ∧ ∀ (x_1 : ι), x_1 ≠ i → y x_1 ∈ {x x_1}

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_nonneg_iff : 0 ≤ sign a ↔ 0 ≤ a

Proof state:
case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 < a
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
simp [h, h.le]

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
simp [← h]

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
simp [h, h.not_le]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
rcases lt_trichotomy 0 a with (h | h | h)

Result:
case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 < a
⊢ 0 ≤ sign a ↔ 0 ≤ a

case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ 0 ≤ sign a ↔ 0 ≤ a

case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ 0 ≤ sign a ↔ 0 ≤ a
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.ofList_eq [BEq α] [Hashable α] {l : List (α × β)} :
    Raw.Const.ofList l = Raw₀.Const.insertMany Raw₀.empty l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
l : List (α × β)
⊢ (Raw₀.Const.insertMany ⟨∅, ⋯⟩ l).val.val = (Raw₀.Const.insertMany Raw₀.empty l).val.val

Tactic:
congr

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
l : List (α × β)
⊢ Raw.Const.ofList l = (Raw₀.Const.insertMany Raw₀.empty l).val.val

Tactic:
simp only [Raw.Const.ofList, Raw.Const.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
l : List (α × β)
⊢ (Raw₀.Const.insertMany ⟨∅, ⋯⟩ l).val.val = (Raw₀.Const.insertMany Raw₀.empty l).val.val
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive (attr := simp)]
lemma injective_pow_iff_not_isOfFinOrder : Injective (fun n : ℕ ↦ x ^ n) ↔ ¬IsOfFinOrder x

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : (fun n => x ^ n) n = (fun n => x ^ n) m
⊢ n = m

Tactic:
rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, modEq_zero_iff] at hnm

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
⊢ (Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
refine ⟨fun h => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => ?_⟩

Result:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : (fun n => x ^ n) n = (fun n => x ^ n) m
⊢ n = m
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_congr {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ a in f, p a → u a = v a) :
    blimsup u f p = blimsup v f p

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ blimsup u f p = blimsup v f p

Tactic:
simpa only [blimsup_eq_limsup] using limsup_congr <| eventually_inf_principal.2 h

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_drop : ∀ (n) {l₁ l₂}, Forall₂ R l₁ l₂ → Forall₂ R (drop n l₁) (drop n l₂)
  | 0, _, _, h => by simp only [drop, h]
  | _ + 1, _, _, Forall₂.nil => by simp only [Forall₂.nil, drop]
  | n + 1, _, _, Forall₂.cons h₁ h₂ => by simp [And.intro h₁ h₂, forall₂_drop n]

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
n : ℕ
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (drop (n + 1) (a✝ :: l₁✝)) (drop (n + 1) (b✝ :: l₂✝))

Tactic:
simp [And.intro h₁ h₂, forall₂_drop n]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
x✝¹ : List α
x✝ : List β
h : Forall₂ R x✝¹ x✝
⊢ Forall₂ R (drop 0 x✝¹) (drop 0 x✝)

Tactic:
simp only [drop, h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
n✝ : ℕ
⊢ Forall₂ R (drop (n✝ + 1) []) (drop (n✝ + 1) [])

Tactic:
simp only [Forall₂.nil, drop]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma nontrivial_of_diam_ne_zero (h : G.diam ≠ 0) : Nontrivial α

Proof state:
α : Type u_1
G : SimpleGraph α
h : G.ediam = 0
⊢ G.diam = 0

Tactic:
simp [diam, h]

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
h : G.diam ≠ 0
⊢ Nontrivial α

Tactic:
apply G.nontrivial_of_ediam_ne_zero

Result:
α : Type u_1
G : SimpleGraph α
h : G.diam ≠ 0
⊢ G.ediam ≠ 0

Proof state:
α : Type u_1
G : SimpleGraph α
h : G.diam ≠ 0
⊢ G.ediam ≠ 0

Tactic:
contrapose! h

Result:
α : Type u_1
G : SimpleGraph α
h : G.ediam = 0
⊢ G.diam = 0