harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/W/Basic.lean
theorem infinite_of_nonempty_of_isEmpty (a b : α) [ha : Nonempty (β a)] [he : IsEmpty (β b)] :
    Infinite (WType β) :=
  ⟨by
    intro hf
    have hba : b ≠ a := fun h => ha.elim (IsEmpty.elim' (show IsEmpty (β a) from h ▸ he))
    refine
      not_injective_infinite_finite
        (fun n : ℕ =>
          show WType β from Nat.recOn n ⟨b, IsEmpty.elim' he⟩ fun _ ih => ⟨a, fun _ => ih⟩)
        ?_
    intro n m h
    induction' n with n ih generalizing m
    · rcases m with - | m <;> simp_all
    · rcases m with - | m
      · simp_all
      · refine congr_arg Nat.succ (ih ?_)
        simp_all [funext_iff]⟩

Proof state:
case succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (n + 1) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      m
⊢ n + 1 = m

Tactic:
rcases m with - | m

Result:
case succ.zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (n + 1) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      0
⊢ n + 1 = 0

case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (n + 1) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih;
        this)
      (m + 1)
⊢ n + 1 = m + 1
-- Mathlib/CategoryTheory/Simple.lean
theorem simple_iff_subobject_isSimpleOrder (X : C) : Simple X ↔ IsSimpleOrder (Subobject X) :=
  ⟨by
    intro h
    infer_instance, by
    intro h
    exact simple_of_isSimpleOrder_subobject X⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : IsSimpleOrder (Subobject X)
⊢ Simple X

Tactic:
exact simple_of_isSimpleOrder_subobject X

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
⊢ Simple X → IsSimpleOrder (Subobject X)

Tactic:
intro h

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : Simple X
⊢ IsSimpleOrder (Subobject X)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : Simple X
⊢ IsSimpleOrder (Subobject X)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
⊢ IsSimpleOrder (Subobject X) → Simple X

Tactic:
intro h

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : IsSimpleOrder (Subobject X)
⊢ Simple X
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_insertMany_list [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
    {m : Raw₀ α β} {l : List ((a : α) × (β a))} (h : Raw.WFImp m.1) :
    Perm (toListModel (insertMany m l).1.1.buckets)
      (List.insertList (toListModel m.1.buckets) l)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
l : List ((a : α) × β a)
h : Raw.WFImp m.val
⊢ toListModel (m.insertMany l).val.val.buckets ~ insertList (toListModel m.val.buckets) l

Tactic:
rw [insertMany_eq_insertListₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
l : List ((a : α) × β a)
h : Raw.WFImp m.val
⊢ toListModel (m.insertListₘ l).val.buckets ~ insertList (toListModel m.val.buckets) l

Proof state:
case h
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
l : List ((a : α) × β a)
h : Raw.WFImp m.val
⊢ Raw.WFImp m.val

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
l : List ((a : α) × β a)
h : Raw.WFImp m.val
⊢ toListModel (m.insertListₘ l).val.buckets ~ insertList (toListModel m.val.buckets) l

Tactic:
apply toListModel_insertListₘ

Result:
case h
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
l : List ((a : α) × β a)
h : Raw.WFImp m.val
⊢ Raw.WFImp m.val
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mapRange_injective (f : ∀ i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) :
    Function.Injective (mapRange f hf) ↔ ∀ i, Function.Injective (f i) :=
  ⟨fun h i x y eq ↦ single_injective (@h (single i x) (single i y) <| by
    simpa using congr_arg _ eq), fun h _ _ eq ↦ DFinsupp.ext fun i ↦ h i congr($eq i)⟩

Proof state:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : Function.Injective (mapRange f hf)
i : ι
x y : β₁ i
eq : f i x = f i y
⊢ mapRange f hf (single i x) = mapRange f hf (single i y)

Tactic:
simpa using congr_arg _ eq

Result:
no goals
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Fix.mk_dest (x : Fix F) : Fix.mk (Fix.dest x) = x

Proof state:
case h
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ mk <$> rec (Functor.map mk) <$> x = x → mk (mk <$> rec (Functor.map mk) <$> x) = mk x

Tactic:
intro h

Result:
case h
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
h : mk <$> rec (Functor.map mk) <$> x = x
⊢ mk (mk <$> rec (Functor.map mk) <$> x) = mk x

Proof state:
F : Type u → Type u
q : QPF F
x : Fix F
⊢ mk x.dest = x

Tactic:
change (Fix.mk ∘ Fix.dest) x = id x

Result:
F : Type u → Type u
q : QPF F
x : Fix F
⊢ (mk ∘ dest) x = id x

Proof state:
case h
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
h : mk <$> rec (Functor.map mk) <$> x = x
⊢ mk (mk <$> rec (Functor.map mk) <$> x) = mk x

Tactic:
rw [h]

Result:
no goals

Proof state:
case h
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)

Tactic:
rw [Function.comp_apply, id_eq, Fix.dest, Fix.rec_eq, id_map, comp_map]

Result:
case h
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ mk <$> rec (Functor.map mk) <$> x = x → mk (mk <$> rec (Functor.map mk) <$> x) = mk x

Proof state:
F : Type u → Type u
q : QPF F
x : Fix F
⊢ (mk ∘ dest) x = id x

Tactic:
apply Fix.ind_rec (mk ∘ dest) id

Result:
case h
F : Type u → Type u
q : QPF F
x : Fix F
⊢ ∀ (x : F (Fix F)), (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)

Proof state:
case h
F : Type u → Type u
q : QPF F
x : Fix F
⊢ ∀ (x : F (Fix F)), (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)

Tactic:
intro x

Result:
case h
F : Type u → Type u
q : QPF F
x✝ : Fix F
x : F (Fix F)
⊢ (mk ∘ dest) <$> x = id <$> x → (mk ∘ dest) (mk x) = id (mk x)
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffWithinAt_iff :
    ContMDiffWithinAt I I' n f s x ↔
      ContinuousWithinAt f s x ∧
        ContDiffWithinAt 𝕜 n (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm)
          ((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
⊢ ContMDiffWithinAt I I' n f s x ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
simp_rw [ContMDiffWithinAt, liftPropWithinAt_iff']

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
n : WithTop ℕ∞
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    ContinuousWithinAt f s x ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
-- Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean
theorem with_gaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily 𝕜 E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
⊢ WithSeminorms (gaugeSeminormFamily 𝕜 E)

Tactic:
refine SeminormFamily.withSeminorms_of_hasBasis _ ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
⊢ (𝓝 0).HasBasis (fun s => s ∈ (gaugeSeminormFamily 𝕜 E).basisSets) id
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
theorem IsMatching.even_card [Fintype M.verts] (h : M.IsMatching) : Even M.verts.toFinset.card

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : M.IsMatching
⊢ Even M.verts.toFinset.card

Tactic:
classical
rw [isMatching_iff_forall_degree] at h
use M.coe.edgeFinset.card
rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
convert_to _ = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v using 3
simp [h, Finset.card_univ]

Result:
no goals

Proof state:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = M.coe.edgeFinset.card + M.coe.edgeFinset.card

Tactic:
rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]

Result:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = ∑ v : ↑M.verts, M.coe.degree v

Proof state:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = ∑ v : ↑M.verts, M.coe.degree v

Tactic:
convert_to _ = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v using 3

Result:
case h.convert_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = ∑ v : ↑M.verts, M.coe.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ Even M.verts.toFinset.card

Tactic:
use M.coe.edgeFinset.card

Result:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = M.coe.edgeFinset.card + M.coe.edgeFinset.card

Proof state:
case h.convert_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = ∑ v : ↑M.verts, M.coe.degree v

Tactic:
simp [h, Finset.card_univ]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : M.IsMatching
⊢ Even M.verts.toFinset.card

Tactic:
rw [isMatching_iff_forall_degree] at h

Result:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ Even M.verts.toFinset.card
-- Mathlib/Combinatorics/Colex.lean
/-- `s ≤ {a}` in colex iff all elements of `s` are strictly less than `a`, except possibly `a` in
which case `s = {a}`. -/
lemma toColex_le_singleton : toColex s ≤ toColex {a} ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ { ofColex := s } ≤ { ofColex := {a} } ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)

Tactic:
simp only [toColex_le_toColex, mem_singleton, and_assoc, exists_eq_left]

Result:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 = a → a ∉ s ∧ a_1 ≤ a) ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 = a → a ∉ s ∧ a_1 ≤ a) ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)

Tactic:
refine forall₂_congr fun b _ ↦ ?_

Result:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
x✝ : b ∈ s
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
x✝ : b ∈ s
⊢ ¬b = a → a ∉ s ∧ b ≤ a ↔ b ≤ a ∧ (a ∈ s → b = a)

Tactic:
obtain rfl | hba := eq_or_ne b a <;> aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attachWith_ne_empty_iff {l : Array α} {P : α → Prop} {H : ∀ a ∈ l, P a} :
    l.attachWith P H ≠ #[] ↔ l ≠ #[]

Proof state:
case mk
α : Type u_1
P : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ { toList := toList✝ }.attachWith P H ≠ #[] ↔ { toList := toList✝ } ≠ #[]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : Array α
P : α → Prop
H : ∀ (a : α), a ∈ l → P a
⊢ l.attachWith P H ≠ #[] ↔ l ≠ #[]

Tactic:
cases l

Result:
case mk
α : Type u_1
P : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ { toList := toList✝ }.attachWith P H ≠ #[] ↔ { toList := toList✝ } ≠ #[]
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem conjTranspose_zpow [StarRing R] (A : M) : ∀ n : ℤ, (A ^ n)ᴴ = Aᴴ ^ n
  | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, conjTranspose_pow]
  | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]

Proof state:
n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ -[n+1])ᴴ = Aᴴ ^ -[n+1]

Tactic:
rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]

Result:
no goals

Proof state:
n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ ↑n)ᴴ = Aᴴ ^ ↑n

Tactic:
rw [zpow_natCast, zpow_natCast, conjTranspose_pow]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
lemma emb_injective : Injective (fun (p : Σ m, Fin (c.partSize m)) ↦ c.emb p.1 p.2)

Proof state:
case mk.mk
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
⊢ ⟨m, r⟩ = ⟨m', r'⟩

Tactic:
have : m = m' := by
  contrapose! h
  have A : Disjoint (range (c.emb m)) (range (c.emb m')) :=
    c.disjoint (mem_univ m) (mem_univ m') h
  apply disjoint_iff_forall_ne.1 A (mem_range_self r) (mem_range_self r')

Result:
case mk.mk
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
this : m = m'
⊢ ⟨m, r⟩ = ⟨m', r'⟩

Proof state:
case mk.mk
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
this : m = m'
⊢ ⟨m, r⟩ = ⟨m', r'⟩

Tactic:
subst this

Result:
case mk.mk
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r r' : Fin (c.partSize m)
h : c.emb m r = c.emb m r'
⊢ ⟨m, r⟩ = ⟨m, r'⟩

Proof state:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : m ≠ m'
A : Disjoint (range (c.emb m)) (range (c.emb m'))
⊢ c.emb m r ≠ c.emb m' r'

Tactic:
apply disjoint_iff_forall_ne.1 A (mem_range_self r) (mem_range_self r')

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition n
⊢ Injective fun p => c.emb p.fst p.snd

Tactic:
rintro ⟨m, r⟩ ⟨m', r'⟩ (h : c.emb m r = c.emb m' r')

Result:
case mk.mk
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
⊢ ⟨m, r⟩ = ⟨m', r'⟩

Proof state:
case mk.mk
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r r' : Fin (c.partSize m)
h : c.emb m r = c.emb m r'
⊢ ⟨m, r⟩ = ⟨m, r'⟩

Tactic:
simpa using (c.emb_strictMono m).injective h

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
⊢ m = m'

Tactic:
contrapose! h

Result:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : m ≠ m'
⊢ c.emb m r ≠ c.emb m' r'

Proof state:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : m ≠ m'
⊢ c.emb m r ≠ c.emb m' r'

Tactic:
have A : Disjoint (range (c.emb m)) (range (c.emb m')) :=
  c.disjoint (mem_univ m) (mem_univ m') h

Result:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : m ≠ m'
A : Disjoint (range (c.emb m)) (range (c.emb m'))
⊢ c.emb m r ≠ c.emb m' r'
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.op (h : S.Exact) : S.op.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
⊢ S.op.Exact

Tactic:
obtain ⟨h, z⟩ := h

Result:
case mk.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
z : IsZero h.left.H
⊢ S.op.Exact

Proof state:
case mk.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
z : IsZero h.left.H
⊢ S.op.Exact

Tactic:
exact ⟨⟨h.op, (IsZero.of_iso z h.iso.symm).op⟩⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_add_mul_self_real (x y : F) :
    ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Tactic:
simpa using h

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Tactic:
have h := @norm_add_mul_self ℝ _ _ _ _ x y

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
-- Mathlib/Topology/CompactOpen.lean
theorem Topology.IsQuotientMap.continuous_lift_prod_left (hf : IsQuotientMap f) {g : X × Y → Z}
    (hg : Continuous fun p : X₀ × Y => g (f p.1, p.2)) : Continuous g

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => { toFun := fun y => g (x, y), continuous_toFun := ⋯ }
⊢ Continuous g

Tactic:
have : Continuous G := by
  rw [hf.continuous_iff]
  exact Gf.continuous

Result:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => { toFun := fun y => g (x, y), continuous_toFun := ⋯ }
this : Continuous G
⊢ Continuous g