harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem dart_fst_mem_support_of_mem_darts {u v : V} :
    ∀ (p : G.Walk u v) {d : G.Dart}, d ∈ p.darts → d.fst ∈ p.support
  | cons h p', d, hd => by
    simp only [support_cons, darts_cons, List.mem_cons] at hd ⊢
    rcases hd with (rfl | hd)
    · exact Or.inl rfl
    · exact Or.inr (dart_fst_mem_support_of_mem_darts _ hd)

Proof state:
case inr
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
d : G.Dart
hd : d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support

Tactic:
exact Or.inr (dart_fst_mem_support_of_mem_darts _ hd)

Result:
no goals

Proof state:
case inl
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
⊢ { toProd := (u, v✝), adj := h }.toProd.1 = u ∨ { toProd := (u, v✝), adj := h }.toProd.1 ∈ p'.support

Tactic:
exact Or.inl rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
d : G.Dart
hd : d ∈ (cons h p').darts
⊢ d.toProd.1 ∈ (cons h p').support

Tactic:
simp only [support_cons, darts_cons, List.mem_cons] at hd ⊢

Result:
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
d : G.Dart
hd : d = { toProd := (u, v✝), adj := h } ∨ d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support

Proof state:
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
d : G.Dart
hd : d = { toProd := (u, v✝), adj := h } ∨ d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support

Tactic:
rcases hd with (rfl | hd)

Result:
case inl
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
⊢ { toProd := (u, v✝), adj := h }.toProd.1 = u ∨ { toProd := (u, v✝), adj := h }.toProd.1 ∈ p'.support

case inr
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p' : G.Walk v✝ v
d : G.Dart
hd : d ∈ p'.darts
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_apply_right (a : α) : toIcoMod hp a (a + p) = a

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ z, a + p = a + z • p

Tactic:
exact ⟨lt_add_of_pos_right _ hp, 1, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIcoMod hp a (a + p) = a

Tactic:
rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ z, a + p = a + z • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p = a + 1 • p

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem ball_normSeminorm : (normSeminorm 𝕜 E).ball = Metric.ball

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ (normSeminorm 𝕜 E).ball = Metric.ball

Tactic:
ext x r y

Result:
case h.h.h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ (normSeminorm 𝕜 E).ball x r ↔ y ∈ Metric.ball x r

Proof state:
case h.h.h
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ (normSeminorm 𝕜 E).ball x r ↔ y ∈ Metric.ball x r

Tactic:
simp only [Seminorm.mem_ball, Metric.mem_ball, coe_normSeminorm, dist_eq_norm]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
lemma range_domRestrict_le_range [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (S : Submodule R M) :
    LinearMap.range (f.domRestrict S) ≤ LinearMap.range f

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
⊢ range (f.domRestrict S) ≤ range f

Tactic:
rintro x ⟨⟨y, hy⟩, rfl⟩

Result:
case intro.mk
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
y : M
hy : y ∈ S
⊢ (f.domRestrict S) ⟨y, hy⟩ ∈ range f

Proof state:
case intro.mk
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
y : M
hy : y ∈ S
⊢ (f.domRestrict S) ⟨y, hy⟩ ∈ range f

Tactic:
exact LinearMap.mem_range_self f y

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α) :
    countP p (filterMap f l) = countP (fun a => ((f a).map p).getD false) l

Proof state:
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
l : List α
⊢ (filterMap (fun x => Option.filter p (f x)) l).length =
    (filterMap (Option.guard fun x => (Option.map p (f x)).getD false = true) l).length

Tactic:
simp only [length_filterMap_eq_countP]

Result:
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
l : List α
⊢ countP (fun a => (Option.filter p (f a)).isSome) l =
    countP (fun a => (Option.guard (fun x => (Option.map p (f x)).getD false = true) a).isSome) l

Proof state:
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
l : List α
⊢ countP p (filterMap f l) = countP (fun a => (Option.map p (f a)).getD false) l

Tactic:
simp only [countP_eq_length_filter, filter_filterMap, ← filterMap_eq_filter]

Result:
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
l : List α
⊢ (filterMap (fun x => Option.filter p (f x)) l).length =
    (filterMap (Option.guard fun x => (Option.map p (f x)).getD false = true) l).length

Proof state:
case e_p.h
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
l : List α
a : α
⊢ (Option.filter p (f a)).isSome = (Option.guard (fun x => (Option.map p (f x)).getD false = true) a).isSome

Tactic:
simp +contextual [Option.getD_eq_iff, Option.isSome_eq_isSome]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
l : List α
⊢ countP (fun a => (Option.filter p (f a)).isSome) l =
    countP (fun a => (Option.guard (fun x => (Option.map p (f x)).getD false = true) a).isSome) l

Tactic:
congr

Result:
case e_p
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
l : List α
⊢ (fun a => (Option.filter p (f a)).isSome) = fun a =>
    (Option.guard (fun x => (Option.map p (f x)).getD false = true) a).isSome

Proof state:
case e_p
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
l : List α
⊢ (fun a => (Option.filter p (f a)).isSome) = fun a =>
    (Option.guard (fun x => (Option.map p (f x)).getD false = true) a).isSome

Tactic:
ext a

Result:
case e_p.h
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Option β
l : List α
a : α
⊢ (Option.filter p (f a)).isSome = (Option.guard (fun x => (Option.map p (f x)).getD false = true) a).isSome
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive (attr := simp)]
lemma isMulFreimanIso_zero_iff : IsMulFreimanIso 0 A B f ↔ BijOn f A B :=
  ⟨fun h => h.bijOn, fun h => ⟨h, by aesop⟩⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
h : BijOn f A B
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 0 → t.card = 0 → ((map f s).prod = (map f t).prod ↔ s.prod = t.prod)

Tactic:
aesop

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean
private lemma hurwitzZeta_neg_two_mul_nat (hk : k ≠ 0) (hx : x ∈ Icc (0 : ℝ) 1) :
    hurwitzZeta x (-(2 * k)) = -1 / (2 * k + 1) *
      ((Polynomial.bernoulli (2 * k + 1)).map (algebraMap ℚ ℂ)).eval (x : ℂ)

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZeta (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
suffices hurwitzZetaEven x (-(2 * k)) = 0 by
  rw [hurwitzZeta, this, zero_add, hurwitzZetaOdd_neg_two_mul_nat hk hx]

Result:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZetaEven (↑x) (-(2 * ↑k)) = 0

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaEven (↑x) (-(2 * ↑k)) = 0
⊢ hurwitzZeta (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
rw [hurwitzZeta, this, zero_add, hurwitzZetaOdd_neg_two_mul_nat hk hx]

Result:
no goals

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZetaEven (↑x) (-(2 * ↑k)) = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hk

Result:
case intro
x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaEven (↑x) (-(2 * ↑k.succ)) = 0

Proof state:
case intro
x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaEven (↑x) (-(2 * ↑k.succ)) = 0

Tactic:
simpa using hurwitzZetaEven_neg_two_mul_nat_add_one x k

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).size ≤ m.size + 1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).size ≤ m.size + 1

Tactic:
simp_to_raw using Raw₀.size_alter_le_size

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem powHalf_moveLeft (n i) : (powHalf n).moveLeft i = 0

Proof state:
n : ℕ
i : (powHalf n).LeftMoves
⊢ (powHalf n).moveLeft i = 0

Tactic:
cases n <;> cases i <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Extension.lean
@[simp]
lemma Cotangent.map_id :
    Cotangent.map (.id P) = LinearMap.id

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ map (Hom.id P) = LinearMap.id

Tactic:
ext x

Result:
case h.e
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
⊢ ((map (Hom.id P)) x).val = (LinearMap.id x).val

Proof state:
case h.e.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
⊢ ((map (Hom.id P)) (mk x)).val = (LinearMap.id (mk x)).val

Tactic:
simp only [map_mk, Hom.toAlgHom_id, AlgHom.coe_id, id_eq, Subtype.coe_eta, val_mk,
  LinearMap.id_coe]

Result:
no goals

Proof state:
case h.e
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
⊢ ((map (Hom.id P)) x).val = (LinearMap.id x).val

Tactic:
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x

Result:
case h.e.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
⊢ ((map (Hom.id P)) (mk x)).val = (LinearMap.id (mk x)).val
-- Mathlib/Data/Matroid/Basic.lean
lemma insert_isBase_of_insert_indep {M : Matroid α} {I : Set α} {e f : α}
    (he : e ∉ I) (hf : f ∉ I) (heI : M.IsBase (insert e I)) (hfI : M.Indep (insert f I)) :
    M.IsBase (insert f I)

Proof state:
case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.IsBase (insert f I)

Tactic:
simpa [diff_singleton_eq_self he, hfI]
  using heI.exchange_isBase_of_indep (e := e) (f := f) (by simp [hef.symm, hf])

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ f ∉ insert e I

Tactic:
simp [hef.symm, hf]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
⊢ M.IsBase (insert f I)

Tactic:
obtain rfl | hef := eq_or_ne e f

Result:
case inl
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∉ I
heI : M.IsBase (insert e I)
hf : e ∉ I
hfI : M.Indep (insert e I)
⊢ M.IsBase (insert e I)

case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.IsBase (insert f I)

Proof state:
case inl
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∉ I
heI : M.IsBase (insert e I)
hf : e ∉ I
hfI : M.Indep (insert e I)
⊢ M.IsBase (insert e I)

Tactic:
assumption

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem arrow_congr {A : C} (X Y : Subobject A) (h : X = Y) :
    eqToHom (congr_arg (fun X : Subobject A => (X : C)) h) ≫ Y.arrow = X.arrow

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A : C
X Y : Subobject A
⊢ eqToHom ⋯ ≫ X.arrow = X.arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A : C
X Y : Subobject A
h : X = Y
⊢ eqToHom ⋯ ≫ Y.arrow = X.arrow

Tactic:
induction h

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A : C
X Y : Subobject A
⊢ eqToHom ⋯ ≫ X.arrow = X.arrow
-- Mathlib/Topology/Constructions.lean
lemma Topology.IsInducing.prodMap {f : X → Y} {g : Z → W} (hf : IsInducing f) (hg : IsInducing g) :
    IsInducing (Prod.map f g) :=
  isInducing_iff_nhds.2 fun (x, z) => by simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap,
    hg.nhds_eq_comap, prod_comap_comap_eq]

Proof state:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x✝ : X × Z
x : X
z : Z
⊢ 𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))

Tactic:
simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap,
hg.nhds_eq_comap, prod_comap_comap_eq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem t'_snd_fst_snd (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ pullback.snd _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ pullback.snd (𝒰.map j ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g

Tactic:
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc,
  pullbackRightPullbackFstIso_inv_fst_assoc, pullback.lift_fst_assoc, t_fst_snd,
  pullbackRightPullbackFstIso_hom_fst_assoc]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coe_eq_zero_iff : (φ : PowerSeries R) = 0 ↔ φ = 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
φ : R[X]
⊢ ↑φ = 0 ↔ φ = 0

Tactic:
rw [← coe_zero, coe_inj]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem imaginaryPart_I_smul (a : A) : ℑ (I • a) = ℜ a

Proof state:
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℑ (I • a)) = ↑(ℜ a)

Tactic:
rw [realPart_apply_coe, imaginaryPart_apply_coe, smul_comm]

Result:
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ 2⁻¹ • -I • (I • a - star (I • a)) = 2⁻¹ • (a + star a)

Proof state:
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ 2⁻¹ • -I • (I • a - star (I • a)) = 2⁻¹ • (a + star a)

Tactic:
simp [← smul_assoc]

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ℑ (I • a) = ℜ a

Tactic:
ext

Result:
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℑ (I • a)) = ↑(ℜ a)
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem ωSup_iterate_le_prefixedPoint (h : x ≤ f x) {a : α}
    (h_a : f a ≤ a) (h_x_le_a : x ≤ a) :
    ωSup (iterateChain f x h) ≤ a

Proof state:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
⊢ ∀ (i : ℕ), (iterateChain (↑f) x h) i ≤ a

Tactic:
intro n

Result:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
⊢ (iterateChain (↑f) x h) n ≤ a

Proof state:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
⊢ (iterateChain (↑f) x h) n ≤ a

Tactic:
induction n with
| zero => exact h_x_le_a
| succ n h_ind =>
  have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
    Function.iterate_succ_apply' ..
  rw [this]
  exact le_trans (f.monotone h_ind) h_a

Result:
no goals

Proof state:
case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ (iterateChain (↑f) x h) (n + 1) ≤ a

Tactic:
rw [this]

Result:
case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ f ((iterateChain (↑f) x h) n) ≤ a

Proof state:
case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ f ((iterateChain (↑f) x h) n) ≤ a

Tactic:
exact le_trans (f.monotone h_ind) h_a

Result:
no goals

Proof state:
case a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
⊢ (iterateChain (↑f) x h) 0 ≤ a

Tactic:
exact h_x_le_a

Result:
no goals

Proof state:
case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
⊢ (iterateChain (↑f) x h) (n + 1) ≤ a

Tactic:
have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
  Function.iterate_succ_apply' ..

Result:
case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ (iterateChain (↑f) x h) (n + 1) ≤ a

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Tactic:
apply ωSup_le

Result:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
⊢ ∀ (i : ℕ), (iterateChain (↑f) x h) i ≤ a
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma rnDeriv_of_not_haveLebesgueDecomposition (h : ¬ HaveLebesgueDecomposition μ ν) :
    μ.rnDeriv ν = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.rnDeriv ν = 0

Tactic:
rw [rnDeriv, dif_neg h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_X_sub_C (r : R) : roots (X - C r) = {r}

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ (X - C r).roots = {r}

Tactic:
ext s

Result:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r s : R
⊢ count s (X - C r).roots = count s {r}

Proof state:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r s : R
⊢ count s (X - C r).roots = count s {r}

Tactic:
rw [count_roots, rootMultiplicity_X_sub_C, count_singleton]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ (X - C r).roots = {r}

Tactic:
classical
ext s
rw [count_roots, rootMultiplicity_X_sub_C, count_singleton]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal_map (M : o → Matrix m n α) (f : α → β) (hf : f 0 = 0) :
    (blockDiagonal M).map f = blockDiagonal fun k => (M k).map f

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
j✝ : n × o
⊢ (blockDiagonal M).map f i✝ j✝ = blockDiagonal (fun k => (M k).map f) i✝ j✝

Tactic:
simp only [map_apply, blockDiagonal_apply, eq_comm]

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
j✝ : n × o
⊢ f (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0) = if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else 0

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
⊢ (blockDiagonal M).map f = blockDiagonal fun k => (M k).map f

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
j✝ : n × o
⊢ (blockDiagonal M).map f i✝ j✝ = blockDiagonal (fun k => (M k).map f) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
j✝ : n × o
⊢ f (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0) = if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else 0

Tactic:
rw [apply_ite f, hf]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem transGen_eq_self (trans : Transitive r) : TransGen r = r :=
  funext fun a ↦ funext fun b ↦ propext <|
    ⟨fun h ↦ by
      induction h with
      | single hc => exact hc
      | tail _ hcd hac => exact trans hac hcd, TransGen.single⟩

Proof state:
case single
α : Type u_1
r : α → α → Prop
trans : Transitive r
a b b✝ : α
hc : r a b✝
⊢ r a b✝

Tactic:
exact hc

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
trans : Transitive r
a b b✝ c✝ : α
a✝ : TransGen r a b✝
hcd : r b✝ c✝
hac : r a b✝
⊢ r a c✝

Tactic:
exact trans hac hcd

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
trans : Transitive r
a b : α
h : TransGen r a b
⊢ r a b

Tactic:
induction h with
| single hc => exact hc
| tail _ hcd hac => exact trans hac hcd

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed
    {S : Set (Set X)} [hS : Nonempty S] (hSd : DirectedOn (· ⊇ ·) S) (hSn : ∀ U ∈ S, U.Nonempty)
    (hSc : ∀ U ∈ S, IsCompact U) (hScl : ∀ U ∈ S, IsClosed U) : (⋂₀ S).Nonempty

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : Nonempty ↑S
hSd : DirectedOn (fun x1 x2 => x1 ⊇ x2) S
hSn : ∀ U ∈ S, U.Nonempty
hSc : ∀ U ∈ S, IsCompact U
hScl : ∀ U ∈ S, IsClosed U
⊢ (⋂ i, ↑i).Nonempty

Tactic:
exact IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _
  (DirectedOn.directed_val hSd) (fun i ↦ hSn i i.2) (fun i ↦ hSc i i.2) (fun i ↦ hScl i i.2)

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : Nonempty ↑S
hSd : DirectedOn (fun x1 x2 => x1 ⊇ x2) S
hSn : ∀ U ∈ S, U.Nonempty
hSc : ∀ U ∈ S, IsCompact U
hScl : ∀ U ∈ S, IsClosed U
⊢ (⋂₀ S).Nonempty

Tactic:
rw [sInter_eq_iInter]

Result:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : Nonempty ↑S
hSd : DirectedOn (fun x1 x2 => x1 ⊇ x2) S
hSn : ∀ U ∈ S, U.Nonempty
hSc : ∀ U ∈ S, IsCompact U
hScl : ∀ U ∈ S, IsClosed U
⊢ (⋂ i, ↑i).Nonempty