harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem sigma_eq_sigmaTR : @List.sigma = @sigmaTR

Proof state:
case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ l₁.sigma l₂ = l₁.sigmaTR l₂

Tactic:
simp [List.sigma, sigmaTR]

Result:
case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ flatMap (fun a => map (Sigma.mk a) (l₂ a)) l₁ =
    (foldl (fun acc a => foldl (fun acc b => acc.push ⟨a, b⟩) acc (l₂ a)) #[] l₁).toList

Proof state:
case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ flatMap (fun a => map (Sigma.mk a) (l₂ a)) l₁ =
    (foldl (fun acc a => foldl (fun acc b => acc.push ⟨a, b⟩) acc (l₂ a)) #[] l₁).toList

Tactic:
rw [Array.foldl_toList_eq_flatMap]

Result:
case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ flatMap (fun a => map (Sigma.mk a) (l₂ a)) l₁ = #[].toList ++ flatMap ?h.h.h.h.G l₁

case h.h.h.h.G
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ α → List ((a : α) × β a)

case h.h.h.h.H
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ ∀ (acc : Array ((a : α) × β a)) (a : α),
    (foldl (fun acc b => acc.push ⟨a, b⟩) acc (l₂ a)).toList = acc.toList ++ ?h.h.h.h.G a

Proof state:
⊢ @List.sigma = @sigmaTR

Tactic:
funext α β l₁ l₂

Result:
case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ l₁.sigma l₂ = l₁.sigmaTR l₂

Proof state:
case h.h.h.h.H
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
acc✝ : Array ((a : α) × β a)
a✝ : α
⊢ (foldl (fun acc b => acc.push ⟨a✝, b⟩) acc✝ (l₂ a✝)).toList = acc✝.toList ++ map (Sigma.mk a✝) (l₂ a✝)

Tactic:
apply Array.foldl_toList_eq_map

Result:
no goals

Proof state:
case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ flatMap (fun a => map (Sigma.mk a) (l₂ a)) l₁ = #[].toList ++ flatMap ?h.h.h.h.G l₁

case h.h.h.h.G
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ α → List ((a : α) × β a)

case h.h.h.h.H
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ ∀ (acc : Array ((a : α) × β a)) (a : α),
    (foldl (fun acc b => acc.push ⟨a, b⟩) acc (l₂ a)).toList = acc.toList ++ ?h.h.h.h.G a

Tactic:
rfl

Result:
case h.h.h.h.H
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ ∀ (acc : Array ((a : α) × β a)) (a : α),
    (foldl (fun acc b => acc.push ⟨a, b⟩) acc (l₂ a)).toList = acc.toList ++ map (Sigma.mk a) (l₂ a)

Proof state:
case h.h.h.h.H
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ ∀ (acc : Array ((a : α) × β a)) (a : α),
    (foldl (fun acc b => acc.push ⟨a, b⟩) acc (l₂ a)).toList = acc.toList ++ map (Sigma.mk a) (l₂ a)

Tactic:
intros

Result:
case h.h.h.h.H
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
acc✝ : Array ((a : α) × β a)
a✝ : α
⊢ (foldl (fun acc b => acc.push ⟨a✝, b⟩) acc✝ (l₂ a✝)).toList = acc✝.toList ++ map (Sigma.mk a✝) (l₂ a✝)
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem Reachable.dist_anti {G' : SimpleGraph V} (h : G ≤ G') (hr : G.Reachable u v) :
    G'.dist u v ≤ G.dist u v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
⊢ G'.dist u v ≤ G.dist u v

Tactic:
obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_dist

Result:
case intro
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ G.dist u v

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ (Walk.map (Hom.mapSpanningSubgraphs h) w✝).length

Tactic:
apply dist_le

Result:
no goals

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ G.dist u v

Tactic:
rw [← hw, ← Walk.length_map (Hom.mapSpanningSubgraphs h)]

Result:
case intro
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ (Walk.map (Hom.mapSpanningSubgraphs h) w✝).length
-- Mathlib/Data/Int/GCD.lean
theorem lcm_comm (i j : ℤ) : lcm i j = lcm j i

Proof state:
i j : ℤ
⊢ i.lcm j = j.lcm i

Tactic:
rw [Int.lcm, Int.lcm]

Result:
i j : ℤ
⊢ i.natAbs.lcm j.natAbs = j.natAbs.lcm i.natAbs

Proof state:
i j : ℤ
⊢ i.natAbs.lcm j.natAbs = j.natAbs.lcm i.natAbs

Tactic:
exact Nat.lcm_comm _ _

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem not_isUnit_X : ¬IsUnit (X : R[X]) := fun ⟨⟨_, g, _hfg, hgf⟩, rfl⟩ =>
  zero_ne_one' R <| by
    rw [← coeff_one_zero, ← hgf]
    simp

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : IsUnit X
g : R[X]
_hfg : (monomial 1) 1 * g = 1
hgf : g * (monomial 1) 1 = 1
⊢ 0 = (g * (monomial 1) 1).coeff 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : IsUnit X
g : R[X]
_hfg : (monomial 1) 1 * g = 1
hgf : g * (monomial 1) 1 = 1
⊢ 0 = 1

Tactic:
rw [← coeff_one_zero, ← hgf]

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : IsUnit X
g : R[X]
_hfg : (monomial 1) 1 * g = 1
hgf : g * (monomial 1) 1 = 1
⊢ 0 = (g * (monomial 1) 1).coeff 0
-- Mathlib/Topology/Order/LeftRightLim.lean
theorem leftLim_eq_of_eq_bot [hα : TopologicalSpace α] [h'α : OrderTopology α] (f : α → β) {a : α}
    (h : 𝓝[<] a = ⊥) : leftLim f a = f a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[<] a = ⊥
⊢ leftLim f a = f a

Tactic:
simp [leftLim, ite_eq_left_iff, h]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem univ_pi_eq_empty_iff : pi univ t = ∅ ↔ ∃ i, t i = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
⊢ univ.pi t = ∅ ↔ ∃ i, t i = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty, univ_pi_nonempty_iff]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem bitwise_diff : (bitwise fun a b => a && not b) = ldiff

Proof state:
case h.h.ofNat.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y => x && !!y) m n) = ↑(m &&& n)

Tactic:
congr

Result:
case h.h.ofNat.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => x && !!y) = and

Proof state:
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun y x => !x && !!y) = fun a b => a && !b

Tactic:
funext x y

Result:
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!y && !!x) = (x && !y)

Proof state:
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y => !x && !!y) m n) = ↑(Nat.bitwise (fun a b => a && !b) n m)

Tactic:
rw [Nat.bitwise_swap, Function.swap]

Result:
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x => !x && !!y) n m) = ↑(Nat.bitwise (fun a b => a && !b) n m)

Proof state:
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise (fun a b => a && !b) (ofNat m) (ofNat n) = (ofNat m).ldiff (ofNat n)

Tactic:
rfl

Result:
no goals

Proof state:
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y => !(!x && !y)) m n = m ||| n

Tactic:
congr

Result:
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or

Proof state:
⊢ (bitwise fun a b => a && !b) = ldiff

Tactic:
funext m n

Result:
case h.h
m n : ℤ
⊢ bitwise (fun a b => a && !b) m n = m.ldiff n

Proof state:
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x && !y)) = or

Tactic:
funext x y

Result:
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)

Proof state:
case h.h
m n : ℤ
⊢ bitwise (fun a b => a && !b) m n = m.ldiff n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}
  <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true,
    cond_false, cond_true, lor, Nat.ldiff, Bool.and_true, negSucc.injEq,
    Bool.and_false, Nat.land, Bool.not_true, ldiff, Nat.lor]

Result:
case h.h.ofNat.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y => x && !!y) m n) = ↑(m &&& n)

case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y => !(!x && !y)) m n = m ||| n

case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y => !x && !!y) m n) = ↑(Nat.bitwise (fun a b => a && !b) n m)

Proof state:
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x && !y)) = (x || y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals

Proof state:
case h.h.ofNat.negSucc.e_a.e_f
m n : ℕ
⊢ (fun x y => x && !!y) = and

Tactic:
funext x y

Result:
case h.h.ofNat.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (x && !!y) = (x && y)

Proof state:
case h.h.negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun y x => !x && !!y) n m) = ↑(Nat.bitwise (fun a b => a && !b) n m)

Tactic:
congr

Result:
case h.h.negSucc.negSucc.e_a.e_f
m n : ℕ
⊢ (fun y x => !x && !!y) = fun a b => a && !b

Proof state:
case h.h.negSucc.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!y && !!x) = (x && !y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals

Proof state:
case h.h.ofNat.negSucc.e_a.e_f.h.h
m n : ℕ
x y : Bool
⊢ (x && !!y) = (x && y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma cyclesOpIso_inv_op_iCycles [S.HasRightHomology] :
    S.cyclesOpIso.inv ≫ S.op.iCycles = S.pOpcycles.op

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.rightHomologyData.op.i = S.pOpcycles.op

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.rightHomologyData.op.cyclesIso.inv ≫ S.op.iCycles = S.pOpcycles.op

Tactic:
rw [← S.rightHomologyData.op.cyclesIso_hom_comp_i, Iso.inv_hom_id_assoc]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.rightHomologyData.op.i = S.pOpcycles.op

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.cyclesOpIso.inv ≫ S.op.iCycles = S.pOpcycles.op

Tactic:
dsimp [cyclesOpIso]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.rightHomologyData.op.cyclesIso.inv ≫ S.op.iCycles = S.pOpcycles.op
-- Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean
lemma whiskerLeftIso_mapId (f : a ⟶ b) : whiskerLeftIso (F.map f) (F.mapId b) =
    (F.mapComp f (𝟙 b)).symm ≪≫ F.map₂Iso (ρ_ f) ≪≫ (ρ_ (F.map f)).symm

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : Pseudofunctor B C
a b : B
f : a ⟶ b
⊢ whiskerLeftIso (F.map f) (F.mapId b) = (F.mapComp f (𝟙 b)).symm ≪≫ F.map₂Iso (ρ_ f) ≪≫ (ρ_ (F.map f)).symm

Tactic:
simp [mapComp_id_right]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem CNF_of_lt {b o : Ordinal} (ho : o ≠ 0) (hb : o < b) : CNF b o = [(0, o)]

Proof state:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ CNF b o = [(0, o)]

Tactic:
rw [CNF_ne_zero ho, log_eq_zero hb, opow_zero, div_one, mod_one, CNF_zero]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma sub_lt_of_lt_add {a b c : EReal} (h : a < b + c) : a - c < b :=
  add_lt_of_lt_sub <| by rwa [sub_eq_add_neg, neg_neg]

Proof state:
a b c : EReal
h : a < b + c
⊢ a < b - -c

Tactic:
rwa [sub_eq_add_neg, neg_neg]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma basicOpen_add_le :
    X.basicOpen (f + g) ≤ X.basicOpen f ⊔ X.basicOpen g

Proof state:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑(X.basicOpen (f + g))
hxU : x ∈ U
⊢ x ∈ ↑(X.basicOpen f ⊔ X.basicOpen g)

Tactic:
simp only [SetLike.mem_coe, Scheme.mem_basicOpen _ _ _ hxU, map_add, Opens.coe_sup,
  Set.mem_union] at hx ⊢

Result:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f + (ConcreteCategory.hom (X.presheaf.germ U x hxU)) g)
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f) ∨
    IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) g)

Proof state:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑(X.basicOpen (f + g))
⊢ x ∈ ↑(X.basicOpen f ⊔ X.basicOpen g)

Tactic:
have hxU : x ∈ U := X.basicOpen_le _ hx

Result:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑(X.basicOpen (f + g))
hxU : x ∈ U
⊢ x ∈ ↑(X.basicOpen f ⊔ X.basicOpen g)

Proof state:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f + (ConcreteCategory.hom (X.presheaf.germ U x hxU)) g)
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f) ∨
    IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) g)

Tactic:
exact IsLocalRing.isUnit_or_isUnit_of_isUnit_add hx

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
⊢ X.basicOpen (f + g) ≤ X.basicOpen f ⊔ X.basicOpen g

Tactic:
intro x hx

Result:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑(X.basicOpen (f + g))
⊢ x ∈ ↑(X.basicOpen f ⊔ X.basicOpen g)
-- Mathlib/Data/Finset/Sups.lean
theorem forall_disjSups_iff {p : α → Prop} :
    (∀ c ∈ s ○ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)) → ∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c

Tactic:
rintro h _ ⟨a, ha, b, hb, hab, rfl⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
h : ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
⊢ p (a ⊔ b)

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
h : ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
⊢ p (a ⊔ b)

Tactic:
exact h _ ha _ hb hab

Result:
no goals

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ c ∈ s ○ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

Tactic:
simp_rw [mem_disjSups]

Result:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)

Tactic:
refine ⟨fun h a ha b hb hab => h _ ⟨_, ha, _, hb, hab, rfl⟩, ?_⟩

Result:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
⊢ (∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)) → ∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_eq_right {a b : Cardinal} (hb : ℵ₀ ≤ b) (ha : a ≤ b) (ha' : a ≠ 0) : a * b = b

Proof state:
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
ha' : a ≠ 0
⊢ a * b = b

Tactic:
rw [mul_comm, mul_eq_left hb ha ha']

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem map_monic_eq_zero_iff (hp : p.Monic) : p.map f = 0 ↔ ∀ x, f x = 0 :=
  ⟨fun hfp x =>
    calc
      f x = f x * f p.leadingCoeff

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
hfp : map f p = 0
x : R
⊢ f x = f x * f p.leadingCoeff

Tactic:
simp only [mul_one, hp.leadingCoeff, f.map_one]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
h : ∀ (x : R), f x = 0
n : ℕ
⊢ (map f p).coeff n = coeff 0 n

Tactic:
simp only [h, coeff_map, coeff_zero]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : p.Monic
hfp : map f p = 0
x : R
⊢ f x * (map f p).coeff p.natDegree = 0

Tactic:
simp only [hfp, mul_zero, coeff_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_mod_mul_right (z x y : Nat) : (x * z) % (y * z) = (x % y) * z

Proof state:
z x y : Nat
⊢ z * x % (z * y) = z * (x % y)

Tactic:
apply mul_mod_mul_left

Result:
no goals

Proof state:
z x y : Nat
⊢ x * z % (y * z) = x % y * z

Tactic:
rw [Nat.mul_comm x z, Nat.mul_comm y z, Nat.mul_comm (x % y) z]

Result:
z x y : Nat
⊢ z * x % (z * y) = z * (x % y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_eq_none {a : Vector α n} (h : n ≤ i) : a[i]? = none

Proof state:
α : Type u_1
n i : Nat
a : Vector α n
h : n ≤ i
⊢ a[i]? = none

Tactic:
simp [getElem?_eq_none_iff, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attachWith_reverse {P : α → Prop} {xs : Array α}
    {H : ∀ (a : α), a ∈ xs.reverse → P a} :
    xs.reverse.attachWith P H =
      (xs.attachWith P (fun a h => H a (by simpa using h))).reverse

Proof state:
case mk
α : Type u_1
P : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ }.reverse → P a
⊢ { toList := toList✝ }.reverse.attachWith P H = ({ toList := toList✝ }.attachWith P ⋯).reverse

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
xs : Array α
H : ∀ (a : α), a ∈ xs.reverse → P a
⊢ xs.reverse.attachWith P H = (xs.attachWith P ⋯).reverse

Tactic:
cases xs

Result:
case mk
α : Type u_1
P : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ }.reverse → P a
⊢ { toList := toList✝ }.reverse.attachWith P H = ({ toList := toList✝ }.attachWith P ⋯).reverse

Proof state:
α : Type ?u.129026
P : α → Prop
xs : Array α
H : ∀ (a : α), a ∈ xs.reverse → P a
a : α
h : a ∈ xs
⊢ a ∈ xs.reverse

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_empty {s : Set Ω} : uniformOn s ∅ = 0

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s : Set Ω
⊢ (uniformOn s) ∅ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem ι_fstSigmaMap (b) : Sigma.ι I.left b ≫ I.fstSigmaMap = I.fst b ≫ Sigma.ι I.right _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.L
⊢ Sigma.ι I.left b ≫ I.fstSigmaMap = I.fst b ≫ Sigma.ι I.right (J.fst b)

Tactic:
simp [fstSigmaMap]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_zero (n : σ) : degreeOf n (0 : MvPolynomial σ R) = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
⊢ degreeOf n 0 = 0

Tactic:
simp only [degreeOf_def, degrees_zero, Multiset.count_zero]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
⊢ degreeOf n 0 = 0

Tactic:
classical simp only [degreeOf_def, degrees_zero, Multiset.count_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc (attr := simp)]
lemma mapCyclesIso_hom_iCycles [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :
    (S.mapCyclesIso F).hom ≫ F.map S.iCycles = (S.map F).iCycles

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.mapCyclesIso F).hom ≫ F.map S.iCycles = (S.map F).iCycles

Tactic:
apply LeftHomologyData.cyclesIso_hom_comp_i

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem dist_div_cos_oangle_left_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : dist p₁ p₂ / Real.Angle.cos (∡ p₃ p₁ p₂) = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
  dist_div_cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃