harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem ofPermHom_mem_centralizer :
    a.ofPermHom τ ∈ centralizer {g}

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ a.ofPermHom τ * g = g * a.ofPermHom τ

Tactic:
ext x

Result:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ (a.ofPermHom τ * g) x = (g * a.ofPermHom τ) x

Proof state:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ (a.ofPermHom τ) (g x) = g ((a.ofPermHom τ) x)

Tactic:
exact ofPermHomFun_commute_zpow_apply a τ x 1

Result:
no goals

Proof state:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ (a.ofPermHom τ * g) x = (g * a.ofPermHom τ) x

Tactic:
simp only [mul_apply]

Result:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ (a.ofPermHom τ) (g x) = g ((a.ofPermHom τ) x)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ a.ofPermHom τ ∈ centralizer {g}

Tactic:
rw [mem_centralizer_singleton_iff]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ a.ofPermHom τ * g = g * a.ofPermHom τ
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem commonNeighbors_top_eq {v w : V} :
    (⊤ : SimpleGraph V).commonNeighbors v w = Set.univ \ {v, w}

Proof state:
case h
V : Type u
v w u : V
⊢ u ∈ ⊤.commonNeighbors v w ↔ u ∈ Set.univ \ {v, w}

Tactic:
simp [commonNeighbors, eq_comm, not_or]

Result:
no goals

Proof state:
V : Type u
v w : V
⊢ ⊤.commonNeighbors v w = Set.univ \ {v, w}

Tactic:
ext u

Result:
case h
V : Type u
v w u : V
⊢ u ∈ ⊤.commonNeighbors v w ↔ u ∈ Set.univ \ {v, w}
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_sub_intCast' {n : ℤ} (h : y - n ≠ 0) (x : ℝ≥0) : x ^ (y - n) = x ^ y / x ^ n

Proof state:
y : ℝ
n : ℤ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
ext

Result:
case a
y : ℝ
n : ℤ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)

Proof state:
case a
y : ℝ
n : ℤ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)

Tactic:
exact Real.rpow_sub_intCast' (mod_cast x.2) h

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
lemma toColex_lt_toColex_iff_max'_mem :
    toColex s < toColex t ↔ ∃ hst : s ≠ t, (s ∆ t).max' (symmDiff_nonempty.2 hst) ∈ t

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t) ∧ { ofColex := s } ≠ { ofColex := t } ↔ ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ { ofColex := s } < { ofColex := t } ↔ ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
rw [lt_iff_le_and_ne, toColex_le_toColex_iff_max'_mem]

Result:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t) ∧ { ofColex := s } ≠ { ofColex := t } ↔ ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
-- Mathlib/Data/Fin/Basic.lean
theorem coe_eq_castSucc {a : Fin n} : (a : Fin (n + 1)) = castSucc a

Proof state:
n : ℕ
a : Fin n
⊢ ↑↑a = a.castSucc

Tactic:
ext

Result:
case h
n : ℕ
a : Fin n
⊢ ↑↑↑a = ↑a.castSucc

Proof state:
case h
n : ℕ
a : Fin n
⊢ ↑↑↑a = ↑a.castSucc

Tactic:
exact val_cast_of_lt (Nat.lt.step a.is_lt)

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem coe_ennreal_mul : ∀ x y : ℝ≥0∞, ((x * y : ℝ≥0∞) : EReal) = (x : EReal) * y
  | ⊤, ⊤ => rfl
  | ⊤, (y : ℝ≥0) => coe_ennreal_top_mul y
  | (x : ℝ≥0), ⊤ => by
    rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]
  | (x : ℝ≥0), (y : ℝ≥0) => by
    simp only [← ENNReal.coe_mul, coe_nnreal_eq_coe_real, NNReal.coe_mul, EReal.coe_mul]

Proof state:
x : ℝ≥0
⊢ ↑(↑x * ⊤) = ↑↑x * ↑⊤

Tactic:
rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]

Result:
no goals

Proof state:
x y : ℝ≥0
⊢ ↑(↑x * ↑y) = ↑↑x * ↑↑y

Tactic:
simp only [← ENNReal.coe_mul, coe_nnreal_eq_coe_real, NNReal.coe_mul, EReal.coe_mul]

Result:
no goals
-- Mathlib/Algebra/Module/FinitePresentation.lean
theorem Module.FinitePresentation.exists_fin [fp : Module.FinitePresentation R M] :
    ∃ (n : ℕ) (K : Submodule R (Fin n → R)) (_ : M ≃ₗ[R] (Fin n → R) ⧸ K), K.FG

Proof state:
case refine_1
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Submodule.span R ↑ι = ⊤
hι₂ : (LinearMap.ker (linearCombination R Subtype.val)).FG
⊢ LinearMap.range
      (linearCombination R Subtype.val ∘ₗ
        ↑(lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card)).symm) =
    ⊤

Tactic:
simpa [range_linearCombination] using hι₁

Result:
no goals

Proof state:
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
⊢ ∃ n K x, K.FG

Tactic:
have ⟨ι, ⟨hι₁, hι₂⟩⟩ := fp

Result:
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Submodule.span R ↑ι = ⊤
hι₂ : (LinearMap.ker (linearCombination R Subtype.val)).FG
⊢ ∃ n K x, K.FG

Proof state:
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Submodule.span R ↑ι = ⊤
hι₂ : (LinearMap.ker (linearCombination R Subtype.val)).FG
⊢ ∃ n K x, K.FG

Tactic:
refine ⟨_, LinearMap.ker (linearCombination R Subtype.val ∘ₗ
  (lcongr ι.equivFin (.refl ..) ≪≫ₗ linearEquivFunOnFinite R R _).symm.toLinearMap),
  (LinearMap.quotKerEquivOfSurjective _ <| LinearMap.range_eq_top.mp ?_).symm, ?_⟩

Result:
case refine_1
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Submodule.span R ↑ι = ⊤
hι₂ : (LinearMap.ker (linearCombination R Subtype.val)).FG
⊢ LinearMap.range
      (linearCombination R Subtype.val ∘ₗ
        ↑(lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card)).symm) =
    ⊤

case refine_2
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Submodule.span R ↑ι = ⊤
hι₂ : (LinearMap.ker (linearCombination R Subtype.val)).FG
⊢ (LinearMap.ker
      (linearCombination R Subtype.val ∘ₗ
        ↑(lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card)).symm)).FG

Proof state:
case refine_2
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Submodule.span R ↑ι = ⊤
hι₂ : (LinearMap.ker (linearCombination R Subtype.val)).FG
⊢ (LinearMap.ker
      (linearCombination R Subtype.val ∘ₗ
        ↑(lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card)).symm)).FG

Tactic:
simpa [LinearMap.ker_comp, Submodule.comap_equiv_eq_map_symm] using hι₂.map _

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem map_id' {α : Type*} {n : ℕ} (s : Sym α n) : Sym.map (fun x : α => x) s = s

Proof state:
case h
α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map (fun x => x) s) = ↑s

Tactic:
simp only [map, Multiset.map_id', ← val_eq_coe]

Result:
no goals

Proof state:
α : Type u_3
n : ℕ
s : Sym α n
⊢ map (fun x => x) s = s

Tactic:
ext

Result:
case h
α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map (fun x => x) s) = ↑s
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofMkLEMk_refl {B A₁ : C} (f : A₁ ⟶ B) [Mono f] : ofMkLEMk f f le_rfl = 𝟙 _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
⊢ ofMkLEMk f f ⋯ = 𝟙 A₁

Tactic:
apply (cancel_mono f).mp

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
⊢ ofMkLEMk f f ⋯ ≫ f = 𝟙 A₁ ≫ f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
⊢ ofMkLEMk f f ⋯ ≫ f = 𝟙 A₁ ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem rename_injective (f : σ → τ) (hf : Function.Injective f) :
    Function.Injective (rename f : MvPolynomial σ R → MvPolynomial τ R)

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
⊢ Injective ⇑(rename f)

Tactic:
have :
  (rename f : MvPolynomial σ R → MvPolynomial τ R) = Finsupp.mapDomain (Finsupp.mapDomain f) :=
  funext (rename_eq f)

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
this : ⇑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective ⇑(rename f)

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
this : ⇑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective ⇑(rename f)

Tactic:
rw [this]

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
this : ⇑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective (Finsupp.mapDomain (Finsupp.mapDomain f))

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
this : ⇑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective (Finsupp.mapDomain (Finsupp.mapDomain f))

Tactic:
exact Finsupp.mapDomain_injective (Finsupp.mapDomain_injective hf)

Result:
no goals
-- Mathlib/Data/Nat/Count.lean
theorem count_mono_left {n : ℕ} (hpq : ∀ k, p k → q k) : count p n ≤ count q n

Proof state:
p : ℕ → Prop
inst✝¹ : DecidablePred p
q : ℕ → Prop
inst✝ : DecidablePred q
n : ℕ
hpq : ∀ (k : ℕ), p k → q k
⊢ #(filter (fun x => p x) (range n)) ≤ #(filter (fun x => q x) (range n))

Tactic:
exact card_le_card ((range n).monotone_filter_right hpq)

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝¹ : DecidablePred p
q : ℕ → Prop
inst✝ : DecidablePred q
n : ℕ
hpq : ∀ (k : ℕ), p k → q k
⊢ count p n ≤ count q n

Tactic:
simp only [count_eq_card_filter_range]

Result:
p : ℕ → Prop
inst✝¹ : DecidablePred p
q : ℕ → Prop
inst✝ : DecidablePred q
n : ℕ
hpq : ∀ (k : ℕ), p k → q k
⊢ #(filter (fun x => p x) (range n)) ≤ #(filter (fun x => q x) (range n))
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem coplanar_of_finrank_eq_two (s : Set P) (h : finrank k V = 2) : Coplanar k s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : finrank k V = 2
⊢ Coplanar k s

Tactic:
have : FiniteDimensional k V := .of_finrank_eq_succ h

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : finrank k V = 2
this : FiniteDimensional k V
⊢ Coplanar k s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : finrank k V = 2
this : FiniteDimensional k V
⊢ Coplanar k s

Tactic:
rw [coplanar_iff_finrank_le_two, ← h]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : finrank k V = 2
this : FiniteDimensional k V
⊢ finrank k ↥(vectorSpan k s) ≤ finrank k V

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : finrank k V = 2
this : FiniteDimensional k V
⊢ finrank k ↥(vectorSpan k s) ≤ finrank k V

Tactic:
exact Submodule.finrank_le _

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem updateRow_submatrix_equiv [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l)
    (r : o → α) (e : l ≃ m) (f : o ≃ n) :
    updateRow (A.submatrix e f) i r = (A.updateRow (e i) fun j => r (f.symm j)).submatrix e f

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
⊢ (A.submatrix ⇑e ⇑f).updateRow i r = (A.updateRow (e i) fun j => r (f.symm j)).submatrix ⇑e ⇑f

Tactic:
ext i' j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
i' : l
j : o
⊢ (A.submatrix ⇑e ⇑f).updateRow i r i' j = (A.updateRow (e i) fun j => r (f.symm j)).submatrix (⇑e) (⇑f) i' j

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
i' : l
j : o
⊢ (A.submatrix ⇑e ⇑f).updateRow i r i' j = (A.updateRow (e i) fun j => r (f.symm j)).submatrix (⇑e) (⇑f) i' j

Tactic:
simp only [submatrix_apply, updateRow_apply, Equiv.apply_eq_iff_eq, Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/Data/Multiset/Lattice.lean
theorem inf_ndunion (s₁ s₂ : Multiset α) : (ndunion s₁ s₂).inf = s₁.inf ⊓ s₂.inf

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).inf = s₁.inf ⊓ s₂.inf

Tactic:
rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_add]

Result:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem piecewise_compl [∀ i, Decidable (i ∈ sᶜ)] : sᶜ.piecewise f g = s.piecewise g f :=
  funext fun x => if hx : x ∈ s then by simp [hx] else by simp [hx]

Proof state:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : x ∈ s
⊢ sᶜ.piecewise f g x = s.piecewise g f x

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : x ∉ s
⊢ sᶜ.piecewise f g x = s.piecewise g f x

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem zero_rpow_of_pos {y : ℝ} (h : 0 < y) : (0 : ℝ≥0∞) ^ y = 0

Proof state:
y : ℝ
h : 0 < y
⊢ (if 0 = 0 ∧ y < 0 then ⊤ else ↑(NNReal.rpow 0 y)) = some 0

Tactic:
simp [h, asymm h, ne_of_gt h]

Result:
no goals

Proof state:
y : ℝ
h : 0 < y
⊢ 0 ^ y = 0

Tactic:
rw [← ENNReal.coe_zero, ← ENNReal.some_eq_coe]

Result:
y : ℝ
h : 0 < y
⊢ some 0 ^ y = some 0
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.countable (hs : f.IsCycleOn s) : s.Countable

Proof state:
case inl
α : Type u_2
f : Perm α
hs : f.IsCycleOn ∅
⊢ ∅.Countable

Tactic:
exact Set.countable_empty

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
⊢ s.Countable

Tactic:
obtain rfl | ⟨a, ha⟩ := s.eq_empty_or_nonempty

Result:
case inl
α : Type u_2
f : Perm α
hs : f.IsCycleOn ∅
⊢ ∅.Countable

case inr.intro
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
a : α
ha : a ∈ s
⊢ s.Countable

Proof state:
case inr.intro
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
a : α
ha : a ∈ s
⊢ s.Countable

Tactic:
exact (Set.countable_range fun n : ℤ => (⇑(f ^ n) : α → α) a).mono (hs.2 ha)

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.inter_iInter_nonempty {ι : Type v} (hs : IsLindelof s) (t : ι → Set X)
    (htc : ∀ i, IsClosed (t i)) (hst : ∀ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty) :
    (s ∩ ⋂ i, t i).Nonempty

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : ∀ (u : Set ι), u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty
⊢ (s ∩ ⋂ i, t i).Nonempty

Tactic:
contrapose! hst

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ ∃ u, u.Countable → s ∩ ⋂ i ∈ u, t i = ∅

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
u : Set ι
left✝ : u.Countable
husub : s ∩ ⋂ i ∈ u, t i = ∅
⊢ ∃ u, u.Countable → s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
exact ⟨u, fun _ ↦ husub⟩

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ ∃ u, u.Countable → s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
rcases hs.elim_countable_subfamily_closed t htc hst with ⟨u, ⟨_, husub⟩⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
u : Set ι
left✝ : u.Countable
husub : s ∩ ⋂ i ∈ u, t i = ∅
⊢ ∃ u, u.Countable → s ∩ ⋂ i ∈ u, t i = ∅
-- Mathlib/Data/Set/Finite/Basic.lean
theorem card_fintypeInsertOfNotMem {a : α} (s : Set α) [Fintype s] (h : a ∉ s) :
    @Fintype.card _ (fintypeInsertOfNotMem s h) = Fintype.card s + 1

Proof state:
α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

Tactic:
simp [fintypeInsertOfNotMem, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/Tower.lean
theorem minpoly.map_eq_of_isSeparable_of_isPurelyInseparable (x : K)
    (hsep : IsSeparable F x) [IsPurelyInseparable F E] :
    (minpoly F x).map (algebraMap F E) = minpoly E x

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
⊢ (Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree

Tactic:
have hsep' := IsSeparable.tower_top E hsep

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
⊢ (Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem eq_one_of_mul_left (h : a * b = 1) : b = 1

Proof state:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b = 1

Tactic:
rwa [LeftCancelMonoid.eq_one_of_mul_right h, one_mul] at h

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem _root_.MeasurableEmbedding.integral_map {β} {_ : MeasurableSpace β} {f : α → β}
    (hf : MeasurableEmbedding f) (g : β → G) : ∫ y, g y ∂Measure.map f μ = ∫ x, g (f x) ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : AEStronglyMeasurable g (Measure.map f μ)
⊢ ∫ (y : β), g y ∂Measure.map f μ = ∫ (x : α), g (f x) ∂μ

Tactic:
exact MeasureTheory.integral_map hf.measurable.aemeasurable hgm

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
⊢ ∫ (y : β), g y ∂Measure.map f μ = ∫ (x : α), g (f x) ∂μ

Tactic:
by_cases hgm : AEStronglyMeasurable g (Measure.map f μ)

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : AEStronglyMeasurable g (Measure.map f μ)
⊢ ∫ (y : β), g y ∂Measure.map f μ = ∫ (x : α), g (f x) ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ ∫ (y : β), g y ∂Measure.map f μ = ∫ (x : α), g (f x) ∂μ

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ ¬AEStronglyMeasurable (fun x => g (f x)) μ

Tactic:
exact fun hgf => hgm (hf.aestronglyMeasurable_map_iff.2 hgf)

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ ∫ (y : β), g y ∂Measure.map f μ = ∫ (x : α), g (f x) ∂μ

Tactic:
rw [integral_non_aestronglyMeasurable hgm, integral_non_aestronglyMeasurable]

Result:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : ¬AEStronglyMeasurable g (Measure.map f μ)
⊢ ¬AEStronglyMeasurable (fun x => g (f x)) μ
-- Mathlib/Data/ENNReal/Order.lean
theorem pow_ne_zero : a ≠ 0 → ∀ n : ℕ, a ^ n ≠ 0

Proof state:
a : ℝ≥0∞
⊢ a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0

Tactic:
simpa only [pos_iff_ne_zero] using ENNReal.pow_pos

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_vsub_right (p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ (lineMap p₀ p₁) c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)

Tactic:
rw [← lineMap_apply_one_sub, lineMap_vsub_left]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_mul_le_one_iff : a⁻¹ * b ≤ 1 ↔ b ≤ a :=
  inv_mul_le_iff_le_mul.trans <| by rw [mul_one]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ b ≤ a * 1 ↔ b ≤ a

Tactic:
rw [mul_one]

Result:
no goals