harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem opProductIsoCoproduct_inv_comp_lift [HasProduct Z] {X : C} (π : (a : α) → X ⟶ Z a) :
    (opProductIsoCoproduct Z).inv ≫ (Pi.lift π).op  = Sigma.desc (fun a ↦ (π a).op)

Proof state:
case h.e'_2.h.h.e'_7.h.h.e'_5.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x => op (Z x)) ⟶ op X) =
    ((Cofan.mk (∐ fun x => op (Z x)) (Sigma.ι fun x => op (Z x))).pt ⟶ op (Fan.mk X π).pt)
e_4✝¹ : op (∏ᶜ Z) = op (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
e_5✝ : op X = op (Fan.mk X π).pt
e_3✝ : X = (Fan.mk X π).pt
e_4✝ : ∏ᶜ Z = (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
⊢ Pi.lift π = (productIsProduct Z).lift (Fan.mk X π)

Tactic:
ext

Result:
case h.e'_2.h.h.e'_7.h.h.e'_5.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x => op (Z x)) ⟶ op X) =
    ((Cofan.mk (∐ fun x => op (Z x)) (Sigma.ι fun x => op (Z x))).pt ⟶ op (Fan.mk X π).pt)
e_4✝¹ : op (∏ᶜ Z) = op (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
e_5✝ : op X = op (Fan.mk X π).pt
e_3✝ : X = (Fan.mk X π).pt
e_4✝ : ∏ᶜ Z = (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
b✝ : α
⊢ Pi.lift π ≫ Pi.π Z b✝ = (productIsProduct Z).lift (Fan.mk X π) ≫ Pi.π Z b✝

Proof state:
case h.e'_2.h.h.e'_7.h.h.e'_5.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x => op (Z x)) ⟶ op X) =
    ((Cofan.mk (∐ fun x => op (Z x)) (Sigma.ι fun x => op (Z x))).pt ⟶ op (Fan.mk X π).pt)
e_4✝¹ : op (∏ᶜ Z) = op (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
e_5✝ : op X = op (Fan.mk X π).pt
e_3✝ : X = (Fan.mk X π).pt
e_4✝ : ∏ᶜ Z = (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
b✝ : α
⊢ Pi.lift π ≫ Pi.π Z b✝ = (productIsProduct Z).lift (Fan.mk X π) ≫ Pi.π Z b✝

Tactic:
simp [Pi.lift, productIsProduct]

Result:
no goals

Proof state:
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x => op (Z x)) ⟶ op X) =
    ((Cofan.mk (∐ fun x => op (Z x)) (Sigma.ι fun x => op (Z x))).pt ⟶ op (Fan.mk X π).pt)
⊢ (Sigma.desc fun a => (π a).op) = (coproductIsCoproduct fun x => op (Z x)).desc (Fan.mk X π).op

Tactic:
ext

Result:
case h.e'_3.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x => op (Z x)) ⟶ op X) =
    ((Cofan.mk (∐ fun x => op (Z x)) (Sigma.ι fun x => op (Z x))).pt ⟶ op (Fan.mk X π).pt)
b✝ : α
⊢ (Sigma.ι (fun a => op (Z a)) b✝ ≫ Sigma.desc fun a => (π a).op) =
    Sigma.ι (fun a => op (Z a)) b✝ ≫ (coproductIsCoproduct fun x => op (Z x)).desc (Fan.mk X π).op

Proof state:
case h.e'_3.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x => op (Z x)) ⟶ op X) =
    ((Cofan.mk (∐ fun x => op (Z x)) (Sigma.ι fun x => op (Z x))).pt ⟶ op (Fan.mk X π).pt)
b✝ : α
⊢ (Sigma.ι (fun a => op (Z a)) b✝ ≫ Sigma.desc fun a => (π a).op) =
    Sigma.ι (fun a => op (Z a)) b✝ ≫ (coproductIsCoproduct fun x => op (Z x)).desc (Fan.mk X π).op

Tactic:
simp [Sigma.desc, coproductIsCoproduct]

Result:
no goals
-- Mathlib/MeasureTheory/Order/UpperLower.lean
theorem Set.OrdConnected.null_frontier (hs : s.OrdConnected) : volume (frontier s) = 0

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : s.OrdConnected
⊢ volume (frontier (↑(upperClosure s) ∩ ↑(lowerClosure s))) = 0

Tactic:
exact measure_mono_null (frontier_inter_subset _ _) <| measure_union_null
  (measure_inter_null_of_null_left _ (UpperSet.upper _).null_frontier)
  (measure_inter_null_of_null_right _ (LowerSet.lower _).null_frontier)

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : s.OrdConnected
⊢ volume (frontier s) = 0

Tactic:
rw [← hs.upperClosure_inter_lowerClosure]

Result:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : s.OrdConnected
⊢ volume (frontier (↑(upperClosure s) ∩ ↑(lowerClosure s))) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem map_findSome? (f : α → Option β) (g : β → γ) (l : Array α) :
    (l.findSome? f).map g = l.findSome? (Option.map g ∘ f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
l : Array α
⊢ Option.map g (findSome? f l) = findSome? (Option.map g ∘ f) l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
toList✝ : List α
⊢ Option.map g (findSome? f { toList := toList✝ }) = findSome? (Option.map g ∘ f) { toList := toList✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
toList✝ : List α
⊢ Option.map g (findSome? f { toList := toList✝ }) = findSome? (Option.map g ∘ f) { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_succ_succ {i j : Nat} : dist (succ i) (succ j) = dist i j

Proof state:
i j : ℕ
⊢ i.succ.dist j.succ = i.dist j

Tactic:
simp [dist, succ_sub_succ]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma mul_mul_div (a : α) (h : IsUnit b) : a * b * (1 / b) = a

Proof state:
α : Type u
inst✝ : DivisionMonoid α
b a : α
h : IsUnit b
⊢ a * b * (1 / b) = a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem ratio_id : ratio (Dilation.id α) = 1

Proof state:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ edist ((Dilation.id α) x) ((Dilation.id α) y) = ↑1 * edist x y

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (Dilation.id α) = 1

Tactic:
rcases h with ⟨x, y, hne⟩

Result:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (Dilation.id α) = 1

Proof state:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Dilation.id α) = 1

Tactic:
push_neg at h

Result:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (Dilation.id α) = 1

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ ratio (Dilation.id α) = 1

Tactic:
by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞

Result:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Dilation.id α) = 1

case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Dilation.id α) = 1

Proof state:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (Dilation.id α) = 1

Tactic:
refine (ratio_unique hne.1 hne.2 ?_).symm

Result:
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ edist ((Dilation.id α) x) ((Dilation.id α) y) = ↑1 * edist x y

Proof state:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Dilation.id α) = 1

Tactic:
rw [ratio, if_pos h]

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

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 ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          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.fst (𝒰.map i ≫ 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.fst (𝒰.map i ≫ f) g

Tactic:
simp only [t'_fst_fst_fst, t'_fst_snd, t'_snd_snd]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_eq_univ_iff {f : ι → Set α} : ⋃ i, f i = univ ↔ ∀ x, ∃ i, x ∈ f i

Proof state:
α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ ⋃ i, f i = univ ↔ ∀ (x : α), ∃ i, x ∈ f i

Tactic:
simp only [eq_univ_iff_forall, mem_iUnion]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem singleton_div_closedBall_one : {x} / closedBall 1 δ = closedBall x δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} / closedBall 1 δ = closedBall x δ

Tactic:
rw [singleton_div_closedBall, div_one]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.of_pow {r : A} {n : ℕ} (hn : 0 < n) (ht : IsAlgebraic R (r ^ n)) :
    IsAlgebraic R r :=
  have ⟨p, p_nonzero, hp⟩ := ht
  ⟨_, by rwa [expand_ne_zero hn], by rwa [expand_aeval n p r]⟩

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
n : ℕ
hn : 0 < n
ht : IsAlgebraic R (r ^ n)
p : R[X]
p_nonzero : p ≠ 0
hp : (aeval (r ^ n)) p = 0
⊢ ?m.165740 p p_nonzero hp ≠ 0

Tactic:
rwa [expand_ne_zero hn]

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
n : ℕ
hn : 0 < n
ht : IsAlgebraic R (r ^ n)
p : R[X]
p_nonzero : p ≠ 0
hp : (aeval (r ^ n)) p = 0
⊢ (aeval r) ((expand R n) p) = 0

Tactic:
rwa [expand_aeval n p r]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem map_mk {f : α → β} (h : UniformContinuous f) (a : α) : map f (mk a) = mk (f a)

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ map f (mk a) = mk (f a)

Tactic:
rw [map, lift'_mk (uniformContinuous_mk.comp h)]

Result:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ (mk ∘ f) a = mk (f a)

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ (mk ∘ f) a = mk (f a)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Field/Periodic.lean
theorem Antiperiodic.mul_const' [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
    (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a)) (c / a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : DivisionSemiring α
inst✝ : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic (fun x => f (x * a)) (c / a)

Tactic:
simpa only [div_eq_mul_inv] using h.mul_const ha

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem one_lt_rootMultiplicity_iff_isRoot_iterate_derivative
    {p : R[X]} {t : R} (h : p ≠ 0) :
    1 < p.rootMultiplicity t ↔ ∀ m ≤ 1, (derivative^[m] p).IsRoot t :=
  lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors h
    (by rw [Nat.factorial_one, Nat.cast_one]; exact Submonoid.one_mem _)

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ ↑(Nat.factorial 1) ∈ nonZeroDivisors R

Tactic:
rw [Nat.factorial_one, Nat.cast_one]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ 1 ∈ nonZeroDivisors R

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ 1 ∈ nonZeroDivisors R

Tactic:
exact Submonoid.one_mem _

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_mul_inv : (mulSupport fun x => f x * (g x)⁻¹) ⊆ mulSupport f ∪ mulSupport g :=
  mulSupport_binop_subset (fun a b => a * b⁻¹) (by simp) f g

Proof state:
α : Type u_1
G : Type u_9
inst✝ : DivisionMonoid G
f g : α → G
⊢ (fun a b => a * b⁻¹) 1 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_add_of_le_one (ho : o ≤ 1) : Principal (· + ·) o

Proof state:
case inl
ho : 0 ≤ 1
⊢ Principal (fun x1 x2 => x1 + x2) 0

Tactic:
exact principal_zero

Result:
no goals

Proof state:
o : Ordinal.{u}
ho : o ≤ 1
⊢ Principal (fun x1 x2 => x1 + x2) o

Tactic:
rcases le_one_iff.1 ho with (rfl | rfl)

Result:
case inl
ho : 0 ≤ 1
⊢ Principal (fun x1 x2 => x1 + x2) 0

case inr
ho : 1 ≤ 1
⊢ Principal (fun x1 x2 => x1 + x2) 1

Proof state:
case inr
ho : 1 ≤ 1
⊢ Principal (fun x1 x2 => x1 + x2) 1

Tactic:
exact principal_add_one

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_int_mul_two_pi_add_pi (n : ℤ) : cos (n * (2 * π) + π) = -1

Proof state:
n : ℤ
⊢ cos (↑n * (2 * π) + π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).add_antiperiod_eq cos_antiperiodic

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem map_top (f : α → β) : map f ⊤ = restrict (range f) ⊤ :=
  ext fun s => by
    rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
      Set.image_eq_empty]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ((map f) ⊤) s = ((restrict (range f)) ⊤) s

Tactic:
rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
  Set.image_eq_empty]

Result:
no goals
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem exists_eq_const [PreconnectedSpace X] [Nonempty Y] (f : LocallyConstant X Y) :
    ∃ y, f = const X y

Proof state:
case inl.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
x : X
⊢ ∃ y, f = const X y

Tactic:
exact ⟨f x, f.eq_const x⟩

Result:
no goals

Proof state:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
hX : ¬Nonempty X
⊢ ∃ y, f = const X y

Tactic:
exact ⟨Classical.arbitrary Y, ext fun x => (hX ⟨x⟩).elim⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
⊢ ∃ y, f = const X y

Tactic:
rcases Classical.em (Nonempty X) with (⟨⟨x⟩⟩ | hX)

Result:
case inl.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
x : X
⊢ ∃ y, f = const X y

case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
hX : ¬Nonempty X
⊢ ∃ y, f = const X y
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_right_comm {m : δ → γ → ε} {n : α → β → δ} {m' : α → γ → δ'} {n' : δ' → β → ε}
    (h_right_comm : ∀ a b c, m (n a b) c = n' (m' a c) b) :
    map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g

Tactic:
rw [map₂_swap n, map₂_swap n']

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ (fun a b => n b a) g f) h = map₂ (fun a b => n' b a) g (map₂ m' f h)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ (fun a b => n b a) g f) h = map₂ (fun a b => n' b a) g (map₂ m' f h)

Tactic:
exact map₂_assoc fun _ _ _ => h_right_comm _ _ _

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem ne_zero (h0 : P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0) : P.toPoly ≠ 0

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
h0 : P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0
⊢ P.toPoly ≠ 0

Tactic:
contrapose! h0

Result:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
h0 : P.toPoly = 0
⊢ P.a = 0 ∧ P.b = 0 ∧ P.c = 0 ∧ P.d = 0

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
h0 : P.toPoly = 0
⊢ a 0 = 0 ∧ b 0 = 0 ∧ c 0 = 0 ∧ d 0 = 0

Tactic:
exact ⟨rfl, rfl, rfl, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
h0 : P.toPoly = 0
⊢ P.a = 0 ∧ P.b = 0 ∧ P.c = 0 ∧ P.d = 0

Tactic:
rw [(toPoly_eq_zero_iff P).mp h0]

Result:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
h0 : P.toPoly = 0
⊢ a 0 = 0 ∧ b 0 = 0 ∧ c 0 = 0 ∧ d 0 = 0
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma expect_ite_eq (i : ι) (f : ι → M) :
    𝔼 j ∈ s, (if i = j then f j else 0) = if i ∈ s then f i /ℚ #s else 0

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j ∈ s, if i = j then f j else 0) = if i ∈ s then (↑(#s))⁻¹ • f i else 0

Tactic:
split_ifs <;> simp [expect, *]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem bind_promises {s : Computation α} {f : α → Computation β} {a b} (h1 : s ~> a)
    (h2 : f a ~> b) : bind s f ~> b := fun b' bB => by
  rcases exists_of_mem_bind bB with ⟨a', a's, ba'⟩
  rw [← h1 a's] at ba'; exact h2 ba'

Proof state:
case intro.intro
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a'
⊢ b = b'

Tactic:
rw [← h1 a's] at ba'

Result:
case intro.intro
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'

Proof state:
case intro.intro
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'

Tactic:
exact h2 ba'

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
⊢ b = b'

Tactic:
rcases exists_of_mem_bind bB with ⟨a', a's, ba'⟩

Result:
case intro.intro
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a'
⊢ b = b'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_sub_of_le {x y : BitVec n} (h : y ≤ x) :
    (x - y).toNat = x.toNat - y.toNat

Proof state:
case neg
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
h' : ¬x.toNat = y.toNat
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = x.toNat - y.toNat

Tactic:
have : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) := by omega

Result:
case neg
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
h' : ¬x.toNat = y.toNat
this : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat)
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = x.toNat - y.toNat

Proof state:
case neg
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
h' : ¬x.toNat = y.toNat
this : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat)
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = x.toNat - y.toNat

Tactic:
rw [this, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = x.toNat - y.toNat

Tactic:
by_cases h' : x.toNat = y.toNat

Result:
case pos
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
h' : x.toNat = y.toNat
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = x.toNat - y.toNat

case neg
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
h' : ¬x.toNat = y.toNat
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = x.toNat - y.toNat

Proof state:
case pos
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
h' : x.toNat = y.toNat
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = x.toNat - y.toNat

Tactic:
rw [h', Nat.sub_self, Nat.sub_add_cancel (by omega), Nat.mod_self]

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
h' : ¬x.toNat = y.toNat
this : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat)
⊢ x.toNat - y.toNat < 2 ^ n

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
h : y ≤ x
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = x.toNat - y.toNat

Tactic:
rw [BitVec.le_def] at h

Result:
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = x.toNat - y.toNat

Proof state:
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
h' : x.toNat = y.toNat
⊢ y.toNat ≤ 2 ^ n

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
h : y ≤ x
⊢ (x - y).toNat = x.toNat - y.toNat

Tactic:
simp only [toNat_sub]

Result:
n : Nat
x y : BitVec n
h : y ≤ x
⊢ (2 ^ n - y.toNat + x.toNat) % 2 ^ n = x.toNat - y.toNat

Proof state:
n : Nat
x y : BitVec n
h : y.toNat ≤ x.toNat
h' : ¬x.toNat = y.toNat
⊢ 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat)

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/LinearMap.lean
theorem rank_comp_le_left (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : rank (f.comp g) ≤ rank f

Proof state:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ Submodule.map f (range g) ≤ range f

Tactic:
exact LinearMap.map_le_range

Result:
no goals

Proof state:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ (f ∘ₗ g).rank ≤ f.rank

Tactic:
refine Submodule.rank_mono ?_

Result:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ range (f ∘ₗ g) ≤ range f

Proof state:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ range (f ∘ₗ g) ≤ range f

Tactic:
rw [LinearMap.range_comp]

Result:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ Submodule.map f (range g) ≤ range f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_eq_some_of_exists {xs : List α} {p : α → Bool} (h : ∃ x, x ∈ xs ∧ p x) :
    xs.findIdx? p = some (xs.findIdx p)

Proof state:
α : Type u_1
xs : List α
p : α → Bool
h : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx? p xs = some (findIdx p xs)

Tactic:
rw [findIdx?_eq_some_iff_findIdx_eq]

Result:
α : Type u_1
xs : List α
p : α → Bool
h : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs < xs.length ∧ findIdx p xs = findIdx p xs

Proof state:
α : Type u_1
xs : List α
p : α → Bool
h : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs < xs.length ∧ findIdx p xs = findIdx p xs

Tactic:
exact ⟨findIdx_lt_length_of_exists h, rfl⟩

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem adjoinRoot_eq_top : Algebra.adjoin R ({root f} : Set (AdjoinRoot f)) = ⊤

Proof state:
case ih
R : Type u
inst✝ : CommRing R
f p : R[X]
⊢ (mk f) p ∈ Algebra.adjoin R {root f}

Tactic:
exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
⊢ Algebra.adjoin R {root f} = ⊤

Tactic:
refine Algebra.eq_top_iff.2 fun x => ?_

Result:
R : Type u
inst✝ : CommRing R
f : R[X]
x : AdjoinRoot f
⊢ x ∈ Algebra.adjoin R {root f}

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
x : AdjoinRoot f
⊢ x ∈ Algebra.adjoin R {root f}

Tactic:
induction x using AdjoinRoot.induction_on with
  | ih p => exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem getRight_eq_getRight? (h₁ : x.isRight) (h₂ : x.getRight?.isSome) :
    x.getRight h₁ = x.getRight?.get h₂

Proof state:
α : Type u
β : Type v
x : α ⊕ β
h₁ : x.isRight = true
h₂ : x.getRight?.isSome = true
⊢ x.getRight h₁ = x.getRight?.get h₂

Tactic:
simp [← getRight?_eq_some_iff]

Result:
no goals