harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
/-- The trivial case if `X` is initial. -/
private lemma has_decomp_connected_components_aux_initial (X : C) (h : IsInitial X) :
    ∃ (ι : Type) (f : ι → C) (g : (i : ι) → (f i) ⟶ X) (_ : IsColimit (Cofan.mk X g)),
    (∀ i, IsConnected (f i)) ∧ Finite ι

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
h : IsInitial X
⊢ ∃ x, (∀ (i : Empty), IsConnected ((fun x => X) i)) ∧ Finite Empty

Tactic:
use mkCofanColimit _ (fun s ↦ IsInitial.to h s.pt) (fun s ↦ by simp)
  (fun s m _ ↦ IsInitial.hom_ext h m _)

Result:
case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
h : IsInitial X
⊢ (∀ (i : Empty), IsConnected ((fun x => X) i)) ∧ Finite Empty

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
h : IsInitial X
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
refine ⟨Empty, fun _ ↦ X, fun _ ↦ 𝟙 X, ?_⟩

Result:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
h : IsInitial X
⊢ ∃ x, (∀ (i : Empty), IsConnected ((fun x => X) i)) ∧ Finite Empty

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
h : IsInitial X
s : Cofan fun x => X
⊢ ∀ (j : Empty), (Cofan.mk X fun x => 𝟙 X).inj j ≫ (fun s => h.to s.pt) s = s.inj j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
h : IsInitial X
⊢ ∀ (i : Empty), IsConnected ((fun x => X) i)

Tactic:
simp only [IsEmpty.forall_iff]

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
h : IsInitial X
⊢ (∀ (i : Empty), IsConnected ((fun x => X) i)) ∧ Finite Empty

Tactic:
exact ⟨by simp only [IsEmpty.forall_iff], inferInstance⟩

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_sup_self' : y \ x ⊔ x = y ⊔ x :=
  calc
    y \ x ⊔ x = y \ x ⊔ (x ⊔ x ⊓ y)

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊔ y \ x ⊔ x = y ⊔ x

Tactic:
rw [sup_inf_sdiff]

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊔ (x ⊔ x ⊓ y) = y ⊓ x ⊔ y \ x ⊔ x

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊔ x = y \ x ⊔ (x ⊔ x ⊓ y)

Tactic:
rw [sup_inf_self]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem signAux_swap_zero_one' (n : ℕ) : signAux (swap (0 : Fin (n + 2)) 1) = -1 :=
  show _ = ∏ x ∈ {(⟨1, 0⟩ : Σ _ : Fin (n + 2), Fin (n + 2))},
      if (Equiv.swap 0 1) x.1 ≤ swap 0 1 x.2 then (-1 : ℤˣ) else 1 by
    refine Eq.symm (prod_subset (fun ⟨x₁, x₂⟩ => by
      simp +contextual [mem_finPairsLT, Fin.one_pos]) fun a ha₁ ha₂ => ?_)
    rcases a with ⟨a₁, a₂⟩
    replace ha₁ : a₂ < a₁ := mem_finPairsLT.1 ha₁
    dsimp only
    rcases a₁.zero_le.eq_or_lt with (rfl | H)
    · exact absurd a₂.zero_le ha₁.not_le
    rcases a₂.zero_le.eq_or_lt with (rfl | H')
    · simp only [and_true, eq_self_iff_true, heq_iff_eq, mem_singleton, Sigma.mk.inj_iff] at ha₂
      have : 1 < a₁ := lt_of_le_of_ne (Nat.succ_le_of_lt ha₁)
        (Ne.symm (by intro h; apply ha₂; simp [h]))
      have h01 : Equiv.swap (0 : Fin (n + 2)) 1 0 = 1

Proof state:
case mk.inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
have h01 : Equiv.swap (0 : Fin (n + 2)) 1 1 = 0 := by simp only [swap_apply_right]

Result:
case mk.inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : (swap 0 1) 1 = 0
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Proof state:
n : ℕ
⊢ (swap 0 1).signAux = ∏ x ∈ {⟨1, 0⟩}, if (swap 0 1) x.fst ≤ (swap 0 1) x.snd then -1 else 1

Tactic:
refine Eq.symm (prod_subset (fun ⟨x₁, x₂⟩ => by
  simp +contextual [mem_finPairsLT, Fin.one_pos]) fun a ha₁ ha₂ => ?_)

Result:
n : ℕ
a : (_ : Fin (n + 2)) × Fin (n + 2)
ha₁ : a ∈ finPairsLT (n + 2)
ha₂ : a ∉ {⟨1, 0⟩}
⊢ (if (swap 0 1) a.fst ≤ (swap 0 1) a.snd then -1 else 1) = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reverse_append (as bs : Array α) : (as ++ bs).reverse = bs.reverse ++ as.reverse

Proof state:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ }).reverse =
    { toList := toList✝ }.reverse ++ { toList := toList✝¹ }.reverse

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
bs : Array α
toList✝ : List α
⊢ ({ toList := toList✝ } ++ bs).reverse = bs.reverse ++ { toList := toList✝ }.reverse

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ }).reverse =
    { toList := toList✝ }.reverse ++ { toList := toList✝¹ }.reverse

Proof state:
α : Type u_1
as bs : Array α
⊢ (as ++ bs).reverse = bs.reverse ++ as.reverse

Tactic:
cases as

Result:
case mk
α : Type u_1
bs : Array α
toList✝ : List α
⊢ ({ toList := toList✝ } ++ bs).reverse = bs.reverse ++ { toList := toList✝ }.reverse
-- Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
theorem finiteDimensional (f : K[X]) [IsSplittingField K L f] : FiniteDimensional K L

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
y : L
hy : y ∈ f.rootSet L
hf : f = 0
⊢ IsIntegral K y

Tactic:
rw [hf, rootSet_zero] at hy

Result:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
y : L
hy : y ∈ ∅
hf : f = 0
⊢ IsIntegral K y

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
⊢ FiniteDimensional K L

Tactic:
exact ⟨@Algebra.top_toSubmodule K L _ _ _ ▸
  adjoin_rootSet L f ▸ fg_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦
    if hf : f = 0 then by rw [hf, rootSet_zero] at hy; cases hy
    else IsAlgebraic.isIntegral ⟨f, hf, (mem_rootSet'.mp hy).2⟩⟩

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
y : L
hy : y ∈ ∅
hf : f = 0
⊢ IsIntegral K y

Tactic:
cases hy

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
⊢ FiniteDimensional K L

Tactic:
classical
exact ⟨@Algebra.top_toSubmodule K L _ _ _ ▸
  adjoin_rootSet L f ▸ fg_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦
    if hf : f = 0 then by rw [hf, rootSet_zero] at hy; cases hy
    else IsAlgebraic.isIntegral ⟨f, hf, (mem_rootSet'.mp hy).2⟩⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem dist_eq_norm_div' (a b : E) : dist a b = ‖b / a‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ dist a b = ‖b / a‖

Tactic:
rw [dist_comm, dist_eq_norm_div]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem IsPrime.multiset_prod_le {s : Multiset (Ideal R)} {P : Ideal R} (hp : IsPrime P) :
    s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P :=
  s.induction_on (by simp [hp.ne_top]) fun I s ih ↦ by simp [hp.mul_le, ih]

Proof state:
R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
P : Ideal R
hp : P.IsPrime
I : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P
⊢ (I ::ₘ s).prod ≤ P ↔ ∃ I_1 ∈ I ::ₘ s, I_1 ≤ P

Tactic:
simp [hp.mul_le, ih]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
P : Ideal R
hp : P.IsPrime
⊢ Multiset.prod 0 ≤ P ↔ ∃ I ∈ 0, I ≤ P

Tactic:
simp [hp.ne_top]

Result:
no goals
-- Mathlib/Algebra/Order/Pi.lean
@[to_additive (attr := simp)]
lemma mulSingle_le_one : mulSingle i a ≤ 1 ↔ a ≤ 1

Proof state:
ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ mulSingle i a ≤ 1 ↔ a ≤ 1

Tactic:
simp [mulSingle]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_univ : ContDiffOn 𝕜 n f univ ↔ ContDiff 𝕜 n f

Proof state:
case mpr.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo ω f p
h'p : ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x => p x i) univ
x : E
a✝ : x ∈ univ
⊢ ContDiffWithinAt 𝕜 ω f univ x

Tactic:
exact ⟨univ, Filter.univ_sets _, p, (hp.hasFTaylorSeriesUpToOn univ).of_le le_top,
  fun i ↦ (h'p i).analyticOn⟩

Result:
no goals

Proof state:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
H : ContDiffOn 𝕜 ω f univ
⊢ HasFTaylorSeriesUpTo ω f (ftaylorSeriesWithin 𝕜 f univ) ∧
    ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x => ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff]

Result:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
H : ContDiffOn 𝕜 ω f univ
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f univ) univ ∧
    ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x => ftaylorSeriesWithin 𝕜 f univ x i) univ

Proof state:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
H : ContDiffOn 𝕜 ω f univ
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f univ) univ ∧
    ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x => ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
refine ⟨H.ftaylorSeriesWithin uniqueDiffOn_univ, fun i ↦ ?_⟩

Result:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
H : ContDiffOn 𝕜 ω f univ
i : ℕ
⊢ AnalyticOnNhd 𝕜 (fun x => ftaylorSeriesWithin 𝕜 f univ x i) univ

Proof state:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
H : ContDiffOn 𝕜 ω f univ
⊢ ContDiff 𝕜 ω f

Tactic:
use ftaylorSeriesWithin 𝕜 f univ

Result:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
H : ContDiffOn 𝕜 ω f univ
⊢ HasFTaylorSeriesUpTo ω f (ftaylorSeriesWithin 𝕜 f univ) ∧
    ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x => ftaylorSeriesWithin 𝕜 f univ x i) univ
-- Mathlib/Analysis/Calculus/FDeriv/Comp.lean
theorem fderivWithin_fderivWithin {g : F → G} {f : E → F} {x : E} {y : F} {s : Set E} {t : Set F}
    (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t)
    (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) (v : E) :
    fderivWithin 𝕜 g t y (fderivWithin 𝕜 f s x v) = fderivWithin 𝕜 (g ∘ f) s x v

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ (fderivWithin 𝕜 g t (f x)) ((fderivWithin 𝕜 f s x) v) = (fderivWithin 𝕜 (g ∘ f) s x) v

Tactic:
rw [fderivWithin_comp x hg hf h hxs, coe_comp', Function.comp_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
y : F
s : Set E
t : Set F
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hy : f x = y
v : E
⊢ (fderivWithin 𝕜 g t y) ((fderivWithin 𝕜 f s x) v) = (fderivWithin 𝕜 (g ∘ f) s x) v

Tactic:
subst y

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ (fderivWithin 𝕜 g t (f x)) ((fderivWithin 𝕜 f s x) v) = (fderivWithin 𝕜 (g ∘ f) s x) v
-- Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean
theorem rank_dual_eq_card_dual_of_aleph0_le_rank' {V : Type*} [AddCommGroup V] [Module K V]
    (h : ℵ₀ ≤ Module.rank K V) : Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Proof state:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] ι → Kᵐᵒᵖ
⊢ Module.rank Kᵐᵒᵖ (ι → Kᵐᵒᵖ) = #(ι → Kᵐᵒᵖ)

Tactic:
apply rank_fun_infinite

Result:
no goals

Proof state:
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)

Result:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type u_1
b : Basis ι K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Proof state:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] ι → Kᵐᵒᵖ
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
rw [e.rank_eq, e.toEquiv.cardinal_eq]

Result:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] ι → Kᵐᵒᵖ
⊢ Module.rank Kᵐᵒᵖ (ι → Kᵐᵒᵖ) = #(ι → Kᵐᵒᵖ)

Proof state:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type u_1
b : Basis ι K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
rw [← b.mk_eq_rank'', aleph0_le_mk_iff] at h

Result:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Basis ι K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Proof state:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Basis ι K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
have e := (b.constr Kᵐᵒᵖ (M' := K)).symm.trans
  (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Kᵐᵒᵖ)

Result:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] ι → Kᵐᵒᵖ
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma orthogonal_cross_right {v w : ℙ F (Fin 3 → F)} (h : v ≠ w) :
    w.orthogonal (cross v w)

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ w.orthogonal (v.cross w)

Tactic:
rw [orthogonal_comm]

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal w

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal w

Tactic:
exact cross_orthogonal_right h

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_neg_left : (fun x => -f' x) =o[l] g ↔ f' =o[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => -f' x) g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g

Tactic:
exact forall₂_congr fun _ _ => isBigOWith_neg_left

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x => -f' x) =o[l] g ↔ f' =o[l] g

Tactic:
simp only [IsLittleO_def]

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => -f' x) g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g
-- Mathlib/Analysis/RCLike/Basic.lean
/-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℝ` and `ℂ` are star ordered rings.
(That is, a star ring in which the nonnegative elements are those of the form `star z * z`.)

Note this is only an instance with `open scoped ComplexOrder`. -/
lemma toStarOrderedRing : StarOrderedRing K :=
  StarOrderedRing.of_nonneg_iff'
    (h_add := fun {x y} hxy z => by
      rw [RCLike.le_iff_re_im] at *
      simpa [map_add, add_le_add_iff_left, add_right_inj] using hxy)
    (h_nonneg_iff := fun x => by
      rw [nonneg_iff]
      refine ⟨fun h ↦ ⟨√(re x), by simp [ext_iff (K := K), h.1, h.2]⟩, ?_⟩
      rintro ⟨s, rfl⟩
      simp [mul_comm, mul_self_nonneg, add_nonneg])

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ (∃ s, x = star s * s) → 0 ≤ re x ∧ im x = 0

Tactic:
rintro ⟨s, rfl⟩

Result:
case intro
K : Type u_1
inst✝ : RCLike K
s : K
⊢ 0 ≤ re (star s * s) ∧ im (star s * s) = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ 0 ≤ x ↔ ∃ s, x = star s * s

Tactic:
rw [nonneg_iff]

Result:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ 0 ≤ re x ∧ im x = 0 ↔ ∃ s, x = star s * s

Proof state:
K : Type u_1
inst✝ : RCLike K
x y : K
hxy : x ≤ y
z : K
⊢ z + x ≤ z + y

Tactic:
rw [RCLike.le_iff_re_im] at *

Result:
K : Type u_1
inst✝ : RCLike K
x y : K
hxy : re x ≤ re y ∧ im x = im y
z : K
⊢ re (z + x) ≤ re (z + y) ∧ im (z + x) = im (z + y)

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ 0 ≤ re x ∧ im x = 0 ↔ ∃ s, x = star s * s

Tactic:
refine ⟨fun h ↦ ⟨√(re x), by simp [ext_iff (K := K), h.1, h.2]⟩, ?_⟩

Result:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ (∃ s, x = star s * s) → 0 ≤ re x ∧ im x = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
h : 0 ≤ re x ∧ im x = 0
⊢ x = star ↑√(re x) * ↑√(re x)

Tactic:
simp [ext_iff (K := K), h.1, h.2]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
x y : K
hxy : re x ≤ re y ∧ im x = im y
z : K
⊢ re (z + x) ≤ re (z + y) ∧ im (z + x) = im (z + y)

Tactic:
simpa [map_add, add_le_add_iff_left, add_right_inj] using hxy

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝ : RCLike K
s : K
⊢ 0 ≤ re (star s * s) ∧ im (star s * s) = 0

Tactic:
simp [mul_comm, mul_self_nonneg, add_nonneg]

Result:
no goals
-- Mathlib/Topology/Irreducible.lean
theorem IsPreirreducible.preimage (ht : IsPreirreducible t) {f : Y → X}
    (hf : IsOpenEmbedding f) : IsPreirreducible (f ⁻¹' t)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsPreirreducible t
f : Y → X
hf : IsOpenEmbedding f
⊢ IsPreirreducible (f ⁻¹' t)

Tactic:
rintro U V hU hV ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩

Result:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsPreirreducible t
f : Y → X
hf : IsOpenEmbedding f
U V : Set Y
hU : IsOpen U
hV : IsOpen V
x : Y
hx : x ∈ f ⁻¹' t
hx' : x ∈ U
y : Y
hy : y ∈ f ⁻¹' t
hy' : y ∈ V
⊢ (f ⁻¹' t ∩ (U ∩ V)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsPreirreducible t
f : Y → X
hf : IsOpenEmbedding f
U V : Set Y
hU : IsOpen U
hV : IsOpen V
x : Y
hx : x ∈ f ⁻¹' t
hx' : x ∈ U
y✝ : Y
hy : y✝ ∈ f ⁻¹' t
hy' : y✝ ∈ V
y : Y
h₂ : y ∈ U
h₁ : f y ∈ t
h₃ : y ∈ V
h₄ : f y = f y
⊢ (f ⁻¹' t ∩ (U ∩ V)).Nonempty

Tactic:
exact ⟨y, h₁, h₂, h₃⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsPreirreducible t
f : Y → X
hf : IsOpenEmbedding f
U V : Set Y
hU : IsOpen U
hV : IsOpen V
x : Y
hx : x ∈ f ⁻¹' t
hx' : x ∈ U
y : Y
hy : y ∈ f ⁻¹' t
hy' : y ∈ V
⊢ (f ⁻¹' t ∩ (U ∩ V)).Nonempty

Tactic:
obtain ⟨_, h₁, ⟨y, h₂, rfl⟩, ⟨y', h₃, h₄⟩⟩ :=
  ht _ _ (hf.isOpenMap _ hU) (hf.isOpenMap _ hV) ⟨f x, hx, Set.mem_image_of_mem f hx'⟩
    ⟨f y, hy, Set.mem_image_of_mem f hy'⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsPreirreducible t
f : Y → X
hf : IsOpenEmbedding f
U V : Set Y
hU : IsOpen U
hV : IsOpen V
x : Y
hx : x ∈ f ⁻¹' t
hx' : x ∈ U
y✝ : Y
hy : y✝ ∈ f ⁻¹' t
hy' : y✝ ∈ V
y : Y
h₂ : y ∈ U
h₁ : f y ∈ t
y' : Y
h₃ : y' ∈ V
h₄ : f y' = f y
⊢ (f ⁻¹' t ∩ (U ∩ V)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsPreirreducible t
f : Y → X
hf : IsOpenEmbedding f
U V : Set Y
hU : IsOpen U
hV : IsOpen V
x : Y
hx : x ∈ f ⁻¹' t
hx' : x ∈ U
y✝ : Y
hy : y✝ ∈ f ⁻¹' t
hy' : y✝ ∈ V
y : Y
h₂ : y ∈ U
h₁ : f y ∈ t
y' : Y
h₃ : y' ∈ V
h₄ : f y' = f y
⊢ (f ⁻¹' t ∩ (U ∩ V)).Nonempty

Tactic:
cases hf.injective h₄

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : IsPreirreducible t
f : Y → X
hf : IsOpenEmbedding f
U V : Set Y
hU : IsOpen U
hV : IsOpen V
x : Y
hx : x ∈ f ⁻¹' t
hx' : x ∈ U
y✝ : Y
hy : y✝ ∈ f ⁻¹' t
hy' : y✝ ∈ V
y : Y
h₂ : y ∈ U
h₁ : f y ∈ t
h₃ : y ∈ V
h₄ : f y = f y
⊢ (f ⁻¹' t ∩ (U ∩ V)).Nonempty
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma conductor_one_dvd (n : ℕ) : conductor (1 : DirichletCharacter R 1) ∣ n

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
⊢ 1 ∣ n

Tactic:
apply one_dvd _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
⊢ conductor 1 ∣ n

Tactic:
rw [(isPrimitive_def _).mp isPrimitive_one_level_one]

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
⊢ 1 ∣ n
-- Mathlib/Topology/UniformSpace/Pi.lean
lemma Cauchy.pi [Nonempty ι] {l : ∀ i, Filter (α i)} (hl : ∀ i, Cauchy (l i)) :
    Cauchy (Filter.pi l)

Proof state:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : (i : ι) → Filter (α i)
hl : ∀ (i : ι), Cauchy (l i)
⊢ Cauchy (Filter.pi l)

Tactic:
have := fun i ↦ (hl i).1

Result:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : (i : ι) → Filter (α i)
hl : ∀ (i : ι), Cauchy (l i)
this : ∀ (i : ι), (l i).NeBot
⊢ Cauchy (Filter.pi l)

Proof state:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : (i : ι) → Filter (α i)
hl : ∀ (i : ι), Cauchy (l i)
this : ∀ (i : ι), (l i).NeBot
⊢ Cauchy (Filter.pi l)

Tactic:
simpa [cauchy_pi_iff]

Result:
no goals