harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem eqToHom_left {X : T} {U V : Over X} (e : U = V) :
    (eqToHom e).left = eqToHom (e ▸ rfl : U.left = V.left)

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
e : U = V
⊢ (eqToHom e).left = eqToHom ⋯

Tactic:
subst e

Result:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U : Over X
⊢ (eqToHom ⋯).left = eqToHom ⋯

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U : Over X
⊢ (eqToHom ⋯).left = eqToHom ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem not_subset_iff_mem (hx : x.IsOrdinal) (hy : y.IsOrdinal) : ¬ x ⊆ y ↔ y ∈ x

Proof state:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ ¬x ⊆ y ↔ y ∈ x

Tactic:
rw [not_iff_comm, not_mem_iff_subset hy hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replace_replicate_self [LawfulBEq α] {a : α} (h : 0 < n) :
    (replicate n a).replace a b = b :: replicate (n - 1) a

Proof state:
α : Type u_1
inst✝¹ : BEq α
n : Nat
b : α
inst✝ : LawfulBEq α
a : α
h : 0 < n
⊢ (replicate n a).replace a b = b :: replicate (n - 1) a

Tactic:
cases n <;> simp_all [replicate_succ, replace_cons]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_flatMap (l : List α) (f : α → List β) :
    length (l.flatMap f) = sum (map (fun a => (f a).length) l)

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → List β
⊢ (flatMap f l).length = (map (fun a => (f a).length) l).sum

Tactic:
rw [List.flatMap, length_flatten, map_map, Function.comp_def]

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

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

Tactic:
simp_to_raw using Raw₀.getKey!_insert

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f)

Proof state:
β : Type u_1
γ : Type u_2
α : Type u_3
f : β → γ
l₁ : List α
l₂ : List β
⊢ l₁.zip (map f l₂) = map (Prod.map id f) (l₁.zip l₂)

Tactic:
rw [← zip_map, map_id]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_preimage (e : E ≃L[𝕜] F) (s : Set F) : dimH (e ⁻¹' s) = dimH s

Proof state:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set F
⊢ dimH (⇑e ⁻¹' s) = dimH s

Tactic:
rw [← e.image_symm_eq_preimage, e.symm.dimH_image]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_singleton : image2 f {a} {b} = {f a b}

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
a : α
b : β
⊢ image2 f {a} {b} = {f a b}

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Star/Conjneg.lean
@[simp] lemma conjneg_pos : 0 < conjneg f ↔ 0 < f

Proof state:
G : Type u_1
R : Type u_2
inst✝³ : AddGroup G
inst✝² : OrderedCommSemiring R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ 0 < conjneg f ↔ 0 < f

Tactic:
simp_rw [lt_iff_le_and_ne, ne_comm, conjneg_nonneg, conjneg_ne_zero]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem natCast_le_cast {m : ℕ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n

Proof state:
K : Type u_5
inst✝ : LinearOrderedField K
m : ℕ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
rw [← cast_le (K := K), cast_natCast]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem get_extract {a : ByteArray} {start stop} (h : i < (a.extract start stop).size) :
    (a.extract start stop)[i] = a[start+i]'(get_extract_aux h)

Proof state:
i : Nat
a : ByteArray
start stop : Nat
h : i < (a.extract start stop).size
⊢ (a.extract start stop)[i] = a[start + i]

Tactic:
simp [getElem_eq_data_getElem]

Result:
no goals
-- Mathlib/RingTheory/Filtration.lean
theorem Ideal.iInf_pow_eq_bot_of_isDomain [IsNoetherianRing R] [IsDomain R] (h : I ≠ ⊤) :
    ⨅ i : ℕ, I ^ i = ⊥

Proof state:
case h.e'_2.h.e'_4.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x✝ : ℕ
⊢ I ^ x✝ = I ^ x✝ • ⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
⊢ ⨅ i, I ^ i = ⊥

Tactic:
convert I.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors (M := R) h

Result:
case h.e'_2.h.e'_4.h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x✝ : ℕ
⊢ I ^ x✝ = I ^ x✝ • ⊤
-- Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
theorem hasStrictDerivAt_log {x : ℂ} (h : x ∈ slitPlane) : HasStrictDerivAt log x⁻¹ x :=
  have h0 : x ≠ 0 := slitPlane_ne_zero h
  expPartialHomeomorph.hasStrictDerivAt_symm h h0 <| by
    simpa [exp_log h0] using hasStrictDerivAt_exp (log x)

Proof state:
x : ℂ
h : x ∈ slitPlane
h0 : x ≠ 0
⊢ HasStrictDerivAt (↑expPartialHomeomorph) x (↑expPartialHomeomorph.symm x)

Tactic:
simpa [exp_log h0] using hasStrictDerivAt_exp (log x)

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem quadratic_reciprocity_one_mod_four {a b : ℕ} (ha : a % 4 = 1) (hb : Odd b) :
    J(a | b) = J(b | a)

Proof state:
a b : ℕ
ha : a % 4 = 1
hb : Odd b
⊢ J(↑a | b) = J(↑b | a)

Tactic:
rw [quadratic_reciprocity (odd_iff.mpr (odd_of_mod_four_eq_one ha)) hb, pow_mul,
  neg_one_pow_div_two_of_one_mod_four ha, one_pow, one_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateRow_add_smul_self (A : Matrix n n R) {i j : n} (hij : i ≠ j) (c : R) :
    det (updateRow A i (A i + c • A j)) = det A

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ (A.updateRow i (A i + c • A j)).det = A.det

Tactic:
simp [det_updateRow_add, det_updateRow_smul,
  det_zero_of_row_eq hij (updateRow_self.trans (updateRow_ne hij.symm).symm)]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem Fintype.coe_image_univ [Fintype α] [DecidableEq β] {f : α → β} :
    ↑(Finset.image f Finset.univ) = Set.range f

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
x : β
⊢ x ∈ ↑(image f univ) ↔ x ∈ Set.range f

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
⊢ ↑(image f univ) = Set.range f

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
x : β
⊢ x ∈ ↑(image f univ) ↔ x ∈ Set.range f
-- Mathlib/Data/Real/EReal.lean
lemma min_neg_neg (x y : EReal) : min (-x) (-y) = -max x y

Proof state:
x y : EReal
⊢ -x ⊓ -y = -(x ⊔ y)

Tactic:
rcases le_total x y with (h | h) <;> simp_all

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_append_pair : ∀ (l : List α) (a b : α),
    formPerm (l ++ [a, b]) = formPerm (l ++ [a]) * swap a b
  | [], _, _ => rfl
  | [_], _, _ => rfl
  | x::y::l, a, b => by
    simpa [mul_assoc] using formPerm_append_pair (y::l) a b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
a b : α
⊢ (x :: y :: l ++ [a, b]).formPerm = (x :: y :: l ++ [a]).formPerm * swap a b

Tactic:
simpa [mul_assoc] using formPerm_append_pair (y::l) a b

Result:
no goals
-- Mathlib/RingTheory/WittVector/Complete.lean
theorem eq_zero_of_p_mul_eq_zero (x : 𝕎 k) (h : x * p = 0) : x = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x * ↑p = 0
⊢ x = 0

Tactic:
rwa [← frobenius_verschiebung, map_eq_zero_iff _ (frobenius_bijective p k).injective,
    map_eq_zero_iff _ (verschiebung_injective p k)] at h

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem _root_.Real.map_toNNReal_atTop : map Real.toNNReal atTop = atTop

Proof state:
⊢ Filter.map Real.toNNReal atTop = atTop

Tactic:
rw [← map_coe_atTop, Function.LeftInverse.filter_map @Real.toNNReal_coe]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem symm {m n : ℕ} (hm : Odd m) (hn : Odd n) : qrSign m n = qrSign n m

Proof state:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ qrSign m n = qrSign n m

Tactic:
rw [neg_one_pow hm hn, neg_one_pow hn hm, mul_comm (m / 2)]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_to_num (n : PosNum) : ↑n = Num.pos n

Proof state:
n : PosNum
⊢ ↑n = pos n

Tactic:
rw [← cast_to_nat, ← of_to_nat n]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem const' (b : β) {K : ℝ≥0} : LipschitzWith K fun _ : α => b := fun x y => by
  simp only [edist_self, zero_le]

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
K : ℝ≥0
x y : α
⊢ edist ((fun x => b) x) ((fun x => b) y) ≤ ↑K * edist x y

Tactic:
simp only [edist_self, zero_le]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem all_iff_not_ex_not (φ : L.BoundedFormula α (n + 1)) :
    φ.all ⇔[T] φ.not.ex.not := fun M v xs => by simp

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α (n + 1)
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (∀'φ ⇔ ∼(∃'∼φ)).Realize v xs

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem catalan_one : catalan 1 = 1

Proof state:
⊢ catalan 1 = 1

Tactic:
simp [catalan_succ]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
theorem opNNNorm_le_bound' (f : E →SL[σ₁₂] F) (M : ℝ≥0) (hM : ∀ x, ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊) :
    ‖f‖₊ ≤ M :=
  opNorm_le_bound' f (zero_le M) fun x hx => hM x <| by rwa [← NNReal.coe_ne_zero]

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
hM : ∀ (x : E), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊
x : E
hx : ‖x‖ ≠ 0
⊢ ‖x‖₊ ≠ 0

Tactic:
rwa [← NNReal.coe_ne_zero]

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem Continuous.div_const (hf : Continuous f) (y : G₀) : Continuous fun x => f x / y

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝³ : DivInvMonoid G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousMul G₀
f : α → G₀
inst✝ : TopologicalSpace α
hf : Continuous f
y : G₀
⊢ Continuous fun x => f x / y

Tactic:
simpa only [div_eq_mul_inv] using hf.mul continuous_const

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem aestronglyMeasurable_zero_measure (f : α → β) :
    AEStronglyMeasurable[m] f (0 : Measure[m₀] α)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEStronglyMeasurable f 0

Tactic:
exact ⟨fun _ => f default, stronglyMeasurable_const, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
a✝ : Nontrivial α
⊢ AEStronglyMeasurable f 0

Tactic:
inhabit α

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEStronglyMeasurable f 0

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
⊢ AEStronglyMeasurable f 0

Tactic:
nontriviality α

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
a✝ : Nontrivial α
⊢ AEStronglyMeasurable f 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_mul_ediv_cancel (a b : Int) (h : b ≠ 0) : -(a * b) / b = -a

Proof state:
a b : Int
h : b ≠ 0
⊢ -(a * b) / b = -a

Tactic:
rw [neg_ediv_of_dvd (Int.dvd_mul_left a b), mul_ediv_cancel _ h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_eq_getValueCast! [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
    [Inhabited (β a)] (h : containsKey a l = true) : getValueCast a l h = getValueCast! a l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
a : α
inst✝ : Inhabited (β a)
h : containsKey a l = true
⊢ getValueCast a l h = getValueCast! a l

Tactic:
rw [getValueCast!_eq_getValueCast?, getValueCast, Option.get_eq_get!]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_hasStrictDerivAt_left (hf : IntervalIntegrable f volume a b)
    (hmeas : StronglyMeasurableAtFilter f (𝓝 a)) (ha : ContinuousAt f a) :
    HasStrictDerivAt (fun u => ∫ x in u..b, f x) (-f a) a

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter f (𝓝 a) volume
ha : ContinuousAt f a
⊢ HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) a

Tactic:
simpa only [← integral_symm] using (integral_hasStrictDerivAt_right hf.symm hmeas ha).neg

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem at_zero : legendreSym p 0 = 0

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p 0 = 0

Tactic:
rw [legendreSym, Int.cast_zero, MulChar.map_zero]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivWithinAt.finset_prod [DecidableEq ι] {x : E}
    (hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x) :
    HasFDerivWithinAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x
⊢ (∑ i ∈ u.attach, (∏ j ∈ u.attach.erase i, g (↑j) x) • proj i).comp (pi fun i => g' ↑i) =
    ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x
x✝ : E
⊢ ((∑ i ∈ u.attach, (∏ j ∈ u.attach.erase i, g (↑j) x) • proj i).comp (pi fun i => g' ↑i)) x✝ =
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x✝
-- Mathlib/Data/Int/Bitwise.lean
theorem testBit_ldiff (m n k) : testBit (ldiff m n) k = (testBit m k && not (testBit n k))

Proof state:
m n : ℤ
k : ℕ
⊢ (m.ldiff n).testBit k = (m.testBit k && !n.testBit k)

Tactic:
rw [← bitwise_diff, testBit_bitwise]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain_of_chain_pmap {S : β → β → Prop} {p : α → Prop} (f : ∀ a, p a → β) {l : List α}
    (hl₁ : ∀ a ∈ l, p a) {a : α} (ha : p a) (hl₂ : Chain S (f a ha) (List.pmap f l hl₁))
    (H : ∀ a b ha hb, S (f a ha) (f b hb) → R a b) : Chain R a l

Proof state:
case nil
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
hl₁ : ∀ (a : α), a ∈ [] → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f [] hl₁)
⊢ Chain R a []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl₁ : ∀ (a : α), a ∈ l → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f l hl₁)
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
⊢ Chain R a l

Tactic:
induction' l with lh lt l_ih generalizing a

Result:
case nil
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
hl₁ : ∀ (a : α), a ∈ [] → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f [] hl₁)
⊢ Chain R a []

case cons
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
lh : α
lt : List α
l_ih : ∀ (hl₁ : ∀ (a : α), a ∈ lt → p a) {a : α} (ha : p a), Chain S (f a ha) (pmap f lt hl₁) → Chain R a lt
hl₁ : ∀ (a : α), a ∈ lh :: lt → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f (lh :: lt) hl₁)
⊢ Chain R a (lh :: lt)

Proof state:
case cons
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b
lh : α
lt : List α
l_ih : ∀ (hl₁ : ∀ (a : α), a ∈ lt → p a) {a : α} (ha : p a), Chain S (f a ha) (pmap f lt hl₁) → Chain R a lt
hl₁ : ∀ (a : α), a ∈ lh :: lt → p a
a : α
ha : p a
hl₂ : Chain S (f a ha) (pmap f (lh :: lt) hl₁)
⊢ Chain R a (lh :: lt)

Tactic:
simp [H _ _ _ _ (rel_of_chain_cons hl₂), l_ih _ _ (chain_of_chain_cons hl₂)]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem comap_top {f : P₁ →ᵃ[k] P₂} : (⊤ : AffineSubspace k P₂).comap f = ⊤

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
⊢ comap f ⊤ = ⊤

Tactic:
rw [AffineSubspace.ext_iff]

Result:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
⊢ ↑(comap f ⊤) = ↑⊤

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
⊢ ↑(comap f ⊤) = ↑⊤

Tactic:
exact preimage_univ (f := f)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashable α]
    (h : m.1.WF) {l : List α} {k : α} :
    m.contains k → getKey? (insertManyIfNewUnit m l).1 k = getKey? m k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k : α
⊢ m.contains k = true → (insertManyIfNewUnit m l).val.getKey? k = m.getKey? k

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKey?_insertListIfNewUnit_of_contains

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
lemma iInf_coe_lt_top : ⨅ i, (f i : WithTop α) < ⊤ ↔ Nonempty ι

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι

Tactic:
rw [lt_top_iff_ne_top, Ne, iInf_coe_eq_top, not_isEmpty_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_def (l : List α) (f : α → List β) : l.flatMap f = flatten (map f l)

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → List β
⊢ flatMap f l = (map f l).flatten

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
lemma adjoin_nonUnitalStarSubalgebra_eq_span (s : NonUnitalStarSubalgebra R A) :
    (adjoin R (s : Set A)).toSubalgebra.toSubmodule = span R {1} ⊔ s.toSubmodule

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : NonUnitalStarSubalgebra R A
⊢ Subalgebra.toSubmodule (adjoin R ↑s).toSubalgebra = span R {1} ⊔ s.toSubmodule

Tactic:
rw [adjoin_eq_span, Submonoid.closure_eq_one_union, span_union,
  ← NonUnitalStarAlgebra.adjoin_eq_span, NonUnitalStarAlgebra.adjoin_eq]

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem prod_assoc_preimage {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    Equiv.prodAssoc α β γ ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
x✝ : (α × β) × γ
⊢ x✝ ∈ ⇑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u ↔ x✝ ∈ (s ×ˢ t) ×ˢ u

Tactic:
simp [and_assoc]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
x✝ : (α × β) × γ
⊢ x✝ ∈ ⇑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u ↔ x✝ ∈ (s ×ˢ t) ×ˢ u
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_diff_Ioc : Iic b \ Ioc a b = Iic (a ⊓ b)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Iic b \ Ioc a b = Iic (a ⊓ b)

Tactic:
rw [diff_eq, compl_Ioc, inter_union_distrib_left, Iic_inter_Iic, ← compl_Iic, inter_compl_self,
  union_empty, min_comm]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem cycleType_inv (σ : Perm α) : σ⁻¹.cycleType = σ.cycleType :=
  cycle_induction_on (P := fun τ : Perm α => τ⁻¹.cycleType = τ.cycleType) σ rfl
    (fun σ hσ => by simp only [hσ.cycleType, hσ.inv.cycleType, support_inv])
    fun σ τ hστ _ hσ hτ => by
      simp only [mul_inv_rev, hστ.cycleType, hστ.symm.inv_left.inv_right.cycleType, hσ, hτ,
        add_comm]

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ✝ σ τ : Perm α
hστ : σ.Disjoint τ
x✝ : σ.IsCycle
hσ : (fun τ => τ⁻¹.cycleType = τ.cycleType) σ
hτ : (fun τ => τ⁻¹.cycleType = τ.cycleType) τ
⊢ (fun τ => τ⁻¹.cycleType = τ.cycleType) (σ * τ)

Tactic:
simp only [mul_inv_rev, hστ.cycleType, hστ.symm.inv_left.inv_right.cycleType, hσ, hτ,
  add_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ✝ σ : Perm α
hσ : σ.IsCycle
⊢ (fun τ => τ⁻¹.cycleType = τ.cycleType) σ

Tactic:
simp only [hσ.cycleType, hσ.inv.cycleType, support_inv]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem iUnion_inf (π₁ π₂ : Prepartition I) : (π₁ ⊓ π₂).iUnion = π₁.iUnion ∩ π₂.iUnion

Proof state:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
⊢ (π₁ ⊓ π₂).iUnion = π₁.iUnion ∩ π₂.iUnion

Tactic:
simp only [inf_def, iUnion_biUnion, iUnion_restrict, ← iUnion_inter, ← iUnion_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem cons_eq_flatten_iff {xs : List (List α)} {y : α} {ys : List α} :
    y :: ys = xs.flatten ↔
      ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ l, l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

Proof state:
α : Type u_1
xs : List (List α)
y : α
ys : List α
⊢ y :: ys = xs.flatten ↔
    ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

Tactic:
rw [eq_comm, flatten_eq_cons_iff]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem rightMoves_neg_cases {x : PGame} (k) {P : (-x).RightMoves → Prop}
    (h : ∀ i, P <| toRightMovesNeg i) :
    P k

Proof state:
x : PGame
k : (-x).RightMoves
P : (-x).RightMoves → Prop
h : ∀ (i : x.LeftMoves), P (toRightMovesNeg i)
⊢ P (toRightMovesNeg (toRightMovesNeg.symm k))

Tactic:
exact h _

Result:
no goals

Proof state:
x : PGame
k : (-x).RightMoves
P : (-x).RightMoves → Prop
h : ∀ (i : x.LeftMoves), P (toRightMovesNeg i)
⊢ P k

Tactic:
rw [← toRightMovesNeg.apply_symm_apply k]

Result:
x : PGame
k : (-x).RightMoves
P : (-x).RightMoves → Prop
h : ∀ (i : x.LeftMoves), P (toRightMovesNeg i)
⊢ P (toRightMovesNeg (toRightMovesNeg.symm k))