harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.gcd_mul_left_cancel_right (m : ℕ+) {n k : ℕ+} :
    k.Coprime m → m.gcd (k * n) = m.gcd n

Proof state:
m n k : ℕ+
h : k.Coprime m
⊢ m.gcd n = (k * n).gcd m

Tactic:
rw [gcd_comm]

Result:
m n k : ℕ+
h : k.Coprime m
⊢ n.gcd m = (k * n).gcd m

Proof state:
m n k : ℕ+
h : k.Coprime m
⊢ m.gcd (k * n) = m.gcd n

Tactic:
iterate 2 rw [gcd_comm]; symm

Result:
m n k : ℕ+
h : k.Coprime m
⊢ (k * n).gcd m = n.gcd m

Proof state:
m n k : ℕ+
h : k.Coprime m
⊢ (k * n).gcd m = n.gcd m

Tactic:
apply Coprime.gcd_mul_left_cancel _ h

Result:
no goals

Proof state:
m n k : ℕ+
⊢ k.Coprime m → m.gcd (k * n) = m.gcd n

Tactic:
intro h

Result:
m n k : ℕ+
h : k.Coprime m
⊢ m.gcd (k * n) = m.gcd n

Proof state:
m n k : ℕ+
h : k.Coprime m
⊢ n.gcd m = (k * n).gcd m

Tactic:
symm

Result:
m n k : ℕ+
h : k.Coprime m
⊢ (k * n).gcd m = n.gcd m
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem resolve_left_lt_lcm (a c d p x : Int) (a_pos : 0 < a) (d_pos : 0 < d) (h₁ : p ≤ a * x) :
    resolve_left a c d p x < lcm a (a * d / gcd (a * d) c)

Proof state:
a c d p x : Int
a_pos : 0 < a
d_pos : 0 < d
h₁ : p ≤ a * x
⊢ resolve_left a c d p x < ↑(a.lcm (a * d / ↑((a * d).gcd c)))

Tactic:
simp only [h₁, resolve_left_eq, resolve_left', add_of_le, Int.ofNat_lt]

Result:
a c d p x : Int
a_pos : 0 < a
d_pos : 0 < d
h₁ : p ≤ a * x
⊢ (a * x - p).toNat % a.lcm (a * d / ↑((a * d).gcd c)) < a.lcm (a * d / ↑((a * d).gcd c))

Proof state:
a c d p x : Int
a_pos : 0 < a
d_pos : 0 < d
h₁ : p ≤ a * x
⊢ (a * x - p).toNat % a.lcm (a * d / ↑((a * d).gcd c)) < a.lcm (a * d / ↑((a * d).gcd c))

Tactic:
exact Nat.mod_lt _ (Nat.pos_of_ne_zero (lcm_ne_zero (Int.ne_of_gt a_pos)
  (Int.ne_of_gt (Int.ediv_pos_of_pos_of_dvd (Int.mul_pos a_pos d_pos) (Int.ofNat_nonneg _)
    gcd_dvd_left))))

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xn_one : xn a1 1 = a

Proof state:
a : ℕ
a1 : 1 < a
⊢ xn a1 1 = a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma π_homologyIsoSc'_inv :
    (K.sc' i j k).homologyπ ≫ (K.homologyIsoSc' i j k hi hk).inv =
      (K.cyclesIsoSc' i j k hi hk).inv ≫ K.homologyπ j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc' i j k).homologyπ ≫ (K.homologyIsoSc' i j k hi hk).inv = (K.cyclesIsoSc' i j k hi hk).inv ≫ K.homologyπ j

Tactic:
apply ShortComplex.homologyπ_naturality

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem zero_measure {f : α → α} (hf : Measurable f) : @QuasiErgodic α m f 0 where
  measurable := hf
  absolutelyContinuous

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
hf : Measurable f
⊢ Measure.map f 0 ≪ 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.eq_true_of_not_eq_false {a : Bool} (h : (!a) = false) : a = true

Proof state:
a : Bool
h : (!a) = false
⊢ a = true

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem one_geom_sum (n : ℕ) : ∑ i ∈ range n, (1 : α) ^ i = n

Proof state:
α : Type u
inst✝ : Semiring α
n : ℕ
⊢ ∑ i ∈ range n, 1 ^ i = ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem spanningSetsIndex_eq_iff (μ : Measure α) [SigmaFinite μ] {x : α} {n : ℕ} :
    spanningSetsIndex μ x = n ↔ x ∈ disjointed (spanningSets μ) n

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
x : α
n : ℕ
⊢ spanningSetsIndex μ x = n ↔ x ∈ disjointed (spanningSets μ) n

Tactic:
convert Set.ext_iff.1 (preimage_spanningSetsIndex_singleton μ n) x

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem disjoint_singleton : Disjoint l [a] ↔ a ∉ l

Proof state:
α✝ : Type u_1
l : List α✝
a : α✝
⊢ l.Disjoint [a] ↔ ¬a ∈ l

Tactic:
rw [disjoint_comm, singleton_disjoint]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_sum [Finite α] [Finite β] : Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
simp_rw [Nat.card_eq_fintype_card, Fintype.card_sum]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
have := Fintype.ofFinite β

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
have := Fintype.ofFinite α

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
-- Mathlib/Computability/PostTuringMachine.lean
theorem reaches_eval {σ} {f : σ → Option σ} {a b} (ab : Reaches f a b) : eval f a = eval f b

Proof state:
case refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f b
bc : Reaches f b x✝
c0 : f x✝ = none
⊢ x✝ ∈ eval f a

Tactic:
exact mem_eval.2 ⟨ab.trans bc, c0⟩

Result:
no goals

Proof state:
case refine_1
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f a
⊢ x✝ ∈ eval f b

Tactic:
have ⟨ac, c0⟩ := mem_eval.1 h

Result:
case refine_1
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f a
ac : Reaches f a x✝
c0 : f x✝ = none
⊢ x✝ ∈ eval f b

Proof state:
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
⊢ eval f a = eval f b

Tactic:
refine Part.ext fun _ ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f a
⊢ x✝ ∈ eval f b

case refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f b
⊢ x✝ ∈ eval f a

Proof state:
case refine_1
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f a
ac : Reaches f a x✝
c0 : f x✝ = none
⊢ x✝ ∈ eval f b

Tactic:
exact mem_eval.2 ⟨(or_iff_left_of_imp fun cb ↦ (eval_maximal h).1 cb ▸ ReflTransGen.refl).1
  (reaches_total ab ac), c0⟩

Result:
no goals

Proof state:
case refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f b
⊢ x✝ ∈ eval f a

Tactic:
have ⟨bc, c0⟩ := mem_eval.1 h

Result:
case refine_2
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f b
bc : Reaches f b x✝
c0 : f x✝ = none
⊢ x✝ ∈ eval f a
-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem mul_polyOfInterest_aux2 (n : ℕ) :
    (p : 𝕄) ^ n * wittMul p n + wittPolyProdRemainder p n = wittPolyProd p n

Proof state:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ n * wittMul p n + wittPolyProdRemainder p n = ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i)

Tactic:
rw [sum_range_succ, add_comm, Nat.sub_self, pow_zero, pow_one]

Result:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittPolyProdRemainder p n + ↑p ^ n * wittMul p n =
    ∑ x ∈ range n, ↑p ^ x * wittMul p x ^ p ^ (n - x) + ↑p ^ n * wittMul p n

Proof state:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ wittPolyProdRemainder p n + ↑p ^ n * wittMul p n =
    ∑ x ∈ range n, ↑p ^ x * wittMul p x ^ p ^ (n - x) + ↑p ^ n * wittMul p n

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ n * wittMul p n + wittPolyProdRemainder p n = wittPolyProd p n

Tactic:
convert mul_polyOfInterest_aux1 p n

Result:
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ n * wittMul p n + wittPolyProdRemainder p n = ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i)
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
theorem evalAt_eq (x : X) : ⟦H.evalAt x⟧ = hcast (H.apply_zero x).symm ≫
    (πₘ (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x))) ≫
      hcast (H.apply_one x).symm.symm

Proof state:
case hp
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
t✝ : ↑I
⊢ (H.evalAt x) t✝ = ((fun q => q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t✝

Tactic:
rfl

Result:
no goals

Proof state:
case hp
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ∀ (t : ↑I), (H.evalAt x) t = ((fun q => q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t

Tactic:
intro

Result:
case hp
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
t✝ : ↑I
⊢ (H.evalAt x) t✝ = ((fun q => q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t✝

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ HEq ⟦H.evalAt x⟧
    ((π.map (TopCat.ofHom H.uliftMap)).map
      ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))))

Tactic:
simp only [id_eq_path_refl, prodToProdTop_map, Path.Homotopic.prod_lift, map_eq, ←
  Path.Homotopic.map_lift]

Result:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ HEq ⟦H.evalAt x⟧
    (Path.Homotopic.Quotient.mapFn
      ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) H.uliftMap)

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ HEq ⟦H.evalAt x⟧
    (Path.Homotopic.Quotient.mapFn
      ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) H.uliftMap)

Tactic:
apply Path.Homotopic.hpath_hext

Result:
case hp
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ∀ (t : ↑I), (H.evalAt x) t = ((fun q => q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ⟦H.evalAt x⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x))) ≫ hcast ⋯

Tactic:
dsimp only [prodToProdTopI, uhpath01, hcast]

Result:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ⟦H.evalAt x⟧ =
    eqToHom ⋯ ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) ≫
        eqToHom ⋯

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ ⟦H.evalAt x⟧ =
    eqToHom ⋯ ≫
      (π.map (TopCat.ofHom H.uliftMap)).map
          ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) ≫
        eqToHom ⋯

Tactic:
refine (@conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _
  (FundamentalGroupoid.ext <| H.apply_one x).symm).mpr ?_

Result:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x : ↑X
⊢ HEq ⟦H.evalAt x⟧
    ((π.map (TopCat.ofHom H.uliftMap)).map
      ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))))
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_neg : exp (-x) = (exp x)⁻¹

Proof state:
x : ℂ
⊢ cexp (-x) = (cexp x)⁻¹

Tactic:
rw [← mul_right_inj' (exp_ne_zero x), ← exp_add]

Result:
x : ℂ
⊢ cexp (x + -x) = cexp x * (cexp x)⁻¹

Proof state:
x : ℂ
⊢ cexp (x + -x) = cexp x * (cexp x)⁻¹

Tactic:
simp [mul_inv_cancel₀ (exp_ne_zero x)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem degree_quadratic (ha : a ≠ 0) : degree (C a * X ^ 2 + C b * X + C c) = 2

Proof state:
R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).degree = 2

Tactic:
rw [add_assoc, degree_add_eq_left_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
  degree_C_mul_X_pow 2 ha]

Result:
R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑2 = 2

Proof state:
R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑2 = 2

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
theorem image_upperBounds_subset_upperBounds_image :
    f '' upperBounds s ⊆ upperBounds (f '' s)

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
Hf : Monotone f
s : Set α
⊢ f '' upperBounds s ⊆ upperBounds (f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
Hf : Monotone f
s : Set α
a : α
ha : a ∈ upperBounds s
⊢ f a ∈ upperBounds (f '' s)

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
Hf : Monotone f
s : Set α
a : α
ha : a ∈ upperBounds s
⊢ f a ∈ upperBounds (f '' s)

Tactic:
exact Hf.mem_upperBounds_image ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/BasicAux.lean
theorem getElem_append_right {as bs : List α} {i : Nat} (h₁ : as.length ≤ i) {h₂} :
    (as ++ bs)[i]'h₂ =
      bs[i - as.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂)

Proof state:
α : Type ?u.4619
as bs : List α
i : Nat
h₁ : as.length ≤ i
h₂ : i < as.length + bs.length
⊢ i - as.length < bs.length

Tactic:
exact Nat.sub_lt_left_of_lt_add h₁ h₂

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
bs : List α
a : α
as : List α
ih : ∀ {i : Nat} (h₁ : as.length ≤ i) {h₂ : i < (as ++ bs).length}, (as ++ bs)[i] = bs[i - as.length]
i : Nat
h₁✝ : (a :: as).length ≤ i + 1
h₂ : i + 1 < (a :: as ++ bs).length
h₁ : as.length ≤ i
⊢ (as ++ bs)[i] = bs[i - as.length]

Tactic:
apply ih

Result:
case cons.succ.h₁
α : Type u_1
bs : List α
a : α
as : List α
ih : ∀ {i : Nat} (h₁ : as.length ≤ i) {h₂ : i < (as ++ bs).length}, (as ++ bs)[i] = bs[i - as.length]
i : Nat
h₁✝ : (a :: as).length ≤ i + 1
h₂ : i + 1 < (a :: as ++ bs).length
h₁ : as.length ≤ i
⊢ as.length ≤ i

Proof state:
case cons.succ.h₁
α : Type u_1
bs : List α
a : α
as : List α
ih : ∀ {i : Nat} (h₁ : as.length ≤ i) {h₂ : i < (as ++ bs).length}, (as ++ bs)[i] = bs[i - as.length]
i : Nat
h₁✝ : (a :: as).length ≤ i + 1
h₂ : i + 1 < (a :: as ++ bs).length
h₁ : as.length ≤ i
⊢ as.length ≤ i

Tactic:
simp [h₁]

Result:
no goals

Proof state:
α : Type ?u.4619
as bs : List α
i : Nat
h₁ : as.length ≤ i
h₂ : i < (as ++ bs).length
⊢ i - as.length < bs.length

Tactic:
rw [length_append] at h₂

Result:
α : Type ?u.4619
as bs : List α
i : Nat
h₁ : as.length ≤ i
h₂ : i < as.length + bs.length
⊢ i - as.length < bs.length

Proof state:
case nil
α : Type u_1
bs : List α
i : Nat
h₁ : [].length ≤ i
h₂ : i < ([] ++ bs).length
⊢ ([] ++ bs)[i] = bs[i - [].length]

Tactic:
trivial

Result:
no goals

Proof state:
case cons
α : Type u_1
bs : List α
a : α
as : List α
ih : ∀ {i : Nat} (h₁ : as.length ≤ i) {h₂ : i < (as ++ bs).length}, (as ++ bs)[i] = bs[i - as.length]
i : Nat
h₁ : (a :: as).length ≤ i
h₂ : i < (a :: as ++ bs).length
⊢ (a :: as ++ bs)[i] = bs[i - (a :: as).length]

Tactic:
cases i with simp [get, Nat.succ_sub_succ] <;> simp [Nat.succ_sub_succ] at h₁
| succ i => apply ih; simp [h₁]

Result:
no goals

Proof state:
α : Type u_1
as bs : List α
i : Nat
h₁ : as.length ≤ i
h₂ : i < (as ++ bs).length
⊢ (as ++ bs)[i] = bs[i - as.length]

Tactic:
induction as generalizing i with
| nil => trivial
| cons a as ih =>
  cases i with simp [get, Nat.succ_sub_succ] <;> simp [Nat.succ_sub_succ] at h₁
  | succ i => apply ih; simp [h₁]

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem selfZPow_zero : selfZPow x B 0 = 1

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
⊢ selfZPow x B 0 = 1

Tactic:
simp [selfZPow_of_nonneg _ _ le_rfl]

Result:
no goals
-- Mathlib/Algebra/Homology/Localization.lean
lemma quotient_map_mem_quasiIso_iff {K L : HomologicalComplex C c} (f : K ⟶ L) :
    quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
eq : ∀ (i : ι), IsIso ((homologyFunctor C c i).map ((quotient C c).map f)) ↔ IsIso (HomologicalComplex.homologyMap f i)
⊢ quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f

Tactic:
simp only [HomologicalComplex.mem_quasiIso_iff, mem_quasiIso_iff, quasiIso_iff,
  quasiIsoAt_iff_isIso_homologyMap, eq]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f

Tactic:
have eq := fun (i : ι) => NatIso.isIso_map_iff (homologyFunctorFactors C c i) f

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
eq :
  ∀ (i : ι),
    IsIso ((quotient C c ⋙ homologyFunctor C c i).map f) ↔ IsIso ((HomologicalComplex.homologyFunctor C c i).map f)
⊢ quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
eq :
  ∀ (i : ι),
    IsIso ((quotient C c ⋙ homologyFunctor C c i).map f) ↔ IsIso ((HomologicalComplex.homologyFunctor C c i).map f)
⊢ quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f

Tactic:
dsimp at eq

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
eq : ∀ (i : ι), IsIso ((homologyFunctor C c i).map ((quotient C c).map f)) ↔ IsIso (HomologicalComplex.homologyMap f i)
⊢ quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ind {X : C} (p : Subobject X → Prop)
    (h : ∀ ⦃A : C⦄ (f : A ⟶ X) [Mono f], p (Subobject.mk f)) (P : Subobject X) : p P

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
a : MonoOver X
⊢ p (Quotient.mk'' a)

Tactic:
exact h a.arrow

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
⊢ ∀ (a : MonoOver X), p (Quotient.mk'' a)

Tactic:
intro a

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
a : MonoOver X
⊢ p (Quotient.mk'' a)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
⊢ p P

Tactic:
apply Quotient.inductionOn'

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Prop
h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f], p (mk f)
P : Subobject X
⊢ ∀ (a : MonoOver X), p (Quotient.mk'' a)
-- Mathlib/Computability/ContextFreeGrammar.lean
lemma produces_reverse : g.reverse.Produces u.reverse v.reverse ↔ g.Produces u v :=
  (Equiv.ofBijective _ ContextFreeRule.reverse_bijective).exists_congr
    (by simp [ContextFreeRule.reverse_involutive.eq_iff])

Proof state:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ ∀ (a : ContextFreeRule T g.reverse.NT),
    a ∈ g.reverse.rules ∧ a.Rewrites u.reverse v.reverse ↔
      (Equiv.ofBijective ContextFreeRule.reverse ⋯) a ∈ g.rules ∧
        ((Equiv.ofBijective ContextFreeRule.reverse ⋯) a).Rewrites u v

Tactic:
simp [ContextFreeRule.reverse_involutive.eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_eq_size {p : α → Bool} {xs : Array α} :
    xs.findIdx p = xs.size ↔ ∀ x ∈ xs, p x = false

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
⊢ findIdx p xs = xs.size ↔ ∀ (x : α), x ∈ xs → p x = false

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx p { toList := xs } = { toList := xs }.size ↔ ∀ (x : α), x ∈ { toList := xs } → p x = false

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx p { toList := xs } = { toList := xs }.size ↔ ∀ (x : α), x ∈ { toList := xs } → p x = false

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem single_pow (a : Γ) (n : ℕ) (r : R) : single a r ^ n = single (n • a) (r ^ n)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
a : Γ
n : ℕ
r : R
⊢ (single a) r ^ n = (single (n • a)) (r ^ n)

Tactic:
induction' n with n IH

Result:
case zero
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
⊢ (single a) r ^ 0 = (single (0 • a)) (r ^ 0)

case succ
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
n : ℕ
IH : (single a) r ^ n = (single (n • a)) (r ^ n)
⊢ (single a) r ^ (n + 1) = (single ((n + 1) • a)) (r ^ (n + 1))

Proof state:
case succ
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
n : ℕ
IH : (single a) r ^ n = (single (n • a)) (r ^ n)
⊢ (single a) r ^ (n + 1) = (single ((n + 1) • a)) (r ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]

Result:
no goals

Proof state:
case zero
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
⊢ (single a) r ^ 0 = (single (0 • a)) (r ^ 0)

Tactic:
ext

Result:
case zero.coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
x✝ : Γ
⊢ ((single a) r ^ 0).coeff x✝ = ((single (0 • a)) (r ^ 0)).coeff x✝

Proof state:
case zero.coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
x✝ : Γ
⊢ ((single a) r ^ 0).coeff x✝ = ((single (0 • a)) (r ^ 0)).coeff x✝

Tactic:
simp only [pow_zero, coeff_one, zero_smul, coeff_single]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem sub_le_self (s t : Multiset α) : s - t ≤ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ≤ s + t

Tactic:
exact le_add_right _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s - t ≤ s

Tactic:
rw [Multiset.sub_le_iff_le_add]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ≤ s + t