harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/AddTorsor.lean
theorem smul_lt_smul_of_le_of_lt [LE G] [Preorder P] [SMul G P] [IsOrderedCancelSMul G P]
    {a b : G} {c d : P} (h₁ : a ≤ b) (h₂ : c < d) :
  a • c < b • d

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ b • c < b • d

Tactic:
refine lt_of_le_not_le (IsOrderedSMul.smul_le_smul_left c d (le_of_lt h₂) b) ?_

Result:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ ¬b • d ≤ b • c

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ False

Tactic:
rw [@lt_iff_le_not_le] at h₂

Result:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c ≤ d ∧ ¬d ≤ c
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ False

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c ≤ d ∧ ¬d ≤ c
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ False

Tactic:
simp_all only [not_true_eq_false, and_false]

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ ¬b • d ≤ b • c

Tactic:
by_contra hbdc

Result:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
⊢ False

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
⊢ False

Tactic:
have h : d ≤ c := IsOrderedCancelSMul.le_of_smul_le_smul_left b d c hbdc

Result:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ False

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ a • c < b • d

Tactic:
refine lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_right a b h₁ c) ?_

Result:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ b • c < b • d
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_one_left_iff : (fun _x => 1 : α → F) =o[l] f ↔ Tendsto (fun x => ‖f x‖) l atTop :=
  calc
    (fun _x => 1 : α → F) =o[l] f ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖(1 : F)‖ ≤ ‖f x‖ :=
      isLittleO_iff_nat_mul_le_aux <| Or.inl fun _x => by simp only [norm_one, zero_le_one]
    _ ↔ ∀ n : ℕ, True → ∀ᶠ x in l, ‖f x‖ ∈ Ici (n : ℝ)

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
f : α → E
l : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖1‖ ≤ ‖f x‖) ↔ ∀ (n : ℕ), True → ∀ᶠ (x : α) in l, ‖f x‖ ∈ Ici ↑n

Tactic:
simp only [norm_one, mul_one, true_imp_iff, mem_Ici]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
f : α → E
l : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
_x : α
⊢ 0 ≤ ‖1‖

Tactic:
simp only [norm_one, zero_le_one]

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem y_zpow_pos {a : Solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) {n : ℤ} (hn : 0 < n) :
    0 < (a ^ n).y

Proof state:
case intro
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : 0 < ↑n
⊢ 0 < (a ^ ↑n).y

Tactic:
norm_cast at hn ⊢

Result:
case intro
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : 0 < n
⊢ 0 < (a ^ n).y

Proof state:
case intro
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : 0 < n
⊢ 0 < (a ^ n).y

Tactic:
rw [← Nat.succ_pred_eq_of_pos hn]

Result:
case intro
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : 0 < n
⊢ 0 < (a ^ n.pred.succ).y

Proof state:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℤ
hn : 0 < n
⊢ 0 < (a ^ n).y

Tactic:
lift n to ℕ using hn.le

Result:
case intro
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : 0 < ↑n
⊢ 0 < (a ^ ↑n).y

Proof state:
case intro
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : 0 < n
⊢ 0 < (a ^ n.pred.succ).y

Tactic:
exact y_pow_succ_pos hax hay _

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.isBasis_iff_forall_insert_dep (hI : M.Indep I) (hIX : I ⊆ X) :
    M.IsBasis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I)

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(M.Indep (insert x I) ∧ insert x I ⊆ X)) ∧ X ⊆ M.E ↔ ∀ e ∈ X \ I, M.Dep (insert e I)

Tactic:
simp only [hI, hIX, and_self, insert_subset_iff, and_true, not_and, true_and, mem_diff, and_imp,
  Dep, hI.subset_ground]

Result:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ (∀ x ∉ I, M.Indep (insert x I) → x ∉ X) ∧ X ⊆ M.E ↔ ∀ e ∈ X, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ (∀ x ∉ I, M.Indep (insert x I) → x ∉ X) ∧ X ⊆ M.E ↔ ∀ e ∈ X, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E

Tactic:
exact ⟨fun h e heX heI ↦ ⟨fun hi ↦ h.1 e heI hi heX, h.2 heX⟩,
  fun h ↦ ⟨fun e heI hi heX ↦ (h e heX heI).1 hi,
    fun e heX ↦ (em (e ∈ I)).elim (fun h ↦ hI.subset_ground h) fun heI ↦ (h _ heX heI).2 ⟩⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ M.IsBasis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I)

Tactic:
rw [IsBasis, maximal_iff_forall_insert (fun I J hI hIJ ↦ ⟨hI.1.subset hIJ, hIJ.trans hI.2⟩)]

Result:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ x ∉ I, ¬(M.Indep (insert x I) ∧ insert x I ⊆ X)) ∧ X ⊆ M.E ↔ ∀ e ∈ X \ I, M.Dep (insert e I)
-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma closedBall_eq_or_disjoint :
    closedBall x r = closedBall y r ∨ Disjoint (closedBall x r) (closedBall y r)

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (closedBall x r ∩ closedBall y r).Nonempty
h₁ : closedBall x r = closedBall h.some r
h₂ : closedBall y r = closedBall h.some r
⊢ closedBall x r = closedBall y r

Tactic:
exact h₁.trans h₂.symm

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (closedBall x r ∩ closedBall y r).Nonempty
h₁ : closedBall x r = closedBall h.some r
⊢ closedBall x r = closedBall y r

Tactic:
have h₂ := closedBall_eq_of_mem <| Set.inter_subset_right h.some_mem

Result:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (closedBall x r ∩ closedBall y r).Nonempty
h₁ : closedBall x r = closedBall h.some r
h₂ : closedBall y r = closedBall h.some r
⊢ closedBall x r = closedBall y r

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
⊢ closedBall x r = closedBall y r ∨ Disjoint (closedBall x r) (closedBall y r)

Tactic:
refine Set.disjoint_or_nonempty_inter (closedBall x r) (closedBall y r) |>.symm.imp
  (fun h ↦ ?_) id

Result:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (closedBall x r ∩ closedBall y r).Nonempty
⊢ closedBall x r = closedBall y r

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (closedBall x r ∩ closedBall y r).Nonempty
⊢ closedBall x r = closedBall y r

Tactic:
have h₁ := closedBall_eq_of_mem <| Set.inter_subset_left h.some_mem

Result:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (closedBall x r ∩ closedBall y r).Nonempty
h₁ : closedBall x r = closedBall h.some r
⊢ closedBall x r = closedBall y r
-- Mathlib/Algebra/Group/Defs.lean
theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹

Proof state:
G : Type u_1
inst✝ : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ (n + 1))⁻¹

Tactic:
rw [← zpow_natCast]

Result:
G : Type u_1
inst✝ : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ ↑(n + 1))⁻¹

Proof state:
G : Type u_1
inst✝ : DivInvMonoid G
a : G
n : ℕ
⊢ a ^ Int.negSucc n = (a ^ ↑(n + 1))⁻¹

Tactic:
exact DivInvMonoid.zpow_neg' n a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem finIdxOf?_toList [BEq α] (a : α) (v : Array α) :
    v.toList.finIdxOf? a = (v.finIdxOf? a).map (Fin.cast (by simp))

Proof state:
α : Type ?u.536226
inst✝ : BEq α
a : α
v : Array α
⊢ v.size = v.toList.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
v : Array α
⊢ List.finIdxOf? a v.toList = Option.map (Fin.cast ⋯) (v.finIdxOf? a)

Tactic:
rcases v with ⟨v⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
v : List α
⊢ List.finIdxOf? a { toList := v }.toList = Option.map (Fin.cast ⋯) ({ toList := v }.finIdxOf? a)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
v : List α
⊢ List.finIdxOf? a { toList := v }.toList = Option.map (Fin.cast ⋯) ({ toList := v }.finIdxOf? a)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem signAux_swap : ∀ {n : ℕ} {x y : Fin n} (_hxy : x ≠ y), signAux (swap x y) = -1
  | 0, x, y => by intro; exact Fin.elim0 x
  | 1, x, y => by
    dsimp [signAux, swap, swapCore]
    simp only [eq_iff_true_of_subsingleton, not_true, ite_true, le_refl, prod_const,
               IsEmpty.forall_iff]
  | n + 2, x, y => fun hxy => by
    have h2n : 2 ≤ n + 2

Proof state:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ (swap x y).signAux = -1

Tactic:
have h2n : 2 ≤ n + 2 := by exact le_add_self

Result:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ (swap x y).signAux = -1

Proof state:
x y : Fin 1
⊢ x ≠ y → (swap x y).signAux = -1

Tactic:
dsimp [signAux, swap, swapCore]

Result:
x y : Fin 1
⊢ ¬x = y →
    (∏ x_1 ∈ finPairsLT 1,
        if
            (if x_1.fst = x then y else if x_1.fst = y then x else x_1.fst) ≤
              if x_1.snd = x then y else if x_1.snd = y then x else x_1.snd then
          -1
        else 1) =
      -1

Proof state:
x y : Fin 0
_hxy✝ : x ≠ y
⊢ (swap x y).signAux = -1

Tactic:
exact Fin.elim0 x

Result:
no goals

Proof state:
x y : Fin 1
⊢ ¬x = y →
    (∏ x_1 ∈ finPairsLT 1,
        if
            (if x_1.fst = x then y else if x_1.fst = y then x else x_1.fst) ≤
              if x_1.snd = x then y else if x_1.snd = y then x else x_1.snd then
          -1
        else 1) =
      -1

Tactic:
simp only [eq_iff_true_of_subsingleton, not_true, ite_true, le_refl, prod_const,
           IsEmpty.forall_iff]

Result:
no goals

Proof state:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ 2 ≤ n + 2

Tactic:
exact le_add_self

Result:
no goals

Proof state:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ IsConj (swap x y).signAux (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux

Tactic:
exact (MonoidHom.mk' signAux signAux_mul).map_isConj
  (isConj_swap hxy (by exact of_decide_eq_true rfl))

Result:
no goals

Proof state:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ ⟨0, ⋯⟩ ≠ ⟨1, ⋯⟩

Tactic:
exact of_decide_eq_true rfl

Result:
no goals

Proof state:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ (swap x y).signAux = -1

Tactic:
rw [← isConj_iff_eq, ← signAux_swap_zero_one h2n]

Result:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ IsConj (swap x y).signAux (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux

Proof state:
x y : Fin 0
⊢ x ≠ y → (swap x y).signAux = -1

Tactic:
intro

Result:
x y : Fin 0
_hxy✝ : x ≠ y
⊢ (swap x y).signAux = -1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_succ_left : range' (s + 1) n step = (range' s n step).map (· + 1)

Proof state:
s n step : Nat
⊢ range' (s + 1) n step = map (fun x => x + 1) (range' s n step)

Tactic:
apply ext_getElem

Result:
case hl
s n step : Nat
⊢ (range' (s + 1) n step).length = (map (fun x => x + 1) (range' s n step)).length

case h
s n step : Nat
⊢ ∀ (i : Nat) (h₁ : i < (range' (s + 1) n step).length) (h₂ : i < (map (fun x => x + 1) (range' s n step)).length),
    (range' (s + 1) n step)[i] = (map (fun x => x + 1) (range' s n step))[i]

Proof state:
case h
s n step : Nat
⊢ ∀ (i : Nat) (h₁ : i < (range' (s + 1) n step).length) (h₂ : i < (map (fun x => x + 1) (range' s n step)).length),
    (range' (s + 1) n step)[i] = (map (fun x => x + 1) (range' s n step))[i]

Tactic:
simp [Nat.add_right_comm]

Result:
no goals

Proof state:
case hl
s n step : Nat
⊢ (range' (s + 1) n step).length = (map (fun x => x + 1) (range' s n step)).length

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Holder.lean
@[simp]
lemma holderWith_zero_iff : HolderWith 0 r f ↔ ∀ x₁ x₂, f x₁ = f x₂

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : MetricSpace Y
r : ℝ≥0
f : X → Y
x₁ x₂ : X
h : edist (f x₁) (f x₂) ≤ ↑0 * edist x₁ x₂ ^ ↑r
⊢ f x₁ = f x₂

Tactic:
simp [ENNReal.coe_zero, zero_mul, nonpos_iff_eq_zero, edist_eq_zero] at h

Result:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : MetricSpace Y
r : ℝ≥0
f : X → Y
x₁ x₂ : X
h : f x₁ = f x₂
⊢ f x₁ = f x₂

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : MetricSpace Y
r : ℝ≥0
f : X → Y
h : HolderWith 0 r f
x₁ x₂ : X
⊢ f x₁ = f x₂

Tactic:
specialize h x₁ x₂

Result:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : MetricSpace Y
r : ℝ≥0
f : X → Y
x₁ x₂ : X
h : edist (f x₁) (f x₂) ≤ ↑0 * edist x₁ x₂ ^ ↑r
⊢ f x₁ = f x₂

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : MetricSpace Y
r : ℝ≥0
f : X → Y
⊢ HolderWith 0 r f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
refine ⟨fun h x₁ x₂ => ?_, fun h x₁ x₂ => h x₁ x₂ ▸ ?_⟩

Result:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : MetricSpace Y
r : ℝ≥0
f : X → Y
h : HolderWith 0 r f
x₁ x₂ : X
⊢ f x₁ = f x₂

case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : MetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
x₁ x₂ : X
⊢ edist (f x₁) (f x₁) ≤ ↑0 * edist x₁ x₂ ^ ↑r

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : MetricSpace Y
r : ℝ≥0
f : X → Y
x₁ x₂ : X
h : f x₁ = f x₂
⊢ f x₁ = f x₂

Tactic:
assumption

Result:
no goals

Proof state:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : MetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
x₁ x₂ : X
⊢ edist (f x₁) (f x₁) ≤ ↑0 * edist x₁ x₂ ^ ↑r

Tactic:
simp only [edist_self, ENNReal.coe_zero, zero_mul, le_refl]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem fromBlocks_eq_of_invertible₂₂ (A : Matrix l m α) (B : Matrix l n α) (C : Matrix n m α)
    (D : Matrix n n α) [Invertible D] :
    fromBlocks A B C D =
      fromBlocks 1 (B * ⅟ D) 0 1 * fromBlocks (A - B * ⅟ D * C) 0 0 D *
        fromBlocks 1 0 (⅟ D * C) 1 :=
  (Matrix.reindex (Equiv.sumComm _ _) (Equiv.sumComm _ _)).injective <| by
    simpa [reindex_apply, Equiv.sumComm_symm, ← submatrix_mul_equiv _ _ _ (Equiv.sumComm n m), ←
      submatrix_mul_equiv _ _ _ (Equiv.sumComm n l), Equiv.sumComm_apply,
      fromBlocks_submatrix_sum_swap_sum_swap] using fromBlocks_eq_of_invertible₁₁ D C B A

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix l m α
B : Matrix l n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ (reindex (Equiv.sumComm l n) (Equiv.sumComm m n)) (fromBlocks A B C D) =
    (reindex (Equiv.sumComm l n) (Equiv.sumComm m n))
      (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)

Tactic:
simpa [reindex_apply, Equiv.sumComm_symm, ← submatrix_mul_equiv _ _ _ (Equiv.sumComm n m), ←
  submatrix_mul_equiv _ _ _ (Equiv.sumComm n l), Equiv.sumComm_apply,
  fromBlocks_submatrix_sum_swap_sum_swap] using fromBlocks_eq_of_invertible₁₁ D C B A

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem pure_seq_eq_map (g : α → β) (f : Filter α) : seq (pure g) f = f.map g

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
a : α
ha : a ∈ t
⊢ g a ∈ s.seq t

Tactic:
exact ⟨g, hs, a, ha, rfl⟩

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ {g}.seq s ∈ (pure g).seq f

Tactic:
apply seq_mem_seq _ hs

Result:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ {g} ∈ pure g

Proof state:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ {g} ∈ pure g

Tactic:
exact singleton_mem_pure

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
⊢ (pure g).seq f = map g f

Tactic:
refine le_antisymm (le_map fun s hs => ?_) (le_seq fun s hs t ht => ?_)

Result:
case refine_1
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ g '' s ∈ (pure g).seq f

case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ map g f

Proof state:
case refine_1
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ g '' s ∈ (pure g).seq f

Tactic:
rw [← singleton_seq]

Result:
case refine_1
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ {g}.seq s ∈ (pure g).seq f

Proof state:
case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ g '' t ⊆ s.seq t

Tactic:
rintro b ⟨a, ha, rfl⟩

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
a : α
ha : a ∈ t
⊢ g a ∈ s.seq t

Proof state:
case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ map g f

Tactic:
refine sets_of_superset (map g f) (image_mem_map ht) ?_

Result:
case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ g '' t ⊆ s.seq t
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem natDegree_trunc_lt (f : R⟦X⟧) (n) : (trunc (n + 1) f).natDegree < n + 1

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n N✝ : ℕ
a✝ : n < N✝
h : ¬n < N✝
⊢ (coeff R N✝) f = 0

Tactic:
contradiction

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∀ (N : ℕ), n < N → (trunc (n + 1) f).coeff N = 0

Tactic:
intros

Result:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n N✝ : ℕ
a✝ : n < N✝
⊢ (trunc (n + 1) f).coeff N✝ = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n N✝ : ℕ
a✝ : n < N✝
⊢ (if N✝ < n + 1 then (coeff R N✝) f else 0) = 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n N✝ : ℕ
a✝ : n < N✝
h : N✝ < n + 1
⊢ (coeff R N✝) f = 0

case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n N✝ : ℕ
a✝ : n < N✝
h : ¬N✝ < n + 1
⊢ 0 = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ (trunc (n + 1) f).natDegree < n + 1

Tactic:
rw [Nat.lt_succ_iff, natDegree_le_iff_coeff_eq_zero]

Result:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∀ (N : ℕ), n < N → (trunc (n + 1) f).coeff N = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n N✝ : ℕ
a✝ : n < N✝
h : ¬N✝ < n + 1
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n N✝ : ℕ
a✝ : n < N✝
h : N✝ < n + 1
⊢ (coeff R N✝) f = 0

Tactic:
rw [lt_succ, ← not_lt] at h

Result:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n N✝ : ℕ
a✝ : n < N✝
h : ¬n < N✝
⊢ (coeff R N✝) f = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n N✝ : ℕ
a✝ : n < N✝
⊢ (trunc (n + 1) f).coeff N✝ = 0

Tactic:
rw [coeff_trunc]

Result:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n N✝ : ℕ
a✝ : n < N✝
⊢ (if N✝ < n + 1 then (coeff R N✝) f else 0) = 0
-- Mathlib/Analysis/Meromorphic/Basic.lean
lemma congr (h_eq : Set.EqOn f g U) (hu : IsOpen U) : MeromorphicOn g U

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h_eq : Set.EqOn f g U
hu : IsOpen U
x : 𝕜
hx : x ∈ U
⊢ f =ᶠ[𝓝 x] g

Tactic:
exact eventually_of_mem (hu.mem_nhds hx) h_eq

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h_eq : Set.EqOn f g U
hu : IsOpen U
⊢ MeromorphicOn g U

Tactic:
refine fun x hx ↦ (hf x hx).congr (EventuallyEq.filter_mono ?_ nhdsWithin_le_nhds)

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h_eq : Set.EqOn f g U
hu : IsOpen U
x : 𝕜
hx : x ∈ U
⊢ f =ᶠ[𝓝 x] g