harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean
@[simp] lemma pointwise_vadd_top (v : V) : v +ᵥ (⊤ : AffineSubspace k P) = ⊤

Proof state:
case h
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊤ ↔ x✝ ∈ ⊤

Tactic:
simp [pointwise_vadd_eq_map, map_top, vadd_eq_iff_eq_neg_vadd]

Result:
no goals

Proof state:
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
⊢ v +ᵥ ⊤ = ⊤

Tactic:
ext

Result:
case h
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊤ ↔ x✝ ∈ ⊤
-- Mathlib/Analysis/LocallyConvex/WeakSpace.lean
theorem Convex.toWeakSpace_closure {s : Set E} (hs : Convex ℝ s) :
    (toWeakSpace 𝕜 E) '' (closure s) = closure (toWeakSpace 𝕜 E '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : E →L[𝕜] 𝕜
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : WeakSpace 𝕜 E →L[𝕜] 𝕜 := { toLinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm, cont := ⋯ }
⊢ u < (RCLike.reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f')) ((toWeakSpace 𝕜 E) x)

Tactic:
simpa [f']

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_le_of_le_log {b x c : Ordinal} (hc : c ≠ 0) (h : c ≤ log b x) : b ^ c ≤ x

Proof state:
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
⊢ b ^ c ≤ x

Tactic:
obtain hb | hb := le_or_lt b 1

Result:
case inl
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : b ≤ 1
⊢ b ^ c ≤ x

case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ b ^ c ≤ x

Proof state:
case inl
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ 0
hb : b ≤ 1
⊢ b ^ c ≤ x

Tactic:
exact (h.not_lt (Ordinal.pos_iff_ne_zero.2 hc)).elim

Result:
no goals

Proof state:
case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ b ^ c ≤ x

Tactic:
rwa [opow_le_iff_le_log' hb hc]

Result:
no goals

Proof state:
case inl
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : b ≤ 1
⊢ b ^ c ≤ x

Tactic:
rw [log_of_left_le_one hb] at h

Result:
case inl
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ 0
hb : b ≤ 1
⊢ b ^ c ≤ x
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem single_mul_apply_aux [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G}
    (H : ∀ a ∈ f.support, x * a = y ↔ a = z) : (single x r * f) y = r * f z

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x y z : G
H : ∀ a ∈ f.support, x * a = y ↔ a = z
⊢ (single x r * f) y = r * f z

Tactic:
classical exact
    have : (f.sum fun a b => ite (x * a = y) (0 * b) 0) = 0 := by simp
    calc
      (single x r * f) y
      _ = sum f fun a b => ite (x * a = y) (r * b) 0 :=
        (mul_apply _ _ _).trans <| sum_single_index this
      _ = f.sum fun a b => ite (a = z) (r * b) 0 := Finsupp.sum_congr fun x hx => by
        simp only [H _ hx]
      _ = if z ∈ f.support then r * f z else 0 := f.support.sum_ite_eq' _ _
      _ = _ := by split_ifs with h <;> simp at h <;> simp [h]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x y z : G
H : ∀ a ∈ f.support, x * a = y ↔ a = z
⊢ (single x r * f) y = r * f z

Tactic:
exact
have : (f.sum fun a b => ite (x * a = y) (0 * b) 0) = 0 := by simp
calc
(single x r * f) y
_ = sum f fun a b => ite (x * a = y) (r * b) 0 :=
(mul_apply _ _ _).trans <| sum_single_index this
_ = f.sum fun a b => ite (a = z) (r * b) 0 := Finsupp.sum_congr fun x hx => by
simp only [H _ hx]
_ = if z ∈ f.support then r * f z else 0 := f.support.sum_ite_eq' _ _
_ = _ := by split_ifs with h <;> simp at h <;> simp [h]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x✝ y z : G
H : ∀ a ∈ f.support, x✝ * a = y ↔ a = z
this : (sum f fun a b => if x✝ * a = y then 0 * b else 0) = 0
x : G
hx : x ∈ f.support
⊢ (if x✝ * x = y then r * f x else 0) = if x = z then r * f x else 0

Tactic:
simp only [H _ hx]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x y z : G
H : ∀ a ∈ f.support, x * a = y ↔ a = z
this : (sum f fun a b => if x * a = y then 0 * b else 0) = 0
⊢ (if z ∈ f.support then r * f z else 0) = r * f z

Tactic:
split_ifs with h <;> simp at h <;> simp [h]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
x y z : G
H : ∀ a ∈ f.support, x * a = y ↔ a = z
⊢ (sum f fun a b => if x * a = y then 0 * b else 0) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem parallel_iff_direction_eq_and_eq_bot_iff_eq_bot {s₁ s₂ : AffineSubspace k P} :
    s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)

Tactic:
refine ⟨fun h => ⟨h.direction_eq, ?_, ?_⟩, fun h => ?_⟩

Result:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₁ = ⊥ → s₂ = ⊥

case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₂ = ⊥ → s₁ = ⊥

case refine_3
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
⊢ s₁ ∥ s₂

Proof state:
case neg.intro.intro.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ ∃ y ∈ s₁, ↑(constVAdd k P (p₂ -ᵥ p₁)) y = p₂

Tactic:
refine ⟨p₁, hp₁, ?_⟩

Result:
case neg.intro.intro.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ ↑(constVAdd k P (p₂ -ᵥ p₁)) p₁ = p₂

Proof state:
case neg.intro.intro.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ p₂ ∈ map (↑(constVAdd k P (p₂ -ᵥ p₁))) s₁

Tactic:
rw [mem_map]

Result:
case neg.intro.intro.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ ∃ y ∈ s₁, ↑(constVAdd k P (p₂ -ᵥ p₁)) y = p₂
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma zeroLocus_span {U : X.Opens} (s : Set Γ(X, U)) :
    X.zeroLocus (U := U) (Ideal.span s) = X.zeroLocus s

Proof state:
case h.refine_1
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ x ∉ X.basicOpen 0

Tactic:
simp only [Scheme.basicOpen_zero]

Result:
case h.refine_1
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ x ∉ ⊥

Proof state:
case h.refine_2
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (x_1 y : ↑Γ(X, U)),
    x_1 ∈ Submodule.span (↑Γ(X, U)) s →
      y ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)

Tactic:
exact fun a b _ _ ha hb H ↦ (X.basicOpen_add_le a b H).elim ha hb

Result:
no goals

Proof state:
case h.refine_1
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ x ∉ ⊥

Tactic:
exact not_false

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ X.zeroLocus ↑(Ideal.span s) = X.zeroLocus s

Tactic:
ext x

Result:
case h
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus ↑(Ideal.span s) ↔ x ∈ X.zeroLocus s

Proof state:
case h
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus ↑(Ideal.span s) ↔ x ∈ X.zeroLocus s

Tactic:
simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]

Result:
case h
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
⊢ (∀ f ∈ Ideal.span s, x ∉ X.basicOpen f) ↔ ∀ f ∈ s, x ∉ X.basicOpen f

Proof state:
case h
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
⊢ (∀ f ∈ Ideal.span s, x ∉ X.basicOpen f) ↔ ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
refine ⟨fun H f hfs ↦ H f (Ideal.subset_span hfs), fun H f ↦ Submodule.span_induction H ?_ ?_ ?_⟩

Result:
case h.refine_1
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ x ∉ X.basicOpen 0

case h.refine_2
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (x_1 y : ↑Γ(X, U)),
    x_1 ∈ Submodule.span (↑Γ(X, U)) s →
      y ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)

case h.refine_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (a x_1 : ↑Γ(X, U)), x_1 ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen (a • x_1)

Proof state:
case h.refine_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : ↑Γ(X, U)
⊢ ∀ (a x_1 : ↑Γ(X, U)), x_1 ∈ Submodule.span (↑Γ(X, U)) s → x ∉ X.basicOpen x_1 → x ∉ X.basicOpen (a • x_1)

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
theorem sheaf_condition : R.IsSheafFor P ↔ Nonempty (IsLimit (Fork.ofι _ (w P R)))

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
⊢ (∃! t, x.IsAmalgamation t) ↔ ∃! x_1, forkMap P R x_1 = (firstObjEqFamily P R).toEquiv.symm x

Tactic:
apply existsUnique_congr

Result:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
⊢ ∀ (a : P.obj (op X)), x.IsAmalgamation a ↔ forkMap P R a = (firstObjEqFamily P R).toEquiv.symm x
-- Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
theorem normalizeIsoApp_eq :
    ∀ (X : F C) (n : N C), normalizeIsoApp C X n = normalizeIsoApp' C X n.as
  | of _, _ => rfl
  | unit, _ => rfl
  | tensor X Y, n => by
      rw [normalizeIsoApp, normalizeIsoApp']
      rw [normalizeIsoApp_eq X n]
      rw [normalizeIsoApp_eq Y ⟨normalizeObj X n.as⟩]
      rfl

Proof state:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ normalizeIsoApp C (X.tensor Y) n = normalizeIsoApp' C (X.tensor Y) n.as

Tactic:
rw [normalizeIsoApp, normalizeIsoApp']

Result:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusion.obj { as := n.as }) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp C X n) Y ≪≫ normalizeIsoApp C Y { as := X.normalizeObj n.as } =
    (α_ (inclusionObj n.as) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp' C X n.as) Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)

Proof state:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusion.obj { as := n.as }) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp' C X n.as) Y ≪≫ normalizeIsoApp' C Y { as := X.normalizeObj n.as }.as =
    (α_ (inclusionObj n.as) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp' C X n.as) Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusion.obj { as := n.as }) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp C X n) Y ≪≫ normalizeIsoApp C Y { as := X.normalizeObj n.as } =
    (α_ (inclusionObj n.as) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp' C X n.as) Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)

Tactic:
rw [normalizeIsoApp_eq X n]

Result:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusion.obj { as := n.as }) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp' C X n.as) Y ≪≫ normalizeIsoApp C Y { as := X.normalizeObj n.as } =
    (α_ (inclusionObj n.as) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp' C X n.as) Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)

Proof state:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusion.obj { as := n.as }) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp' C X n.as) Y ≪≫ normalizeIsoApp C Y { as := X.normalizeObj n.as } =
    (α_ (inclusionObj n.as) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp' C X n.as) Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)

Tactic:
rw [normalizeIsoApp_eq Y ⟨normalizeObj X n.as⟩]

Result:
C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusion.obj { as := n.as }) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp' C X n.as) Y ≪≫ normalizeIsoApp' C Y { as := X.normalizeObj n.as }.as =
    (α_ (inclusionObj n.as) X Y).symm ≪≫
      whiskerRightIso (normalizeIsoApp' C X n.as) Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)
-- Mathlib/GroupTheory/Sylow.lean
theorem ext {P Q : Sylow p G} (h : (P : Subgroup G) = Q) : P = Q

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
P Q : Sylow p G
h : ↑P = ↑Q
⊢ P = Q

Tactic:
cases P

Result:
case mk
p : ℕ
G : Type u_1
inst✝ : Group G
Q : Sylow p G
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p ↥toSubgroup✝
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h : ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = ↑Q
⊢ { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = Q

Proof state:
case mk.mk
p : ℕ
G : Type u_1
inst✝ : Group G
toSubgroup✝¹ : Subgroup G
isPGroup'✝¹ : IsPGroup p ↥toSubgroup✝¹
is_maximal'✝¹ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝¹ ≤ Q → Q = toSubgroup✝¹
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p ↥toSubgroup✝
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h :
  ↑{ toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
⊢ { toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }

Tactic:
congr

Result:
no goals

Proof state:
case mk
p : ℕ
G : Type u_1
inst✝ : Group G
Q : Sylow p G
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p ↥toSubgroup✝
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h : ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = ↑Q
⊢ { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = Q

Tactic:
cases Q

Result:
case mk.mk
p : ℕ
G : Type u_1
inst✝ : Group G
toSubgroup✝¹ : Subgroup G
isPGroup'✝¹ : IsPGroup p ↥toSubgroup✝¹
is_maximal'✝¹ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝¹ ≤ Q → Q = toSubgroup✝¹
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p ↥toSubgroup✝
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h :
  ↑{ toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
⊢ { toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem extract_congr (start len : Nat) (w : Nat) (x x' : BitVec w) (h1 : x = x') :
    BitVec.extractLsb' start len x' = BitVec.extractLsb' start len x

Proof state:
start len w : Nat
x x' : BitVec w
h1 : x = x'
⊢ BitVec.extractLsb' start len x' = BitVec.extractLsb' start len x

Tactic:
simp[*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_ushiftRight_lt (x : BitVec w) (n : Nat) (hn : n ≤ w) :
    (x >>> n).toNat < 2 ^ (w - n)

Proof state:
case h
w : Nat
x : BitVec w
n : Nat
hn : n ≤ w
⊢ n ≤ w

Tactic:
apply hn

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : n ≤ w
⊢ x.toNat < 2 ^ w

Tactic:
apply x.isLt

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : n ≤ w
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : n ≤ w
⊢ x.toNat < 2 ^ (w - n) * 2 ^ n

Tactic:
rw [Nat.pow_sub_mul_pow]

Result:
w : Nat
x : BitVec w
n : Nat
hn : n ≤ w
⊢ x.toNat < 2 ^ w

case h
w : Nat
x : BitVec w
n : Nat
hn : n ≤ w
⊢ n ≤ w

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : n ≤ w
⊢ 0 < 2 ^ n

Tactic:
apply Nat.pow_pos (by decide)

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : n ≤ w
⊢ (x >>> n).toNat < 2 ^ (w - n)

Tactic:
rw [toNat_ushiftRight, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul]

Result:
w : Nat
x : BitVec w
n : Nat
hn : n ≤ w
⊢ x.toNat < 2 ^ (w - n) * 2 ^ n

w : Nat
x : BitVec w
n : Nat
hn : n ≤ w
⊢ 0 < 2 ^ n
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
theorem lineMap_slope_lineMap_slope_lineMap (f : k → PE) (a b r : k) :
    lineMap (slope f (lineMap a b r) b) (slope f a (lineMap a b r)) r = slope f a b

Proof state:
case h.e'_2.h.e'_6
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ r = (a - (lineMap a b) r) / (a - b)

Tactic:
rw [lineMap_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub,
  sub_sub_cancel]

Result:
no goals

Proof state:
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ (lineMap (slope f b ((lineMap a b) r)) (slope f ((lineMap a b) r) a)) r = slope f b a

Tactic:
convert lineMap_slope_slope_sub_div_sub f b (lineMap a b r) a hab.symm using 2

Result:
case h.e'_2.h.e'_6
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ r = (a - (lineMap a b) r) / (a - b)

Proof state:
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ (lineMap (slope f ((lineMap a b) r) b) (slope f a ((lineMap a b) r))) r = slope f a b

Tactic:
rw [slope_comm _ a, slope_comm _ a, slope_comm _ _ b]

Result:
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ (lineMap (slope f b ((lineMap a b) r)) (slope f ((lineMap a b) r) a)) r = slope f b a

Proof state:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
⊢ (lineMap (slope f ((lineMap a b) r) b) (slope f a ((lineMap a b) r))) r = slope f a b

Tactic:
obtain rfl | hab : a = b ∨ a ≠ b := Classical.em _

Result:
case inl
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a r : k
⊢ (lineMap (slope f ((lineMap a a) r) a) (slope f a ((lineMap a a) r))) r = slope f a a

case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
⊢ (lineMap (slope f ((lineMap a b) r) b) (slope f a ((lineMap a b) r))) r = slope f a b

Proof state:
case inl
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a r : k
⊢ (lineMap (slope f ((lineMap a a) r) a) (slope f a ((lineMap a a) r))) r = slope f a a

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsNat.to_isRat {α} [Ring α] : ∀ {a : α} {n}, IsNat a n → IsRat a (.ofNat n) (nat_lit 1)
  | _, _, ⟨rfl⟩ => ⟨⟨1, by simp, by simp⟩, by simp⟩

Proof state:
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ 1 * ↑1 = 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑n✝ = ↑(Int.ofNat n✝) * ⅟↑1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑1 * 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma semilength_eq_count_D : p.semilength = p.toList.count D

Proof state:
p : DyckWord
⊢ p.semilength = count D ↑p

Tactic:
rw [← count_U_eq_count_D]

Result:
p : DyckWord
⊢ p.semilength = count U ↑p

Proof state:
p : DyckWord
⊢ p.semilength = count U ↑p

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem sum_mongePointWeightsWithCircumcenter (n : ℕ) :
    ∑ i, mongePointWeightsWithCircumcenter n i = 1

Proof state:
n : ℕ
⊢ ↑(n + 2 + 1) * (↑(n + 1))⁻¹ + -2 / ↑(n + 1) = 1

Tactic:
simp (disch := field_simp_discharge) only [Nat.cast_add, Nat.cast_ofNat, Nat.cast_one,
  inv_eq_one_div, mul_div_assoc', mul_one, add_div', div_mul_cancel₀, div_eq_iff, one_mul]

Result:
n : ℕ
⊢ ↑n + 2 + 1 + -2 = ↑n + 1

Proof state:
n : ℕ
⊢ ∑ i : PointsWithCircumcenterIndex (n + 2), mongePointWeightsWithCircumcenter n i = 1

Tactic:
simp_rw [sum_pointsWithCircumcenter, mongePointWeightsWithCircumcenter, sum_const, card_fin,
  nsmul_eq_mul]

Result:
n : ℕ
⊢ ↑(n + 2 + 1) * (↑(n + 1))⁻¹ + -2 / ↑(n + 1) = 1

Proof state:
n : ℕ
⊢ ↑n + 2 + 1 + -2 = ↑n + 1

Tactic:
ring

Result:
no goals