harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_length_eq_iff {l : List (Option α)} :
    l.reduceOption.length = l.length ↔ ∀ x ∈ l, Option.isSome x

Proof state:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true

Tactic:
rw [reduceOption_length_eq, List.filter_length_eq_length]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem xgcd_val (x y) : xgcd x y = (gcdA x y, gcdB x y)

Proof state:
x y : ℕ
⊢ x.xgcd y = ((x.xgcd y).1, (x.xgcd y).2)

Tactic:
cases xgcd x y

Result:
case mk
x y : ℕ
fst✝ snd✝ : ℤ
⊢ (fst✝, snd✝) = ((fst✝, snd✝).1, (fst✝, snd✝).2)

Proof state:
case mk
x y : ℕ
fst✝ snd✝ : ℤ
⊢ (fst✝, snd✝) = ((fst✝, snd✝).1, (fst✝, snd✝).2)

Tactic:
rfl

Result:
no goals

Proof state:
x y : ℕ
⊢ x.xgcd y = (x.gcdA y, x.gcdB y)

Tactic:
unfold gcdA gcdB

Result:
x y : ℕ
⊢ x.xgcd y = ((x.xgcd y).1, (x.xgcd y).2)
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_map [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂)
    (p : MvPolynomial σ R) : eval₂ φ g (map f p) = eval₂ (φ.comp f) g p

Proof state:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ eval₂ φ g ((map f) p) = eval₂ (φ.comp f) g p

Tactic:
rw [← eval_map, ← eval_map, map_map]

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem existsUnique_pos_generator (h₀ : 0 < d) (hd : ¬IsSquare d) :
    ∃! a₁ : Solution₁ d,
      1 < a₁.x ∧ 0 < a₁.y ∧ ∀ a : Solution₁ d, ∃ n : ℤ, a = a₁ ^ n ∨ a = -a₁ ^ n

Proof state:
case intro.intro.intro.intro.intro.inl.inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (a₁ ^ (-1)).x
Hy : 0 < (a₁ ^ (-1)).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ (-1)) ^ n ∨ a = -(a₁ ^ (-1)) ^ n
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
⊢ a₁ ^ (-1) = a₁

Tactic:
rw [zpow_neg_one, y_inv, lt_neg, neg_zero] at Hy

Result:
case intro.intro.intro.intro.intro.inl.inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (a₁ ^ (-1)).x
Hy : a₁.y < 0
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ (-1)) ^ n ∨ a = -(a₁ ^ (-1)) ^ n
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
⊢ a₁ ^ (-1) = a₁

Proof state:
case intro.intro.intro.intro.intro.inl.inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (a₁ ^ (-1)).x
Hy : a₁.y < 0
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ (-1)) ^ n ∨ a = -(a₁ ^ (-1)) ^ n
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
⊢ a₁ ^ (-1) = a₁

Tactic:
exact False.elim (lt_irrefl _ <| ha₁.2.1.trans Hy)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : (a₁ ^ n₂).x < -1
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁

Tactic:
have := (x_zpow_pos (zero_lt_one.trans ha₁.1) n₂).trans Hx

Result:
case intro.intro.intro.intro.intro.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : (a₁ ^ n₂).x < -1
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
this : 0 < -1
⊢ -a₁ ^ n₂ = a₁

Proof state:
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
a : Solution₁ d
Hx : 1 < a.x
Hy : 0 < a.y
H : ∀ (a_1 : Solution₁ d), ∃ n, a_1 = a ^ n ∨ a_1 = -a ^ n
⊢ a = a₁

Tactic:
obtain ⟨n₁, hn₁⟩ := H a₁

Result:
case intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
a : Solution₁ d
Hx : 1 < a.x
Hy : 0 < a.y
H : ∀ (a_1 : Solution₁ d), ∃ n, a_1 = a ^ n ∨ a_1 = -a ^ n
n₁ : ℤ
hn₁ : a₁ = a ^ n₁ ∨ a₁ = -a ^ n₁
⊢ a = a₁

Proof state:
case intro.intro.intro.intro.intro.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (-a₁ ^ n₂).x
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁

Tactic:
rw [x_neg, lt_neg] at Hx

Result:
case intro.intro.intro.intro.intro.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : (a₁ ^ n₂).x < -1
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_eq_top_iff_of_symmDiff (hμst : μ (s ∆ t) ≠ ∞) : μ s = ∞ ↔ μ t = ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
u v : Set α
hμuv : μ (u ∆ v) ≠ ⊤
hμu : μ u = ⊤
hμv : μ v ≠ ⊤
⊢ ⊤ = μ u - μ v

Tactic:
rw [ENNReal.sub_eq_top_iff.2 ⟨hμu, hμv⟩]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
u v : Set α
hμuv : μ (u ∆ v) ≠ ⊤
hμu : μ u = ⊤
hμv : μ v ≠ ⊤
⊢ ⊤ ≤ μ (u \ v ∪ v \ u)

Tactic:
calc
  ∞ = μ u - μ v := by rw [ENNReal.sub_eq_top_iff.2 ⟨hμu, hμv⟩]
  _ ≤ μ (u \ v) := le_measure_diff
  _ ≤ μ (u \ v ∪ v \ u) := measure_mono subset_union_left

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
u v : Set α
hμuv : μ (u ∆ v) ≠ ⊤
hμu : μ u = ⊤
hμv : μ v ≠ ⊤
⊢ μ (u ∆ v) = ⊤

Tactic:
rw [Set.symmDiff_def, eq_top_iff]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
u v : Set α
hμuv : μ (u ∆ v) ≠ ⊤
hμu : μ u = ⊤
hμv : μ v ≠ ⊤
⊢ ⊤ ≤ μ (u \ v ∪ v \ u)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
⊢ ∀ (u v : Set α), μ (u ∆ v) ≠ ⊤ → μ u = ⊤ → μ v = ⊤

Tactic:
intro u v hμuv hμu

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
u v : Set α
hμuv : μ (u ∆ v) ≠ ⊤
hμu : μ u = ⊤
⊢ μ v = ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
u v : Set α
hμuv : μ (u ∆ v) ≠ ⊤
hμu : μ u = ⊤
hμv : μ v ≠ ⊤
⊢ False

Tactic:
apply hμuv

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
u v : Set α
hμuv : μ (u ∆ v) ≠ ⊤
hμu : μ u = ⊤
hμv : μ v ≠ ⊤
⊢ μ (u ∆ v) = ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
⊢ μ s = ⊤ ↔ μ t = ⊤

Tactic:
suffices h : ∀ u v, μ (u ∆ v) ≠ ∞ → μ u = ∞ → μ v = ∞
  from ⟨h s t hμst, h t s (symmDiff_comm s t ▸ hμst)⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
⊢ ∀ (u v : Set α), μ (u ∆ v) ≠ ⊤ → μ u = ⊤ → μ v = ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
u v : Set α
hμuv : μ (u ∆ v) ≠ ⊤
hμu : μ u = ⊤
⊢ μ v = ⊤

Tactic:
by_contra! hμv

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ⊤
u v : Set α
hμuv : μ (u ∆ v) ≠ ⊤
hμu : μ u = ⊤
hμv : μ v ≠ ⊤
⊢ False
-- Mathlib/Data/List/TakeWhile.lean
theorem takeWhile_eq_self_iff : takeWhile p l = l ↔ ∀ x ∈ l, p x

Proof state:
case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true

Tactic:
by_cases hp : p x <;> simp [hp, IH]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (x : α), x ∈ [] → p x = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
induction' l with x xs IH

Result:
case nil
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (x : α), x ∈ [] → p x = true

case cons
α : Type u_1
p : α → Bool
l : List α
x : α
xs : List α
IH : takeWhile p xs = xs ↔ ∀ (x : α), x ∈ xs → p x = true
⊢ takeWhile p (x :: xs) = x :: xs ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = true
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
protected lemma norm_nonneg {x : E} : 0 ≤ ‖x‖

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
⊢ 0 ≤ ‖x‖

Tactic:
simp [norm_eq_sqrt_norm_inner_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem negSucc_eq' (m : Nat) : -[m+1] = -m - 1

Proof state:
m : Nat
⊢ -[m+1] = -↑m - 1

Tactic:
simp only [negSucc_eq, Int.neg_add]

Result:
m : Nat
⊢ -↑m + -1 = -↑m - 1

Proof state:
m : Nat
⊢ -↑m + -1 = -↑m - 1

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
theorem limsup_measure_compl_le_of_le_liminf_measure {ι : Type*} {L : Filter ι} {μ : Measure Ω}
    {μs : ι → Measure Ω} [IsProbabilityMeasure μ] [∀ i, IsProbabilityMeasure (μs i)] {E : Set Ω}
    (E_mble : MeasurableSet E) (h : μ E ≤ L.liminf fun i ↦ μs i E) :
    (L.limsup fun i ↦ μs i Eᶜ) ≤ μ Eᶜ

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : μ E ≤ liminf (fun i => (μs i) E) L
hne : L.NeBot
⊢ μ Eᶜ = 1 - μ E

Tactic:
simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
@[simp]
lemma turanGraph_zero : turanGraph n 0 = ⊤

Proof state:
n : ℕ
⊢ turanGraph n 0 = ⊤

Tactic:
ext a b

Result:
case Adj.h.h.a
n : ℕ
a b : Fin n
⊢ (turanGraph n 0).Adj a b ↔ ⊤.Adj a b

Proof state:
case Adj.h.h.a
n : ℕ
a b : Fin n
⊢ (turanGraph n 0).Adj a b ↔ ⊤.Adj a b

Tactic:
simp_rw [turanGraph, top_adj, Nat.mod_zero, not_iff_not, Fin.val_inj]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_to_znum : ∀ n : PosNum, (n : ZNum) = ZNum.pos n
  | 1 => rfl
  | bit0 p => by
      have := congr_arg ZNum.bit0 (cast_to_znum p)
      rwa [← ZNum.bit0_of_bit0] at this
  | bit1 p => by
      have := congr_arg ZNum.bit1 (cast_to_znum p)
      rwa [← ZNum.bit1_of_bit1] at this

Proof state:
p : PosNum
this : (↑p).bit0 = (ZNum.pos p).bit0
⊢ ↑p.bit0 = ZNum.pos p.bit0

Tactic:
rwa [← ZNum.bit0_of_bit0] at this

Result:
no goals

Proof state:
p : PosNum
this : (↑p).bit1 = (ZNum.pos p).bit1
⊢ ↑p.bit1 = ZNum.pos p.bit1

Tactic:
rwa [← ZNum.bit1_of_bit1] at this

Result:
no goals

Proof state:
p : PosNum
⊢ ↑p.bit0 = ZNum.pos p.bit0

Tactic:
have := congr_arg ZNum.bit0 (cast_to_znum p)

Result:
p : PosNum
this : (↑p).bit0 = (ZNum.pos p).bit0
⊢ ↑p.bit0 = ZNum.pos p.bit0

Proof state:
p : PosNum
⊢ ↑p.bit1 = ZNum.pos p.bit1

Tactic:
have := congr_arg ZNum.bit1 (cast_to_znum p)

Result:
p : PosNum
this : (↑p).bit1 = (ZNum.pos p).bit1
⊢ ↑p.bit1 = ZNum.pos p.bit1
-- Mathlib/Order/Interval/Set/Image.lean
private lemma image_subtype_val_Ixx_Iix {p q r : α → α → Prop} {a b : α} (c : {x // p a x ∧ q x b})
    (h : ∀ {x}, r x c → q x b) :
    Subtype.val '' {y : {x // p a x ∧ q x b} | r y.1 c.1} = {y : α | p a y ∧ r y c.1} :=
  (Subtype.image_preimage_val {x | p a x ∧ q x b} {y | r y c.1}).trans <| by
    ext; simp (config := { contextual := true}) [h]

Proof state:
case h
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r x ↑c → q x b
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r y ↑c} ↔ x✝ ∈ {y | p a y ∧ r y ↑c}

Tactic:
simp (config := { contextual := true}) [h]

Result:
no goals

Proof state:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r x ↑c → q x b
⊢ {x | p a x ∧ q x b} ∩ {y | r y ↑c} = {y | p a y ∧ r y ↑c}

Tactic:
ext

Result:
case h
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r x ↑c → q x b
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r y ↑c} ↔ x✝ ∈ {y | p a y ∧ r y ↑c}
-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
lemma truncGE'Map_f_eq {i : ι} (hi : ¬ e.BoundaryGE i) {i' : ι'} (h : e.f i = i') :
    (truncGE'Map φ e).f i =
      (K.truncGE'XIso e h hi).hom ≫ φ.f i' ≫ (L.truncGE'XIso e h hi).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ (truncGE'Map φ e).f i = (K.truncGE'XIso e ⋯ hi).hom ≫ φ.f (e.f i) ≫ (L.truncGE'XIso e ⋯ hi).inv

Tactic:
exact dif_neg hi

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
i' : ι'
h : e.f i = i'
⊢ (truncGE'Map φ e).f i = (K.truncGE'XIso e h hi).hom ≫ φ.f i' ≫ (L.truncGE'XIso e h hi).inv

Tactic:
subst h

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ (truncGE'Map φ e).f i = (K.truncGE'XIso e ⋯ hi).hom ≫ φ.f (e.f i) ≫ (L.truncGE'XIso e ⋯ hi).inv
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem const_max (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => max a (f x)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz fun x => a ⊔ f x

Tactic:
simpa [max_comm] using (hf.max_const a)

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem IsPathConnected.image' (hF : IsPathConnected F)
    {f : X → Y} (hf : ContinuousOn f F) : IsPathConnected (f '' F)

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ IsPathConnected (f '' F)

Tactic:
use f x, mem_image_of_mem f x_in

Result:
case right
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ ∀ {y : Y}, y ∈ f '' F → JoinedIn (f '' F) (f x) y

Proof state:
case right.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ JoinedIn (f '' F) (f x) (f y)

Tactic:
refine ⟨(hx y_in).somePath.map' ?_, fun t ↦ ⟨_, (hx y_in).somePath_mem t, rfl⟩⟩

Result:
case right.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ ContinuousOn f (range ⇑⋯.somePath)

Proof state:
case right
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ ∀ {y : Y}, y ∈ f '' F → JoinedIn (f '' F) (f x) y

Tactic:
rintro _ ⟨y, y_in, rfl⟩

Result:
case right.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ JoinedIn (f '' F) (f x) (f y)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
hF : IsPathConnected F
f : X → Y
hf : ContinuousOn f F
⊢ IsPathConnected (f '' F)

Tactic:
rcases hF with ⟨x, x_in, hx⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ IsPathConnected (f '' F)

Proof state:
case right.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ {y : X}, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ ContinuousOn f (range ⇑⋯.somePath)

Tactic:
exact hf.mono (range_subset_iff.2 (hx y_in).somePath_mem)

Result:
no goals
-- Mathlib/Combinatorics/Additive/CauchyDavenport.lean
/-- The **Cauchy-Davenport Theorem**. If `s`, `t` are nonempty sets in $$ℤ/pℤ$$, then the size of
`s + t` is lower-bounded by `|s| + |t| - 1`, unless this quantity is greater than `p`. -/
lemma ZMod.cauchy_davenport {p : ℕ} (hp : p.Prime) {s t : Finset (ZMod p)} (hs : s.Nonempty)
    (ht : t.Nonempty) : min p (#s + #t - 1) ≤ #(s + t)

Proof state:
p : ℕ
hp : Nat.Prime p
s t : Finset (ZMod p)
hs : s.Nonempty
ht : t.Nonempty
⊢ p ⊓ (#s + #t - 1) ≤ #(s + t)

Tactic:
simpa only [ZMod.minOrder_of_prime hp, min_le_iff, Nat.cast_le]
  using cauchy_davenport_minOrder_add hs ht

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem pmap_cons {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : Vector α n)
    (hp : ∀ x ∈ (cons a v).toList, p x) :
    (cons a v).pmap f hp = cons (f a (by
      simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
      exact hp.1))
      (v.pmap f (by
        simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
        exact hp.2)) := rfl

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : p a ∧ ∀ a ∈ v.toList, p a
⊢ ∀ x ∈ v.toList, p x

Tactic:
exact hp.2

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ x ∈ (a ::ᵥ v).toList, p x
⊢ ∀ x ∈ v.toList, p x

Tactic:
simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : p a ∧ ∀ a ∈ v.toList, p a
⊢ ∀ x ∈ v.toList, p x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : ∀ x ∈ (a ::ᵥ v).toList, p x
⊢ p a

Tactic:
simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : p a ∧ ∀ a ∈ v.toList, p a
⊢ p a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
hp : p a ∧ ∀ a ∈ v.toList, p a
⊢ p a

Tactic:
exact hp.1

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Mat.lean
theorem id_apply_self (M : Mat_ C) (i : M.ι) : (𝟙 M : Hom M M) i i = 𝟙 _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i : M.ι
⊢ 𝟙 M i i = 𝟙 (M.X i)

Tactic:
simp [id_apply]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Bounded.to_sep {t₁ t₂ o₁ o₂} {x : α}
    (h₁ : Bounded t₁ o₁ (x : WithTop α)) (h₂ : Bounded t₂ (x : WithBot α) o₂) :
    t₁.All fun y => t₂.All fun z : α => y < z

Proof state:
α : Type u_1
inst✝ : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ ↑x
h₂ : t₂.Bounded (↑x) o₂
⊢ All (fun y => All (fun z => y < z) t₂) t₁

Tactic:
refine h₁.mem_lt.imp fun y yx => ?_

Result:
α : Type u_1
inst✝ : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ ↑x
h₂ : t₂.Bounded (↑x) o₂
y : α
yx : y < x
⊢ All (fun z => y < z) t₂

Proof state:
α : Type u_1
inst✝ : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ ↑x
h₂ : t₂.Bounded (↑x) o₂
y : α
yx : y < x
⊢ All (fun z => y < z) t₂

Tactic:
exact h₂.mem_gt.imp fun z xz => lt_trans yx xz

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.of_apply₂ (hf : ∀ a, ωScottContinuous (f · a)) : ωScottContinuous f :=
  ωScottContinuous.of_monotone_map_ωSup
    ⟨fun _ _ h a ↦ (hf a).monotone h, fun c ↦ by ext a; apply (hf a).map_ωSup c⟩

Proof state:
case h
α : Type u_2
γ : Type u_4
β : α → Type u_6
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (a : α), ωScottContinuous fun x => f x a
c : Chain γ
a : α
⊢ f (ωSup c) a = ωSup (c.map { toFun := f, monotone' := ⋯ }) a

Tactic:
apply (hf a).map_ωSup c

Result:
no goals

Proof state:
α : Type u_2
γ : Type u_4
β : α → Type u_6
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (a : α), ωScottContinuous fun x => f x a
c : Chain γ
⊢ f (ωSup c) = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
ext a

Result:
case h
α : Type u_2
γ : Type u_4
β : α → Type u_6
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (a : α), ωScottContinuous fun x => f x a
c : Chain γ
a : α
⊢ f (ωSup c) a = ωSup (c.map { toFun := f, monotone' := ⋯ }) a
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem intervalIntegrable_norm_iff {f : ℝ → E} {μ : Measure ℝ} {a b : ℝ}
    (hf : AEStronglyMeasurable f (μ.restrict (Ι a b))) :
    IntervalIntegrable (fun t => ‖f t‖) μ a b ↔ IntervalIntegrable f μ a b

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ Integrable (fun t => ‖f t‖) (μ.restrict (Ι a b)) ↔ Integrable f (μ.restrict (Ι a b))

Tactic:
exact integrable_norm_iff hf

Result:
no goals

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ IntervalIntegrable (fun t => ‖f t‖) μ a b ↔ IntervalIntegrable f μ a b

Tactic:
simp_rw [intervalIntegrable_iff, IntegrableOn]

Result:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ Integrable (fun t => ‖f t‖) (μ.restrict (Ι a b)) ↔ Integrable f (μ.restrict (Ι a b))
-- Mathlib/Order/Filter/Finite.lean
theorem mem_iInf_of_finite {ι : Type*} [Finite ι] {α : Type*} {f : ι → Filter α} (s) :
    (s ∈ ⨅ i, f i) ↔ ∃ t : ι → Set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i

Proof state:
ι : Type u_2
inst✝ : Finite ι
α : Type u_3
f : ι → Filter α
s : Set α
⊢ (∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i) → s ∈ ⨅ i, f i

Tactic:
rintro ⟨t, ht, rfl⟩

Result:
case intro.intro
ι : Type u_2
inst✝ : Finite ι
α : Type u_3
f : ι → Filter α
t : ι → Set α
ht : ∀ (i : ι), t i ∈ f i
⊢ ⋂ i, t i ∈ ⨅ i, f i

Proof state:
ι : Type u_2
inst✝ : Finite ι
α : Type u_3
f : ι → Filter α
s : Set α
⊢ s ∈ ⨅ i, f i ↔ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i

Tactic:
refine ⟨exists_iInter_of_mem_iInf, ?_⟩

Result:
ι : Type u_2
inst✝ : Finite ι
α : Type u_3
f : ι → Filter α
s : Set α
⊢ (∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i) → s ∈ ⨅ i, f i

Proof state:
case intro.intro
ι : Type u_2
inst✝ : Finite ι
α : Type u_3
f : ι → Filter α
t : ι → Set α
ht : ∀ (i : ι), t i ∈ f i
⊢ ⋂ i, t i ∈ ⨅ i, f i

Tactic:
exact iInter_mem.2 fun i => mem_iInf_of_mem i (ht i)

Result:
no goals