harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Setoid/Basic.lean
theorem eqvGen_le {r : α → α → Prop} {s : Setoid α} (h : ∀ x y, r x y → s x y) :
    EqvGen.setoid r ≤ s

Proof state:
α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → s x y
⊢ EqvGen.setoid r ≤ s

Tactic:
rw [eqvGen_eq]

Result:
α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → s x y
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ s

Proof state:
α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → s x y
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ s

Tactic:
exact sInf_le h

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive]
lemma SeminormedGroup.disjoint_nhds_one (f : Filter E) :
    Disjoint (𝓝 1) f ↔ ∃ δ > 0, ∀ᶠ y in f, δ ≤ ‖y‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
f : Filter E
⊢ Disjoint (𝓝 1) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖

Tactic:
simpa using disjoint_nhds 1 f

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem intCoe_one [AddGroupWithOne R] : ((1 : ArithmeticFunction ℤ) :
    ArithmeticFunction R) = 1

Proof state:
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑1 n = 1 n

Proof state:
case h
R : Type u_1
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑1 n = 1 n

Tactic:
simp [one_apply]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem strictMono_rpow_of_pos {z : ℝ} (h : 0 < z) : StrictMono fun x : ℝ≥0 => x ^ z :=
  fun x y hxy => by simp only [NNReal.rpow_lt_rpow hxy h, coe_lt_coe]

Proof state:
z : ℝ
h : 0 < z
x y : ℝ≥0
hxy : x < y
⊢ (fun x => x ^ z) x < (fun x => x ^ z) y

Tactic:
simp only [NNReal.rpow_lt_rpow hxy h, coe_lt_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eq_isSome_getKey? [BEq α] {l : List ((a : α) × β a)} {a : α} :
    containsKey a l = (getKey? a l).isSome

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a : α
⊢ containsKey a l = (getKey? a l).isSome

Tactic:
simp [containsKey_eq_isSome_getEntry?, getKey?_eq_getEntry?]

Result:
no goals
-- Mathlib/CategoryTheory/Category/RelCat.lean
theorem rel_comp_apply₂ {X Y Z : RelCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) (z : Z) :
    (f ≫ g) x z ↔ ∃ y, f x y ∧ g y z

Proof state:
X Y Z : RelCat
f : X ⟶ Y
g : Y ⟶ Z
x : X
z : Z
⊢ (f ≫ g) x z ↔ ∃ y, f x y ∧ g y z

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
lemma factorizationLCMLeft_pos :
    0 < factorizationLCMLeft a b

Proof state:
case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : b.factorization p ≤ a.factorization p
⊢ False

Tactic:
simp only [h, reduceIte, pow_eq_zero_iff', ne_eq] at H

Result:
case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
H : p = 0 ∧ ¬(a.lcm b).factorization p = 0
⊢ False

Proof state:
case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False

Tactic:
simp only [h, reduceIte, one_ne_zero] at H

Result:
no goals

Proof state:
case a
a b : ℕ
⊢ a.factorizationLCMLeft b ≠ 0

Tactic:
rw [factorizationLCMLeft, Finsupp.prod_ne_zero_iff]

Result:
case a
a b : ℕ
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (if b.factorization i ≤ a.factorization i then i ^ (a.lcm b).factorization i else 1) ≠ 0

Proof state:
case a
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
⊢ False

Tactic:
by_cases h : b.factorization p ≤ a.factorization p

Result:
case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : b.factorization p ≤ a.factorization p
⊢ False

case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False

Proof state:
case pos
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
H : p = 0 ∧ ¬(a.lcm b).factorization p = 0
⊢ False

Tactic:
simpa [H.1] using H.2

Result:
no goals

Proof state:
case a
a b : ℕ
⊢ ∀ i ∈ (a.lcm b).factorization.support,
    (if b.factorization i ≤ a.factorization i then i ^ (a.lcm b).factorization i else 1) ≠ 0

Tactic:
intro p _ H

Result:
case a
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
⊢ False

Proof state:
a b : ℕ
⊢ 0 < a.factorizationLCMLeft b

Tactic:
apply Nat.pos_of_ne_zero

Result:
case a
a b : ℕ
⊢ a.factorizationLCMLeft b ≠ 0
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem ι_colimitConstInitial_hom {J : Type*} [Category J] {C : Type*} [Category C] [HasInitial C]
    {j : J} :
    colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom =
      initial.to _

Proof state:
J : Type u_1
inst✝² : Category.{u_3, u_1} J
C : Type u_2
inst✝¹ : Category.{u_4, u_2} C
inst✝ : HasInitial C
j : J
⊢ colimit.ι ((Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom = initial.to (⊥_ C)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma RationalMap.mem_domain {f : X ⤏ Y} {x} :
    x ∈ f.domain ↔ ∃ g : X.PartialMap Y, x ∈ g.domain ∧ g.toRationalMap = f :=
  TopologicalSpace.Opens.mem_sSup.trans (by simp [@and_comm (x ∈ _)])

Proof state:
X Y : Scheme
f : X ⤏ Y
x : ↑↑X.toPresheafedSpace
⊢ (∃ u ∈ {x | ∃ g, ∃ (_ : g.toRationalMap = f), g.domain = x}, x ∈ u) ↔ ∃ g, x ∈ g.domain ∧ g.toRationalMap = f

Tactic:
simp [@and_comm (x ∈ _)]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma coyonedaEquiv_naturality {X Y : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op X) ⟶ F)
    (g : X ⟶ Y) : F.map g (coyonedaEquiv f) = coyonedaEquiv (coyoneda.map g.op ≫ f)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ (f.app X ≫ F.map g) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)

Tactic:
rw [← f.naturality]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ ((coyoneda.obj (op X)).map g ≫ f.app Y) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ F.map g (coyonedaEquiv f) = coyonedaEquiv (coyoneda.map g.op ≫ f)

Tactic:
change (f.app X ≫ F.map g) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ (f.app X ≫ F.map g) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ f.app Y (𝟙 X ≫ g) = f.app Y (g ≫ 𝟙 Y)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ ((coyoneda.obj (op X)).map g ≫ f.app Y) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)

Tactic:
dsimp

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ f.app Y (𝟙 X ≫ g) = f.app Y (g ≫ 𝟙 Y)
-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem rayleigh_smul (x : E) {c : 𝕜} (hc : c ≠ 0) :
    rayleighQuotient T (c • x) = rayleighQuotient T x

Proof state:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : x = 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Tactic:
simp [hx]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Tactic:
by_cases hx : x = 0

Result:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : x = 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : ¬x = 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Proof state:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : ¬x = 0
⊢ ‖c‖ ^ 2 * T.reApplyInnerSelf x * ‖x‖ ^ 2 = T.reApplyInnerSelf x * (‖c‖ * ‖x‖) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : ¬x = 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Tactic:
field_simp [norm_smul, T.reApplyInnerSelf_smul]

Result:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : ¬x = 0
⊢ ‖c‖ ^ 2 * T.reApplyInnerSelf x * ‖x‖ ^ 2 = T.reApplyInnerSelf x * (‖c‖ * ‖x‖) ^ 2
-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_le_of_emultiplicity_le {n : ℕ} (h : emultiplicity a b ≤ n) :
    multiplicity a b ≤ n

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b ≤ ↑n
⊢ multiplicity a b ≤ n

Tactic:
exact_mod_cast multiplicity_le_emultiplicity.trans h

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_principal_principal {f : α → β} {s : Set α} {t : Set β} :
    Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ a ∈ s, f a ∈ t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ a ∈ s, f a ∈ t

Tactic:
simp only [tendsto_principal, eventually_principal]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc]
lemma unit_app_tensor_comp_map_δ (X Y : C) :
    adj.unit.app (X ⊗ Y) ≫ G.map (δ F X Y) = (adj.unit.app X ⊗ adj.unit.app Y) ≫ μ G _ _

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.OplaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ adj.unit.app (X ⊗ Y) ≫ G.map (δ F X Y) = (adj.unit.app X ⊗ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)

Tactic:
rw [IsMonoidal.leftAdjoint_μ (adj := adj), homEquiv_unit]

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.OplaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ adj.unit.app (X ⊗ Y) ≫ G.map (δ F X Y) =
    (adj.unit.app X ⊗ adj.unit.app Y) ≫
      adj.unit.app (G.obj (F.obj X) ⊗ G.obj (F.obj Y)) ≫
        G.map (δ F (G.obj (F.obj X)) (G.obj (F.obj Y)) ≫ (adj.counit.app (F.obj X) ⊗ adj.counit.app (F.obj Y)))

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.OplaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ adj.unit.app (X ⊗ Y) ≫ G.map (δ F X Y) =
    (adj.unit.app X ⊗ adj.unit.app Y) ≫
      adj.unit.app (G.obj (F.obj X) ⊗ G.obj (F.obj Y)) ≫
        G.map (δ F (G.obj (F.obj X)) (G.obj (F.obj Y)) ≫ (adj.counit.app (F.obj X) ⊗ adj.counit.app (F.obj Y)))

Tactic:
simp only [← adj.unit_naturality_assoc, ← Functor.map_comp, ← δ_natural_assoc,
  ← tensor_comp, left_triangle_components, tensorHom_id, id_whiskerRight, comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_append_of_containsKey_eq_false [BEq α] [LawfulBEq α]
    {l l' : List ((a : α) × β a)} {a : α} {h} (hl' : containsKey a l' = false) :
    getValueCast a (l ++ l') h =
      getValueCast a l ((containsKey_append_of_not_contains_right hl').symm.trans h)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l l' : List ((a : α) × β a)
a : α
h : containsKey a (l ++ l') = true
hl' : containsKey a l' = false
⊢ getValueCast a (l ++ l') h = getValueCast a l ⋯

Tactic:
rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, ← getValueCast?_eq_some_getValueCast,
  getValueCast?_append_of_containsKey_eq_false hl']

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem associated_pi [Invertible (2 : R)] (Q : ∀ i, QuadraticMap R (Mᵢ i) P) :
    associated (pi Q) = ∑ i, (Q i).associated.compl₁₂ (.proj i) (.proj i)

Proof state:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝⁴ : AddCommGroup P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : Invertible 2
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ associated (pi Q) = ∑ i : ι, LinearMap.compl₁₂ (associated (Q i)) (LinearMap.proj i) (LinearMap.proj i)

Tactic:
dsimp [associated, associatedHom]

Result:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝⁴ : AddCommGroup P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : Invertible 2
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ ⅟2 • (pi Q).polarBilin = ∑ i : ι, LinearMap.compl₁₂ (⅟2 • (Q i).polarBilin) (LinearMap.proj i) (LinearMap.proj i)

Proof state:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝⁴ : AddCommGroup P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : Invertible 2
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ ∑ x : ι, ⅟2 • LinearMap.compl₁₂ (Q x).polarBilin (LinearMap.proj x) (LinearMap.proj x) =
    ∑ i : ι, LinearMap.compl₁₂ (⅟2 • (Q i).polarBilin) (LinearMap.proj i) (LinearMap.proj i)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝⁴ : AddCommGroup P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : Invertible 2
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ ⅟2 • (pi Q).polarBilin = ∑ i : ι, LinearMap.compl₁₂ (⅟2 • (Q i).polarBilin) (LinearMap.proj i) (LinearMap.proj i)

Tactic:
rw [polarBilin_pi, Finset.smul_sum]

Result:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝⁴ : AddCommGroup P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : Invertible 2
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
⊢ ∑ x : ι, ⅟2 • LinearMap.compl₁₂ (Q x).polarBilin (LinearMap.proj x) (LinearMap.proj x) =
    ∑ i : ι, LinearMap.compl₁₂ (⅟2 • (Q i).polarBilin) (LinearMap.proj i) (LinearMap.proj i)
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_add [Add α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α)
    (D : Matrix o m α) (A' : Matrix n l α) (B' : Matrix n m α) (C' : Matrix o l α)
    (D' : Matrix o m α) : fromBlocks A B C D + fromBlocks A' B' C' D' =
      fromBlocks (A + A') (B + B') (C + C') (D + D')

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
⊢ fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A + A') (B + B') (C + C') (D + D')

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Perfectoid/Untilt.lean
lemma exists_smodEq_untiltAux (x : PreTilt O p) :
    ∃ y, ∀ (n : ℕ), x.untiltAux n ≡ y [SMOD Ideal.span {(p : O)} ^ n • (⊤ : Ideal O)]

Proof state:
O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsPrecomplete (span {↑p}) O
x : PreTilt O p
m n : ℕ
h : m ≤ n
⊢ x.untiltAux m ≡ x.untiltAux n [SMOD span {↑p} ^ m • ⊤]

Tactic:
simpa only [span_singleton_pow, smul_eq_mul, mul_top, SModEq.sub_mem,
    mem_span_singleton] using x.pow_dvd_untiltAux_sub_untiltAux h

Result:
no goals

Proof state:
O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsPrecomplete (span {↑p}) O
x : PreTilt O p
⊢ ∃ y, ∀ (n : ℕ), x.untiltAux n ≡ y [SMOD span {↑p} ^ n • ⊤]

Tactic:
refine IsPrecomplete.prec' x.untiltAux (fun {m n} h ↦ ?_)

Result:
O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsPrecomplete (span {↑p}) O
x : PreTilt O p
m n : ℕ
h : m ≤ n
⊢ x.untiltAux m ≡ x.untiltAux n [SMOD span {↑p} ^ m • ⊤]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Mem.lean
theorem sizeOf_get [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf (as.get i h) < sizeOf as

Proof state:
α : Type u_1
inst✝ : SizeOf α
as : Array α
i : Nat
h : i < as.size
⊢ sizeOf (as.get i h) < sizeOf as

Tactic:
cases as with | _ as =>
simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp_arith)

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝ : SizeOf α
i : Nat
as : List α
h : i < { toList := as }.size
⊢ sizeOf ({ toList := as }.get i h) < sizeOf { toList := as }

Tactic:
simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp_arith)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SizeOf α
i : Nat
as : List α
h : i < { toList := as }.size
⊢ sizeOf { toList := as }.toList < 1 + sizeOf as

Tactic:
simp_arith

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem iInf_localization_eq_bot : ⨅ v : PrimeSpectrum R,
    Localization.subalgebra.ofField K _ (v.asIdeal.primeCompl_le_nonZeroDivisors) = ⊥

Proof state:
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : K
⊢ x✝ ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ →
    x✝ ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯

Tactic:
simpa only [Algebra.mem_iInf] using fun hx ⟨v, hv⟩ ↦ hx ⟨v, hv.isPrime⟩

Result:
no goals

Proof state:
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥

Tactic:
refine bot_unique (.trans (fun _ ↦ ?_) (MaximalSpectrum.iInf_localization_eq_bot R K).le)

Result:
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : K
⊢ x✝ ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ →
    x✝ ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_div {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : √(x / y) = √x / √y

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x / y) = √x / √y

Tactic:
rw [division_def, sqrt_mul hx, sqrt_inv, division_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem xor_not : ∀ (x y : Bool), (x ^^ !y) = !(x ^^ y)

Proof state:
⊢ ∀ (x y : Bool), (x ^^ !y) = !(x ^^ y)

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_sub_sq (x y : E) : ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2

Tactic:
rw [sub_eq_add_neg, @norm_add_sq 𝕜 _ _ _ _ x (-y), norm_neg, inner_neg_right, map_neg, mul_neg,
  sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem getElem_range {n : Nat} (m) (h : m < (range n).length) : (range n)[m] = m

Proof state:
n m : Nat
h : m < (range n).length
⊢ (range n)[m] = m

Tactic:
simp [range_eq_range']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem idxOf?_cons [BEq α] (a : α) (xs : List α) (b : α) :
    (a :: xs).idxOf? b = if a == b then some 0 else (xs.idxOf? b).map (· + 1)

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
xs : List α
b : α
⊢ idxOf? b (a :: xs) = if (a == b) = true then some 0 else Option.map (fun x => x + 1) (idxOf? b xs)

Tactic:
simp [idxOf?]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Icc_self (a : α) : Icc a a = {a}

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Icc a a = {a}

Tactic:
rw [Icc, Finset.Icc_self, Finset.singleton_val]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem _root_.Set.Countable.measure_zero (h : s.Countable) (μ : Measure α) [NoAtoms μ] :
    μ s = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst✝ : NoAtoms μ
⊢ ∀ i ∈ s, μ {i} = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst✝ : NoAtoms μ
⊢ μ s = 0

Tactic:
rw [← biUnion_of_singleton s, measure_biUnion_null_iff h]

Result:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst✝ : NoAtoms μ
⊢ ∀ i ∈ s, μ {i} = 0