harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullback_diagonal_map_snd_fst_fst :
    (pullback.snd (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i
        (by simp [condition]) (by simp [condition]))) ≫
      fst _ _ ≫ i₁ ≫ fst _ _ =
      pullback.fst _ _

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.11291, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ (i₁ ≫ snd f i) ≫ i = (i₁ ≫ fst f i) ≫ f

Tactic:
simp [condition]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.11291, u_1} C
X Y Z : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ (i₂ ≫ snd f i) ≫ i = (i₂ ≫ fst f i) ≫ f

Tactic:
simp [condition]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯)

Tactic:
conv_rhs => rw [← Category.comp_id (pullback.fst _ _)]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X

Tactic:
rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem append_consecutive {n m l : ℕ} (hnm : n ≤ m) (hml : m ≤ l) :
    Ico n m ++ Ico m l = Ico n l

Proof state:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ Ico n m ++ Ico m l = Ico n l

Tactic:
dsimp only [Ico]

Result:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' n (m - n) ++ range' m (l - m) = range' n (l - n)

Proof state:
case h.e'_3.h.e'_2
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + (l - m)

Tactic:
omega

Result:
no goals

Proof state:
case h.e'_2.h.e'_6
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' m (l - m) = range' (n + 1 * (m - n)) (l - m)

Tactic:
rw [Nat.one_mul, Nat.add_sub_cancel' hnm]

Result:
no goals

Proof state:
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' n (m - n) ++ range' m (l - m) = range' n (l - n)

Tactic:
convert range'_append n (m-n) (l-m) 1 using 2

Result:
case h.e'_2.h.e'_6
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' m (l - m) = range' (n + 1 * (m - n)) (l - m)

case h.e'_3.h.e'_2
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + (l - m)
-- Mathlib/Order/Lattice.lean
theorem sup_eq_maxDefault [SemilatticeSup α] [DecidableRel ((· ≤ ·) : α → α → Prop)]
    [IsTotal α (· ≤ ·)] :
    (· ⊔ ·) = (maxDefault : α → α → α)

Proof state:
case h.h
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
⊢ x ⊔ y = if x ≤ y then y else x

Tactic:
split_ifs with h'

Result:
case pos
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
h' : x ≤ y
⊢ x ⊔ y = y

case neg
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
h' : ¬x ≤ y
⊢ x ⊔ y = x

Proof state:
case h.h
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
⊢ x ⊔ y = maxDefault x y

Tactic:
unfold maxDefault

Result:
case h.h
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
⊢ x ⊔ y = if x ≤ y then y else x

Proof state:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
⊢ (fun x1 x2 => x1 ⊔ x2) = maxDefault

Tactic:
ext x y

Result:
case h.h
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
⊢ x ⊔ y = maxDefault x y
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem continuous_totalSpaceMk (b : B) :
    Continuous[_, a.totalSpaceTopology] (TotalSpace.mk b)

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ Continuous (↑e.toPartialHomeomorph ∘ TotalSpace.mk b)

Tactic:
exact continuous_iff_le_induced.2 (a.totalSpaceMk_isInducing b).eq_induced.le

Result:
no goals

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ Continuous (TotalSpace.mk b)

Tactic:
rw [e.toPartialHomeomorph.continuous_iff_continuous_comp_left
    (a.totalSpaceMk_preimage_source b)]

Result:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ Continuous (↑e.toPartialHomeomorph ∘ TotalSpace.mk b)

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
⊢ Continuous (TotalSpace.mk b)

Tactic:
letI := a.totalSpaceTopology

Result:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ Continuous (TotalSpace.mk b)

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ Continuous (TotalSpace.mk b)

Tactic:
let e := a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b)

Result:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ Continuous (TotalSpace.mk b)
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem existsUnique_preimage_of_mem_integerSet {a : mixedSpace K} (ha : a ∈ integerSet K) :
    ∃! x : 𝓞 K, mixedEmbedding K x = a

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
ha : (mixedEmbedding K) ↑x ∈ integerSet K
left✝ : (mixedEmbedding K) ↑x ∈ fundamentalCone K
⊢ ∃! x_1, (mixedEmbedding K) ↑x_1 = (mixedEmbedding K) ↑x

Tactic:
refine Function.Injective.existsUnique_of_mem_range ?_ (Set.mem_range_self x)

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
ha : (mixedEmbedding K) ↑x ∈ integerSet K
left✝ : (mixedEmbedding K) ↑x ∈ fundamentalCone K
⊢ Function.Injective fun x => (mixedEmbedding K) ↑x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : mixedSpace K
ha : a ∈ integerSet K
⊢ ∃! x, (mixedEmbedding K) ↑x = a

Tactic:
obtain ⟨_, ⟨x, rfl⟩⟩ := mem_integerSet.mp ha

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
ha : (mixedEmbedding K) ↑x ∈ integerSet K
left✝ : (mixedEmbedding K) ↑x ∈ fundamentalCone K
⊢ ∃! x_1, (mixedEmbedding K) ↑x_1 = (mixedEmbedding K) ↑x

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
ha : (mixedEmbedding K) ↑x ∈ integerSet K
left✝ : (mixedEmbedding K) ↑x ∈ fundamentalCone K
⊢ Function.Injective fun x => (mixedEmbedding K) ↑x

Tactic:
exact (mixedEmbedding_injective K).comp RingOfIntegers.coe_injective

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
/-- Special case of the **Four Functions Theorem** when `s = t = univ`. -/
lemma four_functions_theorem_univ (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
    (h : ∀ a b, f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) :
    (∑ a, f₁ a) * ∑ a, f₂ a ≤ (∑ a, f₃ a) * ∑ a, f₄ a

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst✝ : Fintype α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
⊢ (∑ a : α, f₁ a) * ∑ a : α, f₂ a ≤ (∑ a : α, f₃ a) * ∑ a : α, f₄ a

Tactic:
simpa using four_functions_theorem f₁ f₂ f₃ f₄ h₁ h₂ h₃ h₄ h univ univ

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst✝ : Fintype α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
⊢ (∑ a : α, f₁ a) * ∑ a : α, f₂ a ≤ (∑ a : α, f₃ a) * ∑ a : α, f₄ a

Tactic:
classical simpa using four_functions_theorem f₁ f₂ f₃ f₄ h₁ h₂ h₃ h₄ h univ univ

Result:
no goals
-- Mathlib/Topology/Homotopy/Path.lean
theorem hcomp_apply (F : Homotopy p₀ q₀) (G : Homotopy p₁ q₁) (x : I × I) :
    F.hcomp G x =
      if h : (x.2 : ℝ) ≤ 1 / 2 then
        F.eval x.1 ⟨2 * x.2, (unitInterval.mul_pos_mem_iff zero_lt_two).2 ⟨x.2.2.1, h⟩⟩
      else
        G.eval x.1
          ⟨2 * x.2 - 1, unitInterval.two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, x.2.2.2⟩⟩ :=
  show ite _ _ _ = _ by split_ifs <;> exact Path.extend_extends _ _

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
⊢ (if ↑x.2 ≤ 1 / 2 then (F.eval x.1).extend (2 * ↑x.2) else (G.eval x.1).extend (2 * ↑x.2 - 1)) =
    if h : ↑x.2 ≤ 1 / 2 then (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩ else (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩

Tactic:
split_ifs <;> exact Path.extend_extends _ _

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem add_divInt (a b c : ℤ) : (a + b) /. c = a /. c + b /. c :=
  if h : c = 0 then by simp [h]
  else by
    rw [divInt_add_divInt _ _ h h, divInt_eq_iff h (Int.mul_ne_zero h h)]
    simp [Int.add_mul, Int.mul_assoc]

Proof state:
a b c : ℤ
h : c = 0
⊢ (a + b) /. c = a /. c + b /. c

Tactic:
simp [h]

Result:
no goals

Proof state:
a b c : ℤ
h : ¬c = 0
⊢ (a + b) /. c = a /. c + b /. c

Tactic:
rw [divInt_add_divInt _ _ h h, divInt_eq_iff h (Int.mul_ne_zero h h)]

Result:
a b c : ℤ
h : ¬c = 0
⊢ (a + b) * (c * c) = (a * c + b * c) * c

Proof state:
a b c : ℤ
h : ¬c = 0
⊢ (a + b) * (c * c) = (a * c + b * c) * c

Tactic:
simp [Int.add_mul, Int.mul_assoc]

Result:
no goals
-- Mathlib/Algebra/Category/AlgebraCat/Basic.lean
lemma comp_apply {A B C : AlgebraCat.{v} R} (f : A ⟶ B) (g : B ⟶ C) (a : A) :
    (f ≫ g) a = g (f a)

Proof state:
R : Type u
inst✝ : CommRing R
A B C : AlgebraCat R
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsb_not {x : BitVec w} :
    (~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i))

Proof state:
w i : Nat
x : BitVec w
⊢ (~~~x).getMsbD i = (decide (i < w) && !x.getMsbD i)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_of_Y_ne {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3) :
    W.add P Q = addU P Q • ![1, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3
⊢ W.add P Q = addU P Q • ![1, 1, 0]

Tactic:
rw [add, if_neg <| not_equiv_of_Y_ne hy, addXYZ_of_X_eq hP hQ hPz hQz hx]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem append_nil : append xs nil = xs

Proof state:
case mk
α : Type u_1
n : ℕ
val✝ : List α
property✝ : val✝.length = n
⊢ append ⟨val✝, property✝⟩ nil = ⟨val✝, property✝⟩

Tactic:
simp [append]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
xs : Vector α n
⊢ xs.append nil = xs

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : ℕ
val✝ : List α
property✝ : val✝.length = n
⊢ append ⟨val✝, property✝⟩ nil = ⟨val✝, property✝⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
  | _ :: l₁, _ :: l₂, h => by
    cases h
    case head => simp
    case tail h =>
    · have := of_mem_zip h
      exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : Mem (a, b) (zipWith Prod.mk l₁ l₂)
this : a ∈ l₁ ∧ b ∈ l₂
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂

Tactic:
exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : Mem (a, b) (zipWith Prod.mk l₁ l₂)
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂

Tactic:
have := of_mem_zip h

Result:
α : Type u_1
β : Type u_2
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : Mem (a, b) (zipWith Prod.mk l₁ l₂)
this : a ∈ l₁ ∧ b ∈ l₂
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂

Proof state:
case head
α : Type u_1
β : Type u_2
a : α
b : β
l₁ : List α
l₂ : List β
⊢ a ∈ a :: l₁ ∧ b ∈ b :: l₂

case tail
α : Type u_1
β : Type u_2
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
a✝ : Mem (a, b) (zipWith Prod.mk l₁ l₂)
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂

Tactic:
case head => simp

Result:
case tail
α : Type u_1
β : Type u_2
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
a✝ : Mem (a, b) (zipWith Prod.mk l₁ l₂)
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
h : (a, b) ∈ (head✝¹ :: l₁).zip (head✝ :: l₂)
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂

Tactic:
cases h

Result:
case head
α : Type u_1
β : Type u_2
a : α
b : β
l₁ : List α
l₂ : List β
⊢ a ∈ a :: l₁ ∧ b ∈ b :: l₂

case tail
α : Type u_1
β : Type u_2
a : α
b : β
head✝¹ : α
l₁ : List α
head✝ : β
l₂ : List β
a✝ : Mem (a, b) (zipWith Prod.mk l₁ l₂)
⊢ a ∈ head✝¹ :: l₁ ∧ b ∈ head✝ :: l₂

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
l₁ : List α
l₂ : List β
⊢ a ∈ a :: l₁ ∧ b ∈ b :: l₂

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma ih1_swap (ih : ∀ a, ArgsRel a (Args.P1 x y) → P124 a) : IH1 y x := ih1 <| by
  simp_rw [ArgsRel, InvImage, Args.toMultiset, Multiset.pair_comm] at ih ⊢
  exact ih

Proof state:
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
⊢ ∀ (a : Args), ArgsRel a (Args.P1 y x) → P124 a

Tactic:
simp_rw [ArgsRel, InvImage, Args.toMultiset, Multiset.pair_comm] at ih ⊢

Result:
x y : PGame
ih :
  ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {y, x} →
      P124 a
⊢ ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {y, x} →
      P124 a

Proof state:
x y : PGame
ih :
  ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {y, x} →
      P124 a
⊢ ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {y, x} →
      P124 a

Tactic:
exact ih

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_le_mul_of_nonpos_left {a b c : Int}
    (ha : a ≤ 0) (h : c ≤ b) : a * b ≤ a * c

Proof state:
a b c : Int
ha : a ≤ 0
h : c ≤ b
⊢ a * b ≤ a * c

Tactic:
rw [Int.mul_comm a b, Int.mul_comm a c]

Result:
a b c : Int
ha : a ≤ 0
h : c ≤ b
⊢ b * a ≤ c * a

Proof state:
a b c : Int
ha : a ≤ 0
h : c ≤ b
⊢ b * a ≤ c * a

Tactic:
apply Int.mul_le_mul_of_nonpos_right h ha

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma evalEval_polynomialX (x y : R) :
    W'.polynomialX.evalEval x y = W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y (C (C W'.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W'.a₂) * X + C W'.a₄)) =
    W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄)

Tactic:
eval_simp

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y W'.polynomialX = W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄)

Tactic:
simp only [polynomialX]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y (C (C W'.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W'.a₂) * X + C W'.a₄)) =
    W'.a₁ * y - (3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄)
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem mem_col_iff {μ : YoungDiagram} {j : ℕ} {c : ℕ × ℕ} : c ∈ μ.col j ↔ c ∈ μ ∧ c.snd = j

Proof state:
μ : YoungDiagram
j : ℕ
c : ℕ × ℕ
⊢ c ∈ μ.col j ↔ c ∈ μ ∧ c.2 = j

Tactic:
simp [col]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem restrict_toMeasurable_of_cover {s : Set α} {v : ℕ → Set α} (hv : s ⊆ ⋃ n, v n)
    (h'v : ∀ n, μ (s ∩ v n) ≠ ∞) : μ.restrict (toMeasurable μ s) = μ.restrict s :=
  ext fun t ht => by
    simp only [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_cover ht hv h'v]

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
v : ℕ → Set α
hv : s ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (s ∩ v n) ≠ ⊤
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (toMeasurable μ s)) t = (μ.restrict s) t

Tactic:
simp only [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_cover ht hv h'v]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
    xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j]

Proof state:
case mk
α : Type u_1
p : α → Bool
b : α
xs : List α
⊢ find? p { toList := xs } = some b ↔
    p b = true ∧ ∃ i h, { toList := xs }[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p { toList := xs }[j]) = true

Tactic:
simp [List.find?_eq_some_iff_getElem]

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
b : α
⊢ find? p xs = some b ↔ p b = true ∧ ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p xs[j]) = true

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
b : α
xs : List α
⊢ find? p { toList := xs } = some b ↔
    p b = true ∧ ∃ i h, { toList := xs }[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p { toList := xs }[j]) = true
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
theorem hexagon_reverse (X Y Z : ModuleCat.{u} R) :
    (α_ X Y Z).inv ≫ (braiding _ Z).hom ≫ (α_ Z X Y).inv =
      X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    (Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv =
    (α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv) =
    Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      (Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y))
        ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Tactic:
intro x y z

Result:
case hf.H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    (Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Proof state:
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv =
    X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y

Tactic:
apply (cancel_epi (α_ X Y Z).hom).1

Result:
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv =
    (α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y

Proof state:
case hf
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv) =
    Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)

Tactic:
apply TensorProduct.ext_threefold

Result:
case hf.H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      (Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y))
        ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[simp]
lemma prodComparisonIso_hom : (prodComparisonIso F A B).hom = prodComparison F A B

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : PreservesLimit (pair A B) F
⊢ (prodComparisonIso F A B).hom = prodComparison F A B

Tactic:
rfl

Result:
no goals