harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
theorem arrow_trans (f : Y ⟶ X) (S R : Sieve X) (h : J.Covers S f) :
    (∀ {Z : C} (g : Z ⟶ X), S g → J.Covers R g) → J.Covers R f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
⊢ J.Covers R f

Tactic:
apply J.transitive h

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄, (Sieve.pullback f S).arrows f_1 → Sieve.pullback f_1 (Sieve.pullback f R) ∈ J Y_1

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback (g ≫ f) R ∈ J Z

Tactic:
apply k (g ≫ f) hg

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄, (Sieve.pullback f S).arrows f_1 → Sieve.pullback f_1 (Sieve.pullback f R) ∈ J Y_1

Tactic:
intro Z g hg

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback g (Sieve.pullback f R) ∈ J Z

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback g (Sieve.pullback f R) ∈ J Z

Tactic:
rw [← Sieve.pullback_comp]

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback (g ≫ f) R ∈ J Z

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
⊢ (∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g) → J.Covers R f

Tactic:
intro k

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
⊢ J.Covers R f
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
lemma finrank_le_of_span_eq_top {ι : Type*} [Fintype ι] {v : ι → M}
    (hv : Submodule.span R (Set.range v) = ⊤) : finrank R M ≤ Fintype.card ι

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ (range v).toFinset.card ≤ Fintype.card ι

Tactic:
convert Fintype.card_range_le v

Result:
case h.e'_3
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ (range v).toFinset.card = Fintype.card ↑(range v)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ finrank R M ≤ Fintype.card ι

Tactic:
rw [← finrank_top, ← hv]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ finrank R ↥(span R (range v)) ≤ Fintype.card ι

Proof state:
case h.e'_3
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ (range v).toFinset.card = Fintype.card ↑(range v)

Tactic:
rw [Set.toFinset_card]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ finrank R ↥(span R (range v)) ≤ Fintype.card ι

Tactic:
exact (finrank_span_le_card _).trans (by convert Fintype.card_range_le v; rw [Set.toFinset_card])

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ finrank R M ≤ Fintype.card ι

Tactic:
classical
rw [← finrank_top, ← hv]
exact (finrank_span_le_card _).trans (by convert Fintype.card_range_le v; rw [Set.toFinset_card])

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
theorem IsGδ.measurableSet (h : IsGδ s) : MeasurableSet s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
S : Set (Set α)
hSo : ∀ t ∈ S, IsOpen t
hSc : S.Countable
⊢ MeasurableSet (⋂₀ S)

Tactic:
exact MeasurableSet.sInter hSc fun t ht => (hSo t ht).measurableSet

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
h : IsGδ s
⊢ MeasurableSet s

Tactic:
rcases h with ⟨S, hSo, hSc, rfl⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
S : Set (Set α)
hSo : ∀ t ∈ S, IsOpen t
hSc : S.Countable
⊢ MeasurableSet (⋂₀ S)
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem reindex_relationsSet :
    (M.reindex e).relationsSet =
    FreeGroup.freeGroupCongr e '' M.relationsSet := let M' := M.reindex e; calc
  Set.range (uncurry M'.relation)
  _ = Set.range (uncurry M'.relation ∘ Prod.map e e)

Proof state:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ Set.range (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation) = ⇑(FreeGroup.freeGroupCongr e) '' M.relationsSet

Tactic:
simp [Set.range_comp, relationsSet]

Result:
no goals

Proof state:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ uncurry M'.relation ∘ Prod.map ⇑e ⇑e = ⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation

Tactic:
ext ⟨i, i'⟩

Result:
case h.mk
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
i i' : B
⊢ (uncurry M'.relation ∘ Prod.map ⇑e ⇑e) (i, i') = (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation) (i, i')

Proof state:
case h.mk
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
i i' : B
⊢ (uncurry M'.relation ∘ Prod.map ⇑e ⇑e) (i, i') = (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation) (i, i')

Tactic:
simp [relation, reindex_apply, M']

Result:
no goals

Proof state:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ Set.range (uncurry M'.relation ∘ Prod.map ⇑e ⇑e) = Set.range (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation)

Tactic:
apply congrArg Set.range

Result:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ uncurry M'.relation ∘ Prod.map ⇑e ⇑e = ⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation

Proof state:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ Set.range (uncurry M'.relation) = Set.range (uncurry M'.relation ∘ Prod.map ⇑e ⇑e)

Tactic:
simp [Set.range_comp]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem update_injective (f : ∀ a, β a) (a' : α) : Injective (update f a') := fun v v' h ↦ by
  have := congr_fun h a'
  rwa [update_self, update_self] at this

Proof state:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
this : update f a' v a' = update f a' v' a'
⊢ v = v'

Tactic:
rwa [update_self, update_self] at this

Result:
no goals

Proof state:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
⊢ v = v'

Tactic:
have := congr_fun h a'

Result:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
this : update f a' v a' = update f a' v' a'
⊢ v = v'
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem wittStructureRat_rec (Φ : MvPolynomial idx ℚ) (n : ℕ) :
    wittStructureRat p Φ n =
      C (1 / (p : ℚ) ^ n) *
        (bind₁ (fun b => rename (fun i => (b, i)) (W_ ℚ n)) Φ -
          ∑ i ∈ range n, C ((p : ℚ) ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ C (1 / ↑p ^ n) * (wittStructureRat p Φ n * C (↑p ^ n)) =
    C (1 / ↑p ^ n) *
      ((bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))

Tactic:
rw [wittStructureRat_rec_aux]

Result:
no goals

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n =
    C (1 / ↑p ^ n) *
      ((bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))

Tactic:
calc
  wittStructureRat p Φ n = C (1 / (p : ℚ) ^ n) * (wittStructureRat p Φ n * C ((p : ℚ) ^ n)) := ?_
  _ = _ := by rw [wittStructureRat_rec_aux]

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = C (1 / ↑p ^ n) * (wittStructureRat p Φ n * C (↑p ^ n))

Proof state:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0

Tactic:
exact pow_ne_zero _ (Nat.cast_ne_zero.2 hp.1.ne_zero)

Result:
no goals

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = C (1 / ↑p ^ n) * (wittStructureRat p Φ n * C (↑p ^ n))

Tactic:
rw [mul_left_comm, ← C_mul, div_mul_cancel₀, C_1, mul_one]

Result:
case h
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem tendsto_approxOn_L1_enorm [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f)
    {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s] {μ : Measure β}
    (hμ : ∀ᵐ x ∂μ, f x ∈ closure s) (hi : HasFiniteIntegral (fun x => f x - y₀) μ) :
    Tendsto (fun n => ∫⁻ x, ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ∂μ) atTop (𝓝 0)

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : HasFiniteIntegral (fun x => f x - y₀) μ
⊢ Tendsto (fun n => ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ∂μ) atTop (𝓝 0)

Tactic:
simpa [eLpNorm_one_eq_lintegral_enorm] using
  tendsto_approxOn_Lp_eLpNorm hf h₀ one_ne_top hμ
    (by simpa [eLpNorm_one_eq_lintegral_enorm] using hi)

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : HasFiniteIntegral (fun x => f x - y₀) μ
⊢ eLpNorm (fun x => f x - y₀) 1 μ < ⊤

Tactic:
simpa [eLpNorm_one_eq_lintegral_enorm] using hi

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem expSeries_apply_eq_div (x : 𝔸) (n : ℕ) : (expSeries 𝕂 𝔸 n fun _ => x) = x ^ n / n !

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 => x) = x ^ n / ↑n !

Tactic:
rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul,
  expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝔸]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Basic.lean
theorem exists_not_isUnit_of_not_isField [Nontrivial R] (hf : ¬IsField R) :
    ∃ (x : R) (_hx : x ≠ (0 : R)), ¬IsUnit x

Proof state:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬∃ b, x * b = 1

Tactic:
push_neg at this ⊢

Result:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ∃ a, a ≠ 0 ∧ ∀ (b : R), a * b ≠ 1
⊢ ∃ x, ∃ (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1

Proof state:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x

Tactic:
simp_rw [isUnit_iff_exists_inv]

Result:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬∃ b, x * b = 1

Proof state:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x

Tactic:
have : ¬_ := fun h => hf ⟨exists_pair_ne R, mul_comm, h⟩

Result:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x

Proof state:
case intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
x : R
hx : x ≠ 0
not_unit : ∀ (b : R), x * b ≠ 1
⊢ ∃ x, ∃ (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1

Tactic:
exact ⟨x, hx, not_unit⟩

Result:
no goals

Proof state:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
this : ∃ a, a ≠ 0 ∧ ∀ (b : R), a * b ≠ 1
⊢ ∃ x, ∃ (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1

Tactic:
obtain ⟨x, hx, not_unit⟩ := this

Result:
case intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
x : R
hx : x ≠ 0
not_unit : ∀ (b : R), x * b ≠ 1
⊢ ∃ x, ∃ (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1
-- Mathlib/Algebra/ModEq.lean
theorem zsmul_modEq_zero (z : ℤ) : z • p ≡ 0 [PMOD p] :=
  ⟨-z, by simp⟩

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p : α
z : ℤ
⊢ 0 - z • p = -z • p

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem t2Space_of_covering [T2Space β] (h : ⋃₀ 𝔖 = univ) : T2Space (α →ᵤ[𝔖] β) where
  t2 f g hfg

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous (uniformContinuous_eval_of_mem β 𝔖 hxs hs).continuous hx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
⊢ (fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g

Tactic:
obtain ⟨x, hx⟩ := not_forall.mp (mt funext hfg)

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v

Tactic:
obtain ⟨s, hs, hxs⟩ : ∃ s ∈ 𝔖, x ∈ s := mem_sUnion.mp (h.symm ▸ True.intro)

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsTrivialBlock.smul {B : Set α} (hB : IsTrivialBlock B) (g : M) :
    IsTrivialBlock (g • B)

Proof state:
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
hB : IsTrivialBlock B
g : M
⊢ IsTrivialBlock (g • B)

Tactic:
cases hB with
| inl h =>
  left
  exact (Function.Injective.subsingleton_image_iff (MulAction.injective g)).mpr h
| inr h =>
  right
  rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]

Result:
no goals

Proof state:
case inl
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
h : B.Subsingleton
⊢ IsTrivialBlock (g • B)

Tactic:
left

Result:
case inl.h
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
h : B.Subsingleton
⊢ (g • B).Subsingleton

Proof state:
case inr
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
h : B = univ
⊢ IsTrivialBlock (g • B)

Tactic:
right

Result:
case inr.h
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
h : B = univ
⊢ g • B = univ

Proof state:
case inr.h
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
h : B = univ
⊢ g • B = univ

Tactic:
rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]

Result:
no goals

Proof state:
case inl.h
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
h : B.Subsingleton
⊢ (g • B).Subsingleton

Tactic:
exact (Function.Injective.subsingleton_image_iff (MulAction.injective g)).mpr h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem toArray_range' (start size step) :
    (range' start size step).toArray = Array.range' start size step

Proof state:
start size step : Nat
⊢ (range' start size step).toArray = Array.range' start size step

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Dioph.lean
theorem sub_dioph : DiophFn fun v => f v - g v :=
  diophFn_comp2 df dg <|
    (diophFn_vec _).2 <|
      ext (D&1 D= D&0 D+ D&2 D∨ D&1 D≤ D&2 D∧ D&0 D= D.0) <|
        (vectorAll_iff_forall _).1 fun x y z =>
          show y = x + z ∨ y ≤ z ∧ x = 0 ↔ y - z = x from
            ⟨fun o => by
              rcases o with (ae | ⟨yz, x0⟩)
              · rw [ae, add_tsub_cancel_right]
              · rw [x0, tsub_eq_zero_iff_le.mpr yz], by
              rintro rfl
              rcases le_total y z with yz | zy
              · exact Or.inr ⟨yz, tsub_eq_zero_iff_le.mpr yz⟩
              · exact Or.inl (tsub_add_cancel_of_le zy).symm⟩

Proof state:
case inl
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
ae : y = x + z
⊢ y - z = x

Tactic:
rw [ae, add_tsub_cancel_right]

Result:
no goals

Proof state:
case inr.intro
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
yz : y ≤ z
x0 : x = 0
⊢ y - z = x

Tactic:
rw [x0, tsub_eq_zero_iff_le.mpr yz]

Result:
no goals

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
y z : ℕ
⊢ y = y - z + z ∨ y ≤ z ∧ y - z = 0

Tactic:
rcases le_total y z with yz | zy

Result:
case inl
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
y z : ℕ
yz : y ≤ z
⊢ y = y - z + z ∨ y ≤ z ∧ y - z = 0

case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
y z : ℕ
zy : z ≤ y
⊢ y = y - z + z ∨ y ≤ z ∧ y - z = 0

Proof state:
case inl
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
y z : ℕ
yz : y ≤ z
⊢ y = y - z + z ∨ y ≤ z ∧ y - z = 0

Tactic:
exact Or.inr ⟨yz, tsub_eq_zero_iff_le.mpr yz⟩

Result:
no goals

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
o : y = x + z ∨ y ≤ z ∧ x = 0
⊢ y - z = x

Tactic:
rcases o with (ae | ⟨yz, x0⟩)

Result:
case inl
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
ae : y = x + z
⊢ y - z = x

case inr.intro
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
yz : y ≤ z
x0 : x = 0
⊢ y - z = x

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
⊢ y - z = x → y = x + z ∨ y ≤ z ∧ x = 0

Tactic:
rintro rfl

Result:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
y z : ℕ
⊢ y = y - z + z ∨ y ≤ z ∧ y - z = 0

Proof state:
case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
y z : ℕ
zy : z ≤ y
⊢ y = y - z + z ∨ y ≤ z ∧ y - z = 0

Tactic:
exact Or.inl (tsub_add_cancel_of_le zy).symm

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_div_iff_mul_eq' : a = b / c ↔ a * c = b

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a = b / c ↔ a * c = b

Tactic:
rw [div_eq_mul_inv, eq_mul_inv_iff_mul_eq]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem toList_erase [BEq α] (l : Array α) (a : α) :
    (l.erase a).toList = l.toList.erase a

Proof state:
α : Type u_1
inst✝ : BEq α
l : Array α
a : α
⊢ (l.erase a).toList = l.toList.erase a

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ ({ toList := l }.erase a).toList = { toList := l }.toList.erase a

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ ({ toList := l }.erase a).toList = { toList := l }.toList.erase a

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isNIndepSet_compl : Gᶜ.IsNIndepSet n s ↔ G.IsNClique n s

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNIndepSet n s ↔ G.IsNClique n s

Tactic:
rw [isNClique_iff]

Result:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNIndepSet n s ↔ G.IsClique ↑s ∧ #s = n

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ Gᶜ.IsNIndepSet n s ↔ G.IsClique ↑s ∧ #s = n

Tactic:
simp [isNIndepSet_iff]

Result:
no goals