harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem PiToModule.fromEnd_apply_single_one [DecidableEq ι] (f : Module.End R M) (i : ι) :
    PiToModule.fromEnd R b f (Pi.single i 1) = f (b i)

Proof state:
case h.e'_3
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ b i = 1 • b i

Tactic:
rw [one_smul]

Result:
no goals

Proof state:
case h.e_6.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ ((Fintype.linearCombination R R) b) (Pi.single i 1) = b i

Tactic:
convert Fintype.linearCombination_apply_single (S := R) R b i (1 : R)

Result:
case h.e'_3
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ b i = 1 • b i

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ f (((Fintype.linearCombination R R) b) (Pi.single i 1)) = f (b i)

Tactic:
congr

Result:
case h.e_6.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ ((Fintype.linearCombination R R) b) (Pi.single i 1) = b i

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ ((fromEnd R b) f) (Pi.single i 1) = f (b i)

Tactic:
rw [PiToModule.fromEnd_apply]

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ f (((Fintype.linearCombination R R) b) (Pi.single i 1)) = f (b i)
-- Mathlib/RingTheory/Ideal/Prod.lean
theorem ideal_prod_eq (I : Ideal (R × S)) :
    I = Ideal.prod (map (RingHom.fst R S) I : Ideal R) (map (RingHom.snd R S) I)

Proof state:
case h.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔ (r, s) ∈ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)

Tactic:
rw [mem_prod, mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective,
  mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]

Result:
case h.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔ (∃ x ∈ I, (RingHom.fst R S) x = r) ∧ ∃ x ∈ I, (RingHom.snd R S) x = s

Proof state:
case h.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔ (∃ x ∈ I, (RingHom.fst R S) x = r) ∧ ∃ x ∈ I, (RingHom.snd R S) x = s

Tactic:
refine ⟨fun h => ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, ?_⟩

Result:
case h.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s : S
⊢ ((∃ x ∈ I, (RingHom.fst R S) x = r) ∧ ∃ x ∈ I, (RingHom.snd R S) x = s) → (r, s) ∈ I

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ ∀ (x : R × S), x ∈ I ↔ x ∈ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)

Tactic:
rintro ⟨r, s⟩

Result:
case h.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔ (r, s) ∈ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ I = (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)

Tactic:
apply Ideal.ext

Result:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
⊢ ∀ (x : R × S), x ∈ I ↔ x ∈ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)

Proof state:
case h.mk
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s : S
⊢ ((∃ x ∈ I, (RingHom.fst R S) x = r) ∧ ∃ x ∈ I, (RingHom.snd R S) x = s) → (r, s) ∈ I

Tactic:
rintro ⟨⟨⟨r, s'⟩, ⟨h₁, rfl⟩⟩, ⟨⟨r', s⟩, ⟨h₂, rfl⟩⟩⟩

Result:
case h.mk.intro.intro.mk.intro.intro.mk.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s' : S
h₁ : (r, s') ∈ I
r' : R
s : S
h₂ : (r', s) ∈ I
⊢ ((RingHom.fst R S) (r, s'), (RingHom.snd R S) (r', s)) ∈ I

Proof state:
case h.mk.intro.intro.mk.intro.intro.mk.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s' : S
h₁ : (r, s') ∈ I
r' : R
s : S
h₂ : (r', s) ∈ I
⊢ ((RingHom.fst R S) (r, s'), (RingHom.snd R S) (r', s)) ∈ I

Tactic:
simpa using I.add_mem (I.mul_mem_left (1, 0) h₁) (I.mul_mem_left (0, 1) h₂)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_lt_rpow_of_exponent_gt {x : ℝ≥0∞} {y z : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
    x ^ y < x ^ z

Proof state:
case intro
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < ↑x
hx1 : ↑x < 1
⊢ ↑x ^ y < ↑x ^ z

Tactic:
simp only [coe_lt_one_iff, coe_pos] at hx0 hx1

Result:
case intro
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < x
hx1 : x < 1
⊢ ↑x ^ y < ↑x ^ z

Proof state:
case intro
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < x
hx1 : x < 1
⊢ ↑x ^ y < ↑x ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt hx0), NNReal.rpow_lt_rpow_of_exponent_gt hx0 hx1 hyz]

Result:
no goals

Proof state:
x : ℝ≥0∞
y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx1 le_top)

Result:
case intro
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < ↑x
hx1 : ↑x < 1
⊢ ↑x ^ y < ↑x ^ z
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_add_le (x y : Game) : (x + y).birthday ≤ x.birthday ♯ y.birthday

Proof state:
x y : Game
⊢ (x + y).birthday ≤ x.birthday ♯ y.birthday

Tactic:
let ⟨a, ha₁, ha₂⟩ := birthday_eq_pGameBirthday x

Result:
x y : Game
a : PGame
ha₁ : ⟦a⟧ = x
ha₂ : a.birthday = x.birthday
⊢ (x + y).birthday ≤ x.birthday ♯ y.birthday

Proof state:
x y : Game
a : PGame
ha₁ : ⟦a⟧ = x
ha₂ : a.birthday = x.birthday
b : PGame
hb₁ : ⟦b⟧ = y
hb₂ : b.birthday = y.birthday
⊢ (x + y).birthday ≤ x.birthday ♯ y.birthday

Tactic:
rw [← ha₂, ← hb₂, ← ha₁, ← hb₁, ← PGame.birthday_add]

Result:
x y : Game
a : PGame
ha₁ : ⟦a⟧ = x
ha₂ : a.birthday = x.birthday
b : PGame
hb₁ : ⟦b⟧ = y
hb₂ : b.birthday = y.birthday
⊢ (⟦a⟧ + ⟦b⟧).birthday ≤ (a + b).birthday

Proof state:
x y : Game
a : PGame
ha₁ : ⟦a⟧ = x
ha₂ : a.birthday = x.birthday
⊢ (x + y).birthday ≤ x.birthday ♯ y.birthday

Tactic:
let ⟨b, hb₁, hb₂⟩ := birthday_eq_pGameBirthday y

Result:
x y : Game
a : PGame
ha₁ : ⟦a⟧ = x
ha₂ : a.birthday = x.birthday
b : PGame
hb₁ : ⟦b⟧ = y
hb₂ : b.birthday = y.birthday
⊢ (x + y).birthday ≤ x.birthday ♯ y.birthday

Proof state:
x y : Game
a : PGame
ha₁ : ⟦a⟧ = x
ha₂ : a.birthday = x.birthday
b : PGame
hb₁ : ⟦b⟧ = y
hb₂ : b.birthday = y.birthday
⊢ (⟦a⟧ + ⟦b⟧).birthday ≤ (a + b).birthday

Tactic:
exact birthday_quot_le_pGameBirthday  _

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem sInter_comap_sets (f : α → β) (F : Filter β) : ⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ x ∈ ⋂₀ (comap f F).sets ↔ x ∈ ⋂ U ∈ F, f ⁻¹' U

Tactic:
suffices (∀ (A : Set α) (B : Set β), B ∈ F → f ⁻¹' B ⊆ A → x ∈ A) ↔
    ∀ B : Set β, B ∈ F → f x ∈ B by
  simp only [mem_sInter, mem_iInter, Filter.mem_sets, mem_comap, this, and_imp, exists_prop,
    mem_preimage, exists_imp]

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
this : (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
⊢ x ∈ ⋂₀ (comap f F).sets ↔ x ∈ ⋂ U ∈ F, f ⁻¹' U

Tactic:
simp only [mem_sInter, mem_iInter, Filter.mem_sets, mem_comap, this, and_imp, exists_prop,
  mem_preimage, exists_imp]

Result:
no goals

Proof state:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ B ∈ F, f x ∈ B) → ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A

Tactic:
intro h V U U_in f_U_V

Result:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
V : Set α
U : Set β
U_in : U ∈ F
f_U_V : f ⁻¹' U ⊆ V
⊢ x ∈ V

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
⊢ ⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ x ∈ ⋂₀ (comap f F).sets ↔ x ∈ ⋂ U ∈ F, f ⁻¹' U

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B

Tactic:
constructor

Result:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) → ∀ B ∈ F, f x ∈ B

case h.mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ B ∈ F, f x ∈ B) → ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A

Proof state:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
V : Set α
U : Set β
U_in : U ∈ F
f_U_V : f ⁻¹' U ⊆ V
⊢ x ∈ V

Tactic:
exact f_U_V (h U U_in)

Result:
no goals

Proof state:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) → ∀ B ∈ F, f x ∈ B

Tactic:
intro h U U_in

Result:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
U : Set β
U_in : U ∈ F
⊢ f x ∈ U

Proof state:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
U : Set β
U_in : U ∈ F
⊢ f x ∈ U

Tactic:
simpa only [Subset.rfl, forall_prop_of_true, mem_preimage] using h (f ⁻¹' U) U U_in

Result:
no goals
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem mapL_coe : (mapL f).toLinearMap = map (fun i ↦ (f i).toLinearMap)

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
⊢ ↑(mapL f) = map fun i => ↑(f i)

Tactic:
ext

Result:
case H.H
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x✝ : (i : ι) → E i
⊢ ((↑(mapL f)).compMultilinearMap (tprod 𝕜)) x✝ = ((map fun i => ↑(f i)).compMultilinearMap (tprod 𝕜)) x✝

Proof state:
case H.H
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x✝ : (i : ι) → E i
⊢ ((↑(mapL f)).compMultilinearMap (tprod 𝕜)) x✝ = ((map fun i => ↑(f i)).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
simp only [mapL, LinearMap.compMultilinearMap_apply, ContinuousLinearMap.coe_coe,
  liftIsometry_apply_apply, lift.tprod, ContinuousMultilinearMap.coe_coe,
  ContinuousMultilinearMap.compContinuousLinearMap_apply, tprodL_toFun, map_tprod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem erase_range' :
    (range' s n).erase i =
      range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
case pos.intro.intro.intro
s n i : Nat
h : i ∈ range' s n
as bs : List Nat
h₁ : range' s n = as ++ i :: bs
h₂ : ¬i ∈ as
⊢ (range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
rw [h₁, erase_append_right _ h₂, erase_cons_head]

Result:
case pos.intro.intro.intro
s n i : Nat
h : i ∈ range' s n
as bs : List Nat
h₁ : range' s n = as ++ i :: bs
h₂ : ¬i ∈ as
⊢ as ++ bs = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
lemma shiftIso_add'_hom_app (n m mn : M) (hnm : m + n = mn) (a a' a'' : M)
    (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc])).hom.app X =
      (shift F a).map ((shiftFunctorAdd' C m n mn hnm).hom.app X) ≫
        (shiftIso F n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫
          (shiftIso F m a' a'' ha'').hom.app X

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_6, u_1} C
inst✝³ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso mn a a'' ⋯).hom.app X =
    (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).hom.app X) ≫
      (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X

Tactic:
simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

Result:
no goals

Proof state:
C : Type u_1
A : Type u_2
inst✝⁶ : Category.{?u.56941, u_1} C
inst✝⁵ : Category.{?u.56945, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ mn + a = a''

Tactic:
rw [← hnm, ← ha'', ← ha', add_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assignment)
    (assignments_size : assignments.size = n)
    (units : Array (Literal (PosFin n))) (foundContradiction : Bool) (l : Literal (PosFin n)) :
    let insertUnit_res := insertUnit (units, assignments, foundContradiction) l
    (foundContradiction → ∃ i : PosFin n, assignments[i.1]'(by rw [assignments_size]; exact i.2.2) = both) → insertUnit_res.2.2 →
    ∃ j : PosFin n, insertUnit_res.2.1[j.1]'(by rw [size_insertUnit, assignments_size]; exact j.2.2) = both

Proof state:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ (insertUnit (units, assignments, foundContradiction) l).snd.fst[l.fst.val] = both

Tactic:
simp only [insertUnit, hl, ite_false, Array.getElem_modify_self, reduceCtorEq]

Result:
case inr
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
assignments_l_ne_unassigned : (assignments[l.fst.val]! != unassigned) = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_const_mul'' (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
    ∫⁻ a, r * f a ∂μ = r * ∫⁻ a, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
rw [A, B, lintegral_const_mul _ hf.measurable_mk]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
have A : ∫⁻ a, f a ∂μ = ∫⁻ a, hf.mk f a ∂μ := lintegral_congr_ae hf.ae_eq_mk

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ

Tactic:
have B : ∫⁻ a, r * f a ∂μ = ∫⁻ a, r * hf.mk f a ∂μ :=
  lintegral_congr_ae (EventuallyEq.fun_comp hf.ae_eq_mk _)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma map_id_eq_isoClosure (P : MorphismProperty C) :
    P.map (𝟭 _) = P.isoClosure

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.isoClosure.inverseImage (𝟭 C)

Tactic:
intro X Y f hf

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.isoClosure.inverseImage (𝟭 C) f

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.isoClosure.inverseImage (𝟭 C) f

Tactic:
exact P.le_isoClosure _ hf

Result:
no goals

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.map (𝟭 C) ≤ P.isoClosure

Tactic:
rw [map_le_iff]

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.isoClosure.inverseImage (𝟭 C)

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P.isoClosure f
⊢ P.map (𝟭 C) f

Tactic:
exact hf

Result:
no goals

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.isoClosure ≤ P.map (𝟭 C)

Tactic:
intro X Y f hf

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P.isoClosure f
⊢ P.map (𝟭 C) f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.map (𝟭 C) = P.isoClosure

Tactic:
apply le_antisymm

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.map (𝟭 C) ≤ P.isoClosure

case a
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.isoClosure ≤ P.map (𝟭 C)
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_sub_sinh : cosh x - sinh x = exp (-x)

Proof state:
x : ℝ
⊢ ↑(cosh x - sinh x) = ↑(rexp (-x))

Tactic:
simp

Result:
no goals

Proof state:
x : ℝ
⊢ cosh x - sinh x = rexp (-x)

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(cosh x - sinh x) = ↑(rexp (-x))
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem diam_thickening_le {α : Type*} [PseudoMetricSpace α] (s : Set α) (hε : 0 ≤ ε) :
    diam (thickening ε s) ≤ diam s + 2 * ε

Proof state:
case neg.inl
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : ¬Bornology.IsBounded s
hε : 0 ≤ 0
⊢ diam (thickening 0 s) ≤ diam s + 2 * 0

Tactic:
simp [thickening_of_nonpos, diam_nonneg]

Result:
no goals

Proof state:
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
by_cases hs : IsBounded s

Result:
case pos
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

case neg
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : ¬Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Proof state:
case pos
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
exact (diam_mono (thickening_subset_cthickening _ _) hs.cthickening).trans
  (diam_cthickening_le _ hε)

Result:
no goals

Proof state:
case neg.inr
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bornology.IsBounded s
hε : 0 < ε
⊢ 0 ≤ diam s + 2 * ε

Tactic:
positivity

Result:
no goals

Proof state:
case neg
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : ¬Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
obtain rfl | hε := hε.eq_or_lt

Result:
case neg.inl
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : ¬Bornology.IsBounded s
hε : 0 ≤ 0
⊢ diam (thickening 0 s) ≤ diam s + 2 * 0

case neg.inr
ε : ℝ
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bornology.IsBounded s
hε : 0 < ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIsoAt_iff_isIso_homologyMap (f : K ⟶ L) (i : ι)
    [K.HasHomology i] [L.HasHomology i] :
    QuasiIsoAt f i ↔ IsIso (homologyMap f i)

Proof state:
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) ↔ IsIso (homologyMap f i)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt f i ↔ IsIso (homologyMap f i)

Tactic:
rw [quasiIsoAt_iff, ShortComplex.quasiIso_iff]

Result:
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) ↔ IsIso (homologyMap f i)