harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Products/Basic.lean
theorem isIso_prod_iff {P Q : C} {S T : D} {f : (P, S) ⟶ (Q, T)} :
    IsIso f ↔ IsIso f.1 ∧ IsIso f.2

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f.1 ∧ IsIso f.2 → IsIso f

Tactic:
rintro ⟨⟨g₁, hfg₁, hgf₁⟩, ⟨g₂, hfg₂, hgf₂⟩⟩

Result:
case mpr.intro.mk.intro.intro.mk.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).1 ⟶ (P, S).1
hfg₁ : f.1 ≫ g₁ = 𝟙 (P, S).1
hgf₁ : g₁ ≫ f.1 = 𝟙 (Q, T).1
g₂ : (Q, T).2 ⟶ (P, S).2
hfg₂ : f.2 ≫ g₂ = 𝟙 (P, S).2
hgf₂ : g₂ ≫ f.2 = 𝟙 (Q, T).2
⊢ IsIso f

Proof state:
case mp.mk.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hgf : g.1 ≫ f.1 = 𝟙 Q ∧ g.2 ≫ f.2 = 𝟙 T
hfg₁ : f.1 ≫ g.1 = 𝟙 P
hfg₂ : f.2 ≫ g.2 = 𝟙 S
⊢ IsIso f.1 ∧ IsIso f.2

Tactic:
rcases hgf with ⟨hgf₁, hgf₂⟩

Result:
case mp.mk.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg₁ : f.1 ≫ g.1 = 𝟙 P
hfg₂ : f.2 ≫ g.2 = 𝟙 S
hgf₁ : g.1 ≫ f.1 = 𝟙 Q
hgf₂ : g.2 ≫ f.2 = 𝟙 T
⊢ IsIso f.1 ∧ IsIso f.2

Proof state:
case mpr.intro.mk.intro.intro.mk.intro.intro.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).1 ⟶ (P, S).1
hfg₁ : f.1 ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.1 = 𝟙 Q
g₂ : (Q, T).2 ⟶ (P, S).2
hfg₂ : f.2 ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.2 = 𝟙 T
⊢ g₁ ≫ f.1 = 𝟙 Q ∧ g₂ ≫ f.2 = 𝟙 T

Tactic:
constructor

Result:
case mpr.intro.mk.intro.intro.mk.intro.intro.refine_2.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).1 ⟶ (P, S).1
hfg₁ : f.1 ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.1 = 𝟙 Q
g₂ : (Q, T).2 ⟶ (P, S).2
hfg₂ : f.2 ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.2 = 𝟙 T
⊢ g₁ ≫ f.1 = 𝟙 Q

case mpr.intro.mk.intro.intro.mk.intro.intro.refine_2.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).1 ⟶ (P, S).1
hfg₁ : f.1 ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.1 = 𝟙 Q
g₂ : (Q, T).2 ⟶ (P, S).2
hfg₂ : f.2 ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.2 = 𝟙 T
⊢ g₂ ≫ f.2 = 𝟙 T
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_ofSubtype {p : α → Prop} [DecidablePred p] (u : Perm (Subtype p)) :
    (ofSubtype u).support = u.support.map (Function.Embedding.subtype p)

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
⊢ (ofSubtype u).support = map (Embedding.subtype p) u.support

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
⊢ x ∈ (ofSubtype u).support ↔ x ∈ map (Embedding.subtype p) u.support

Proof state:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x

Tactic:
simp only [forall_prop_of_true hx, ofSubtype_apply_of_mem u hx, ← Subtype.coe_inj]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x

Tactic:
by_cases hx : p x

Result:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x

case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : ¬p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x

Proof state:
case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : ¬p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x

Tactic:
simp only [forall_prop_of_false hx, true_iff, ofSubtype_apply_of_not_mem u hx]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
⊢ x ∈ (ofSubtype u).support ↔ x ∈ map (Embedding.subtype p) u.support

Tactic:
simp only [mem_support, ne_eq, Finset.mem_map, Function.Embedding.coe_subtype, Subtype.exists,
  exists_and_right, exists_eq_right, not_iff_comm, not_exists, not_not]

Result:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem ωSup_apply_ωSup (c₀ : Chain (α →𝒄 β)) (c₁ : Chain α) :
    ωSup c₀ (ωSup c₁) = Prod.apply (ωSup (c₀.zip c₁))

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
⊢ (ωSup c₀) (ωSup c₁) = Prod.apply (ωSup (c₀.zip c₁))

Tactic:
simp [Prod.apply_apply, Prod.ωSup_zip]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem fin_two_induction (P : SL(2, R) → Prop)
    (h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], by rwa [det_fin_two_of]⟩)
    (g : SL(2, R)) : P g

Proof state:
case h.e'_1.h.e'_3
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m = !![m 0 0, m 0 1; m 1 0, m 1 1]

Tactic:
ext i j

Result:
case h.e'_1.h.e'_3.a
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
i j : Fin 2
⊢ m i j = !![m 0 0, m 0 1; m 1 0, m 1 1] i j

Proof state:
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1

Tactic:
rwa [det_fin_two] at hm

Result:
no goals

Proof state:
case h.e'_1.h.e'_3.a
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
i j : Fin 2
⊢ m i j = !![m 0 0, m 0 1; m 1 0, m 1 1] i j

Tactic:
fin_cases i <;> fin_cases j <;> rfl

Result:
no goals

Proof state:
case mk
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ P ⟨m, hm⟩

Tactic:
convert h (m 0 0) (m 0 1) (m 1 0) (m 1 1) (by rwa [det_fin_two] at hm)

Result:
case h.e'_1.h.e'_3
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m = !![m 0 0, m 0 1; m 1 0, m 1 1]

Proof state:
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
g : SL(2, R)
⊢ P g

Tactic:
obtain ⟨m, hm⟩ := g

Result:
case mk
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ P ⟨m, hm⟩

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
a b c d : R
hdet : a * d - b * c = 1
⊢ !![a, b; c, d].det = 1

Tactic:
rwa [det_fin_two_of]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem toMatrix_smul {R₁ S : Type*} [CommRing R₁] [Ring S] [Algebra R₁ S] [Fintype ι]
    [DecidableEq ι] (x : S) (b : Basis ι R₁ S) (w : ι → S) :
    (b.toMatrix (x • w)) = (Algebra.leftMulMatrix b x) * (b.toMatrix w)

Proof state:
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommRing R₁
inst✝³ : Ring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
⊢ b.toMatrix (x • w) = (Algebra.leftMulMatrix b) x * b.toMatrix w

Tactic:
ext

Result:
case a
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommRing R₁
inst✝³ : Ring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i✝ j✝ : ι
⊢ b.toMatrix (x • w) i✝ j✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝

Proof state:
case a
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommRing R₁
inst✝³ : Ring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i✝ j✝ : ι
⊢ ((Algebra.leftMulMatrix b) x *ᵥ ⇑(b.repr (w j✝))) i✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
case a
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommRing R₁
inst✝³ : Ring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i✝ j✝ : ι
⊢ b.toMatrix (x • w) i✝ j✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝

Tactic:
rw [Basis.toMatrix_apply, Pi.smul_apply, smul_eq_mul, ← Algebra.leftMulMatrix_mulVec_repr]

Result:
case a
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommRing R₁
inst✝³ : Ring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i✝ j✝ : ι
⊢ ((Algebra.leftMulMatrix b) x *ᵥ ⇑(b.repr (w j✝))) i✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma GrowsPolynomially.of_isEquivalent {f g : ℝ → ℝ} (hg : GrowsPolynomially g)
    (hf : f ~[atTop] g) : GrowsPolynomially f

Proof state:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially f

Tactic:
rw [this]

Result:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially (g + (f - g))

Proof state:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
⊢ GrowsPolynomially f

Tactic:
have : f = g + (f - g) := by ext; simp

Result:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially f

Proof state:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
this : f = g + (f - g)
⊢ GrowsPolynomially (g + (f - g))

Tactic:
exact add_isLittleO hg hf

Result:
no goals

Proof state:
case h
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
x✝ : ℝ
⊢ f x✝ = (g + (f - g)) x✝

Tactic:
simp

Result:
no goals

Proof state:
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
⊢ f = g + (f - g)

Tactic:
ext

Result:
case h
f g : ℝ → ℝ
hg : GrowsPolynomially g
hf : f ~[atTop] g
x✝ : ℝ
⊢ f x✝ = (g + (f - g)) x✝
-- Mathlib/Data/Matrix/Notation.lean
theorem tail_transpose (A : Matrix m' (Fin n.succ) α) : vecTail (of.symm Aᵀ) = (vecTail ∘ A)ᵀ

Proof state:
case h.h
α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
i : Fin n
j : m'
⊢ vecTail (of.symm Aᵀ) i j = (vecTail ∘ A)ᵀ i j

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
⊢ vecTail (of.symm Aᵀ) = (vecTail ∘ A)ᵀ

Tactic:
ext i j

Result:
case h.h
α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
i : Fin n
j : m'
⊢ vecTail (of.symm Aᵀ) i j = (vecTail ∘ A)ᵀ i j
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblX_smul (P : Fin 3 → R) (u : R) : W'.dblX (u • P) = (u ^ 4) ^ 2 * W'.dblX P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblX (u • P) = (u ^ 4) ^ 2 * W'.dblX P

Tactic:
simp only [dblX, dblU_smul, negY_smul, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ (u ^ 4 * W'.dblU P) ^ 2 - W'.a₁ * (u ^ 4 * W'.dblU P) * (u * P z) * (u ^ 3 * P y - u ^ 3 * W'.negY P) -
        W'.a₂ * (u * P z) ^ 2 * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 2 -
      2 * (u ^ 2 * P x) * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 2 =
    (u ^ 4) ^ 2 *
      (W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) - W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
        2 * P x * (P y - W'.negY P) ^ 2)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ (u ^ 4 * W'.dblU P) ^ 2 - W'.a₁ * (u ^ 4 * W'.dblU P) * (u * P z) * (u ^ 3 * P y - u ^ 3 * W'.negY P) -
        W'.a₂ * (u * P z) ^ 2 * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 2 -
      2 * (u ^ 2 * P x) * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 2 =
    (u ^ 4) ^ 2 *
      (W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) - W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
        2 * P x * (P y - W'.negY P) ^ 2)

Tactic:
ring1

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem countable_image_lt_image_Ioi [OrderTopology α] [LinearOrder β] (f : β → α)
    [SecondCountableTopology α] : Set.Countable {x | ∃ z, f x < z ∧ ∀ y, x < y → z ≤ f y}

Proof state:
case H
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
f : β → α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ (y : β), x < y → z x ≤ f y
x : β
hx : x ∈ s
y : β
x✝ : y ∈ s
hxy : x < y
⊢ f x < f y

Tactic:
calc
  f x < z x := (hz x hx).1
  _ ≤ f y := (hz x hx).2 y hxy

Result:
no goals

Proof state:
case intro.intro.intro.intro.inr
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
f : β → α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial β
this✝ : Nonempty α
s : Set β := {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ (y : β), x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
this : ∀ u ∈ s, ∀ v ∈ s, f u ≠ f v → u ≤ v → (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
hle : ¬u ≤ v
⊢ (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)

Tactic:
exact (this v vs u us huv.symm (le_of_not_le hle)).symm

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
f : β → α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ (y : β), x < y → z x ≤ f y
I : InjOn f s
fs_count : (f '' s).Countable
⊢ {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable

Tactic:
exact MapsTo.countable_of_injOn (mapsTo_image f s) I fs_count

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
f : β → α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ (y : β), x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
a : α
ha : a ∈ Ioo (f u) (z u)
hb : a ∈ Ioo (f v) (z v)
⊢ False

Tactic:
exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v hlt)).trans hb.1)

Result:
no goals

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
f : β → α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ (y : β), x < y → z x ≤ f y
I : InjOn f s
A : (f '' s).PairwiseDisjoint fun x => Ioo x (z (invFunOn f s x))
y : β
ys : y ∈ s
⊢ f y < z (invFunOn f s (f y))

Tactic:
simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobject_arrow_comp : (kernelSubobject f).arrow ≫ f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ (kernelSubobject f).arrow ≫ f = 0

Tactic:
rw [← kernelSubobject_arrow]

Result:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ ((kernelSubobjectIso f).hom ≫ kernel.ι f) ≫ f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ ((kernelSubobjectIso f).hom ≫ kernel.ι f) ≫ f = 0

Tactic:
simp only [Category.assoc, kernel.condition, comp_zero]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalHorizontalCompAux'_whisker {f f' g g' h : C} {η : g ⟶ h} {θ : f' ⟶ g'}
    {ηθ : g ⊗ f' ⟶ h ⊗ g'} {η₁ : f ⊗ (g ⊗ f') ⟶ f ⊗ (h ⊗ g')}
    {η₂ :  f ⊗ (g ⊗ f') ⟶ (f ⊗ h) ⊗ g'} {η₃ : (f ⊗ g) ⊗ f' ⟶ (f ⊗ h) ⊗ g'}
    (e_ηθ : η ⊗ θ = ηθ) (e_η₁ : f ◁ ηθ = η₁)
    (e_η₂ : η₁ ≫ (α_ _ _ _).inv = η₂) (e_η₃ : (α_ _ _ _).hom ≫ η₂ = η₃) :
    (f ◁ η) ⊗ θ = η₃

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
ηθ : g ⊗ f' ⟶ h ⊗ g'
η₁ : f ⊗ g ⊗ f' ⟶ f ⊗ h ⊗ g'
η₂ : f ⊗ g ⊗ f' ⟶ (f ⊗ h) ⊗ g'
η₃ : (f ⊗ g) ⊗ f' ⟶ (f ⊗ h) ⊗ g'
e_ηθ : η ⊗ θ = ηθ
e_η₁ : f ◁ ηθ = η₁
e_η₂ : η₁ ≫ (α_ f h g').inv = η₂
e_η₃ : (α_ f g f').hom ≫ η₂ = η₃
⊢ f ◁ η ⊗ θ = (α_ f g f').hom ≫ f ◁ (η ⊗ θ) ≫ (α_ f h g').inv

Tactic:
simp [MonoidalCategory.tensorHom_def]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
ηθ : g ⊗ f' ⟶ h ⊗ g'
η₁ : f ⊗ g ⊗ f' ⟶ f ⊗ h ⊗ g'
η₂ : f ⊗ g ⊗ f' ⟶ (f ⊗ h) ⊗ g'
η₃ : (f ⊗ g) ⊗ f' ⟶ (f ⊗ h) ⊗ g'
e_ηθ : η ⊗ θ = ηθ
e_η₁ : f ◁ ηθ = η₁
e_η₂ : η₁ ≫ (α_ f h g').inv = η₂
e_η₃ : (α_ f g f').hom ≫ η₂ = η₃
⊢ f ◁ η ⊗ θ = η₃

Tactic:
simp only [← e_ηθ, ← e_η₁, ← e_η₂, ← e_η₃]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
ηθ : g ⊗ f' ⟶ h ⊗ g'
η₁ : f ⊗ g ⊗ f' ⟶ f ⊗ h ⊗ g'
η₂ : f ⊗ g ⊗ f' ⟶ (f ⊗ h) ⊗ g'
η₃ : (f ⊗ g) ⊗ f' ⟶ (f ⊗ h) ⊗ g'
e_ηθ : η ⊗ θ = ηθ
e_η₁ : f ◁ ηθ = η₁
e_η₂ : η₁ ≫ (α_ f h g').inv = η₂
e_η₃ : (α_ f g f').hom ≫ η₂ = η₃
⊢ f ◁ η ⊗ θ = (α_ f g f').hom ≫ f ◁ (η ⊗ θ) ≫ (α_ f h g').inv
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_div (p q : K[X]) :
    num (algebraMap _ _ p / algebraMap _ _ q) =
      Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

Proof state:
case pos
K : Type u
inst✝ : Field K
p q : K[X]
hq : q = 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num =
    C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

Tactic:
simp [hq]

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
p q : K[X]
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num =
    C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

Tactic:
by_cases hq : q = 0

Result:
case pos
K : Type u
inst✝ : Field K
p q : K[X]
hq : q = 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num =
    C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num =
    C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

Proof state:
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num =
    C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

Tactic:
exact num_div' p hq

Result:
no goals
-- Mathlib/FieldTheory/KrullTopology.lean
lemma krullTopology_mem_nhds_one_iff (K L : Type*) [Field K] [Field L] [Algebra K L]
    (s : Set (L ≃ₐ[K] L)) : s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L,
    FiniteDimensional K E ∧ (E.fixingSubgroup : Set (L ≃ₐ[K] L)) ⊆ s

Proof state:
case mp.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
E : IntermediateField K L
fin : E ∈ finiteExts K L
hE : (fun g => g.carrier) E.fixingSubgroup ⊆ s
⊢ ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
exact ⟨E, fin, hE⟩

Result:
no goals

Proof state:
case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
⊢ (∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s) → s ∈ GroupFilterBasis.toFilterBasis.filter

Tactic:
rintro ⟨E, fin, hE⟩

Result:
case mpr.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
E : IntermediateField K L
fin : FiniteDimensional K ↥E
hE : ↑E.fixingSubgroup ⊆ s
⊢ s ∈ GroupFilterBasis.toFilterBasis.filter

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
⊢ s ∈ GroupFilterBasis.toFilterBasis.filter ↔ ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
constructor

Result:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
⊢ s ∈ GroupFilterBasis.toFilterBasis.filter → ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
⊢ (∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s) → s ∈ GroupFilterBasis.toFilterBasis.filter

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
⊢ s ∈ 𝓝 1 ↔ ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
rw [GroupFilterBasis.nhds_one_eq]

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
⊢ s ∈ GroupFilterBasis.toFilterBasis.filter ↔ ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Proof state:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
⊢ s ∈ GroupFilterBasis.toFilterBasis.filter → ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
rintro ⟨-, ⟨-, ⟨E, fin, rfl⟩, rfl⟩, hE⟩

Result:
case mp.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
E : IntermediateField K L
fin : E ∈ finiteExts K L
hE : (fun g => g.carrier) E.fixingSubgroup ⊆ s
⊢ ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Proof state:
case mpr.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set (L ≃ₐ[K] L)
E : IntermediateField K L
fin : FiniteDimensional K ↥E
hE : ↑E.fixingSubgroup ⊆ s
⊢ s ∈ GroupFilterBasis.toFilterBasis.filter

Tactic:
exact ⟨E.fixingSubgroup, ⟨E.fixingSubgroup, ⟨E, fin, rfl⟩, rfl⟩, hE⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
@[simp]
lemma charmatrix_blockTriangular_iff {α : Type*} [Preorder α] {M : Matrix n n R} {b : n → α} :
    M.charmatrix.BlockTriangular b ↔ M.BlockTriangular b

Proof state:
R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α : Type u_5
inst✝ : Preorder α
M : Matrix n n R
b : n → α
⊢ M.charmatrix.BlockTriangular b ↔ M.BlockTriangular b

Tactic:
rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, (blockTriangular_diagonal _).sub_iff_right]

Result:
R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α : Type u_5
inst✝ : Preorder α
M : Matrix n n R
b : n → α
⊢ (M.map ⇑C).BlockTriangular b ↔ M.BlockTriangular b

Proof state:
R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α : Type u_5
inst✝ : Preorder α
M : Matrix n n R
b : n → α
⊢ (M.map ⇑C).BlockTriangular b ↔ M.BlockTriangular b

Tactic:
simp [BlockTriangular]

Result:
no goals