harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Complex/Basic.lean
theorem mul_I_re (z : ℂ) : (z * I).re = -z.im

Proof state:
z : ℂ
⊢ (z * I).re = -z.im

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/OmegaLimit.lean
theorem eventually_mapsTo_of_isOpen_of_omegaLimit_subset [CompactSpace β] {v : Set β}
    (hv₁ : IsOpen v) (hv₂ : ω f ϕ s ⊆ v) : ∀ᶠ t in f, MapsTo (ϕ t) s v

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v

Tactic:
rcases eventually_closure_subset_of_isOpen_of_omegaLimit_subset f ϕ s hv₁ hv₂ with ⟨u, hu_mem, hu⟩

Result:
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v

Proof state:
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ v
t : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ v

Tactic:
exact hu (subset_closure <| mem_image2_of_mem ht hx)

Result:
no goals

Proof state:
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v

Tactic:
refine mem_of_superset hu_mem fun t ht x hx ↦ ?_

Result:
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ v
t : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ v
-- Mathlib/Data/Real/EReal.lean
lemma inv_inv {a : EReal} (h : a ≠ ⊥) (h' : a ≠ ⊤) : (a⁻¹)⁻¹ = a

Proof state:
a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ a⁻¹⁻¹ = a

Tactic:
rw [← coe_toReal h' h, ← coe_inv a.toReal, ← coe_inv a.toReal⁻¹, _root_.inv_inv a.toReal]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_succ (a b : Ordinal) : a ^ succ b = a ^ b * a

Proof state:
a b : Ordinal.{u_1}
⊢ a ^ succ b = a ^ b * a

Tactic:
obtain rfl | h := eq_or_ne a 0

Result:
case inl
b : Ordinal.{u_1}
⊢ 0 ^ succ b = 0 ^ b * 0

case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ succ b = a ^ b * a

Proof state:
case inl
b : Ordinal.{u_1}
⊢ 0 ^ succ b = 0 ^ b * 0

Tactic:
rw [zero_opow (succ_ne_zero b), mul_zero]

Result:
no goals

Proof state:
case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ succ b = a ^ b * a

Tactic:
rw [opow_of_ne_zero h, opow_of_ne_zero h, limitRecOn_succ]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_le_middle (r n : ℕ) : choose n r ≤ choose n (n / 2)

Proof state:
case inl.inl
r n : ℕ
b : r ≤ n
a : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
apply choose_le_middle_of_le_half_left a

Result:
no goals

Proof state:
case inr
r n : ℕ
b : r > n
⊢ 0 ≤ n.choose (n / 2)

Tactic:
apply zero_le

Result:
no goals

Proof state:
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n - r ≤ n / 2

Tactic:
rw [le_div_iff_mul_le Nat.zero_lt_two, Nat.mul_sub_right_distrib, Nat.sub_le_iff_le_add,
  ← Nat.sub_le_iff_le_add', Nat.mul_two, Nat.add_sub_cancel]

Result:
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n ≤ r * 2

Proof state:
case inr
r n : ℕ
b : r > n
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rw [choose_eq_zero_of_lt b]

Result:
case inr
r n : ℕ
b : r > n
⊢ 0 ≤ n.choose (n / 2)

Proof state:
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n - r ≤ n / 2

Tactic:
rw [div_lt_iff_lt_mul Nat.zero_lt_two] at h

Result:
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n - r ≤ n / 2

Proof state:
r n : ℕ
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rcases le_or_gt r n with b | b

Result:
case inl
r n : ℕ
b : r ≤ n
⊢ n.choose r ≤ n.choose (n / 2)

case inr
r n : ℕ
b : r > n
⊢ n.choose r ≤ n.choose (n / 2)

Proof state:
case inl
r n : ℕ
b : r ≤ n
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rcases le_or_lt r (n / 2) with a | h

Result:
case inl.inl
r n : ℕ
b : r ≤ n
a : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)

case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose r ≤ n.choose (n / 2)

Proof state:
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose (n - r) ≤ n.choose (n / 2)

Tactic:
apply choose_le_middle_of_le_half_left

Result:
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n - r ≤ n / 2

Proof state:
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n ≤ r * 2

Tactic:
exact le_of_lt h

Result:
no goals

Proof state:
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rw [← choose_symm b]

Result:
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose (n - r) ≤ n.choose (n / 2)
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_zero_right' (r : R) : multichoose r 0 = r ^ 0

Proof state:
R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ multichoose r 0 = r ^ 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero 0),
  factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_zero, smeval_one, Nat.factorial]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
theorem differentiableWithinAt_arcsin_Ici {x : ℝ} :
    DifferentiableWithinAt ℝ arcsin (Ici x) x ↔ x ≠ -1

Proof state:
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x ↔ x ≠ -1

Tactic:
refine ⟨?_, fun h => (hasDerivWithinAt_arcsin_Ici h).differentiableWithinAt⟩

Result:
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x → x ≠ -1

Proof state:
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x → x ≠ -1

Tactic:
rintro h rfl

Result:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ False

Proof state:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ False

Tactic:
have : sin ∘ arcsin =ᶠ[𝓝[≥] (-1 : ℝ)] id := by
  filter_upwards [Icc_mem_nhdsGE (neg_lt_self zero_lt_one)] with x using sin_arcsin'

Result:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
⊢ False

Proof state:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
⊢ id (-1) = sin (arcsin (-1))

Tactic:
simp

Result:
no goals

Proof state:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
⊢ False

Tactic:
have := h.hasDerivWithinAt.sin.congr_of_eventuallyEq this.symm (by simp)

Result:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this✝ : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
this : HasDerivWithinAt id (cos (arcsin (-1)) * derivWithin arcsin (Ici (-1)) (-1)) (Ici (-1)) (-1)
⊢ False

Proof state:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this✝ : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
this : HasDerivWithinAt id (cos (arcsin (-1)) * derivWithin arcsin (Ici (-1)) (-1)) (Ici (-1)) (-1)
⊢ False

Tactic:
simpa using (uniqueDiffOn_Ici _ _ left_mem_Ici).eq_deriv _ this (hasDerivWithinAt_id _ _)

Result:
no goals

Proof state:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id

Tactic:
filter_upwards [Icc_mem_nhdsGE (neg_lt_self zero_lt_one)] with x using sin_arcsin'

Result:
no goals
-- Mathlib/Order/Iterate.lean
theorem le_iterate_comp_of_le (hf : Monotone f) (H : h ∘ g ≤ f ∘ h) (n : ℕ) :
    h ∘ g^[n] ≤ f^[n] ∘ h := fun x => by
  apply hf.seq_le_seq n <;> intros <;>
    simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]
  case hx => exact H _

Proof state:
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[n]) x ≤ (f^[n] ∘ h) x

Tactic:
apply hf.seq_le_seq n <;> intros <;>
  simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]

Result:
case hx
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ h (g (g^[k✝] x)) ≤ f (h (g^[k✝] x))

Proof state:
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ h (g (g^[k✝] x)) ≤ f (h (g^[k✝] x))

Tactic:
exact H _

Result:
no goals

Proof state:
case hx
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
k✝ : ℕ
a✝ : k✝ < n
⊢ h (g (g^[k✝] x)) ≤ f (h (g^[k✝] x))

Tactic:
case hx => exact H _

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
lemma sup'_image₂_left (g : γ → δ) (h : (image₂ f s t).Nonempty) :
    sup' (image₂ f s t) h g =
      sup' s h.of_image₂_left fun x ↦ sup' t h.of_image₂_right (g <| f x ·)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (s.sup' ⋯ fun i => t.sup' ⋯ fun i' => (g ∘ uncurry f) (i, i')) = s.sup' ⋯ fun x => t.sup' ⋯ fun x_1 => g (f x x_1)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g = s.sup' ⋯ fun x => t.sup' ⋯ fun x_1 => g (f x x_1)

Tactic:
simp only [image₂, sup'_image, sup'_product_left]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (s.sup' ⋯ fun i => t.sup' ⋯ fun i' => (g ∘ uncurry f) (i, i')) = s.sup' ⋯ fun x => t.sup' ⋯ fun x_1 => g (f x x_1)
-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
@[simp]
lemma pushforwardContinuousSheafificationCompatibility_hom_app_val (F : Dᵒᵖ ⥤ A) :
    ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
    sheafifyLift J (whiskerLeft G.op <| toSheafify K F)
      ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F).cond

Proof state:
case a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
⊢ toSheafify J (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
      ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
    whiskerLeft G.op (toSheafify K F)

Tactic:
apply toSheafify_pullbackSheafificationCompatibility

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
⊢ ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
    sheafifyLift J (whiskerLeft G.op (toSheafify K F)) ⋯

Tactic:
apply sheafifyLift_unique

Result:
case a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
⊢ toSheafify J (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
      ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
    whiskerLeft G.op (toSheafify K F)
-- Mathlib/Data/Nat/Init.lean
lemma div_mul_div_comm : b ∣ a → d ∣ c → (a / b) * (c / d) = (a * c) / (b * d)

Proof state:
case intro.intro.inr.inr
b d x y : ℕ
hb : b > 0
hd : d > 0
⊢ b * x / b * (d * y / d) = b * x * (d * y) / (b * d)

Tactic:
rw [Nat.mul_div_cancel_left _ hb, Nat.mul_div_cancel_left _ hd, Nat.mul_assoc b,
  Nat.mul_left_comm x, ← Nat.mul_assoc b, Nat.mul_div_cancel_left _ (Nat.mul_pos hb hd)]

Result:
no goals

Proof state:
case intro.intro.inr.inl
b x y : ℕ
hb : b > 0
⊢ b * x / b * (0 * y / 0) = b * x * (0 * y) / (b * 0)

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
b d x y : ℕ
⊢ b * x / b * (d * y / d) = b * x * (d * y) / (b * d)

Tactic:
obtain rfl | hb := b.eq_zero_or_pos

Result:
case intro.intro.inl
d x y : ℕ
⊢ 0 * x / 0 * (d * y / d) = 0 * x * (d * y) / (0 * d)

case intro.intro.inr
b d x y : ℕ
hb : b > 0
⊢ b * x / b * (d * y / d) = b * x * (d * y) / (b * d)

Proof state:
case intro.intro.inr
b d x y : ℕ
hb : b > 0
⊢ b * x / b * (d * y / d) = b * x * (d * y) / (b * d)

Tactic:
obtain rfl | hd := d.eq_zero_or_pos

Result:
case intro.intro.inr.inl
b x y : ℕ
hb : b > 0
⊢ b * x / b * (0 * y / 0) = b * x * (0 * y) / (b * 0)

case intro.intro.inr.inr
b d x y : ℕ
hb : b > 0
hd : d > 0
⊢ b * x / b * (d * y / d) = b * x * (d * y) / (b * d)

Proof state:
a b c d : ℕ
⊢ b ∣ a → d ∣ c → a / b * (c / d) = a * c / (b * d)

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

Result:
case intro.intro
b d x y : ℕ
⊢ b * x / b * (d * y / d) = b * x * (d * y) / (b * d)

Proof state:
case intro.intro.inl
d x y : ℕ
⊢ 0 * x / 0 * (d * y / d) = 0 * x * (d * y) / (0 * d)

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem ne_of_oangle_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : x ≠ y :=
  o.ne_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 1
⊢ 1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/ShrinkingLemma.lean
theorem find_mem {c : Set (PartialRefinement u s p)} (i : ι) (ne : c.Nonempty) :
    find c ne i ∈ c

Proof state:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
⊢ find c ne i ∈ c

Tactic:
rw [find]

Result:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
⊢ (if hi : ∃ v ∈ c, i ∈ v.carrier then hi.choose else ne.some) ∈ c

Proof state:
case pos
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
h : ∃ v ∈ c, i ∈ v.carrier
⊢ h.choose ∈ c

case neg
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
h : ¬∃ v ∈ c, i ∈ v.carrier
⊢ ne.some ∈ c

Tactic:
exacts [h.choose_spec.1, ne.some_mem]

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
⊢ (if hi : ∃ v ∈ c, i ∈ v.carrier then hi.choose else ne.some) ∈ c

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
h : ∃ v ∈ c, i ∈ v.carrier
⊢ h.choose ∈ c

case neg
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
h : ¬∃ v ∈ c, i ∈ v.carrier
⊢ ne.some ∈ c
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma homMk₃_app_two : (homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app ⟨2, by valid⟩ = app₂ :=
  rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.214360, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 3
app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯
app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯
app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯
app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯
w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯
w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯
w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯
⊢ 2 < 3 + 1

Tactic:
valid

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem leftDistributor_inv {J : Type} [Fintype J] (X : C) (f : J → C) :
    (leftDistributor X f).inv = ∑ j : J, biproduct.π _ j ≫ (X ◁ biproduct.ι f j)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
⊢ (leftDistributor X f).inv = ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ X ◁ biproduct.ι f j

Tactic:
ext

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ X ◁ biproduct.ι f j

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ X ◁ biproduct.ι f j

Tactic:
dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (biproduct.ι (fun j => X ⊗ f j) j✝ ≫ biproduct.desc fun j => X ◁ biproduct.ι f j) =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ X ◁ biproduct.ι f j

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (biproduct.ι (fun j => X ⊗ f j) j✝ ≫ biproduct.desc fun j => X ◁ biproduct.ι f j) =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ X ◁ biproduct.ι f j

Tactic:
simp only [Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp, zero_comp,
  Finset.sum_dite_eq, Finset.mem_univ, ite_true, eqToHom_refl, Category.id_comp,
  biproduct.ι_desc]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
⊢ (leftDistributor X f).inv = ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ X ◁ biproduct.ι f j

Tactic:
classical
ext
dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]
simp only [Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp, zero_comp,
  Finset.sum_dite_eq, Finset.mem_univ, ite_true, eqToHom_refl, Category.id_comp,
  biproduct.ι_desc]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
lemma congr_map {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂)
    {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) :
    iter₁.F.map (homOfLE h : ⟨k₁, h.trans h₁⟩ ⟶ ⟨k₂, h₁⟩) =
      eqToHom (congr_obj iter₁ iter₂ k₁ (h.trans h₁) (h.trans h₂)) ≫
        iter₂.F.map (homOfLE h) ≫
        eqToHom (congr_obj iter₁ iter₂ k₂ h₁ h₂).symm

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
this :
  ∃ (hX : iter₁.F.obj ⟨k₁, ⋯⟩ = iter₂.F.obj ⟨k₁, ⋯⟩) (hY : iter₁.F.obj ⟨k₂, h₁⟩ = iter₂.F.obj ⟨k₂, h₂⟩),
    iter₁.F.map (homOfLE h) = eqToHom hX ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯
⊢ iter₁.F.map (homOfLE h) = eqToHom ⋯ ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯

Tactic:
tauto

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
⊢ iter₁.F.map (homOfLE h) = eqToHom ⋯ ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯

Tactic:
have := (Arrow.mk_eq_mk_iff _ _).1 (congr_arrowMap iter₁ iter₂ h h₁ h₂)

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
this :
  ∃ (hX : iter₁.F.obj ⟨k₁, ⋯⟩ = iter₂.F.obj ⟨k₁, ⋯⟩) (hY : iter₁.F.obj ⟨k₂, h₁⟩ = iter₂.F.obj ⟨k₂, h₂⟩),
    iter₁.F.map (homOfLE h) = eqToHom hX ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯
⊢ iter₁.F.map (homOfLE h) = eqToHom ⋯ ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_inj_iff : ∀ {x y : Bool}, (!x) = (!y) ↔ x = y

Proof state:
⊢ ∀ {x y : Bool}, (!x) = !y ↔ x = y

Tactic:
decide

Result:
no goals