harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Count.lean
theorem count_eq_card_filter_range (n : ℕ) : count p n = #{x ∈ range n | p x}

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = #(filter (fun x => p x) (range n))

Tactic:
rw [count, List.countP_eq_length_filter]

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (List.filter (fun b => decide (p b)) (List.range n)).length = #(filter (fun x => p x) (range n))

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ (List.filter (fun b => decide (p b)) (List.range n)).length = #(filter (fun x => p x) (range n))

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma AnalyticAt.pi (hf : ∀ i, AnalyticAt 𝕜 (f i) e) :
    AnalyticAt 𝕜 (fun x ↦ (f · x)) e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
hf : ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e
⊢ AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) Set.univ e

Tactic:
exact AnalyticWithinAt.pi hf

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
hf : ∀ (i : ι), AnalyticAt 𝕜 (f i) e
⊢ AnalyticAt 𝕜 (fun x x_1 => f x_1 x) e

Tactic:
simp_rw [← analyticWithinAt_univ] at hf ⊢

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
hf : ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e
⊢ AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) Set.univ e
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem toShortNFOfCharThree_spec (hb₂ : W.b₂ = 0) :
    (W.variableChange W.toShortNFOfCharThree).IsShortNF

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
hb₂ : W.b₂ = 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
H : (W.variableChange W.toCharNeTwoNF).IsCharNeTwoNF
⊢ (W.variableChange W.toShortNFOfCharThree).IsShortNF

Tactic:
exact ⟨H.a₁, hb₂ ▸ W.toShortNFOfCharThree_a₂, H.a₃⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
hb₂ : W.b₂ = 0
⊢ (W.variableChange W.toShortNFOfCharThree).IsShortNF

Tactic:
have h : (2 : R) * 2 = 1 := by linear_combination CharP.cast_eq_zero R 3

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
hb₂ : W.b₂ = 0
h : 2 * 2 = 1
⊢ (W.variableChange W.toShortNFOfCharThree).IsShortNF

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
hb₂ : W.b₂ = 0
⊢ 2 * 2 = 1

Tactic:
linear_combination CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
hb₂ : W.b₂ = 0
h : 2 * 2 = 1
⊢ (W.variableChange W.toShortNFOfCharThree).IsShortNF

Tactic:
letI : Invertible (2 : R) := ⟨2, h, h⟩

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
hb₂ : W.b₂ = 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ (W.variableChange W.toShortNFOfCharThree).IsShortNF

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
hb₂ : W.b₂ = 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ (W.variableChange W.toShortNFOfCharThree).IsShortNF

Tactic:
have H := W.toCharNeTwoNF_spec

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
hb₂ : W.b₂ = 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
H : (W.variableChange W.toCharNeTwoNF).IsCharNeTwoNF
⊢ (W.variableChange W.toShortNFOfCharThree).IsShortNF
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
lemma comp_assoc {a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ} (α : Ext X Y a₁) (β : Ext Y Z a₂) (γ : Ext Z T a₃)
    (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h : a₁ + a₂ + a₃ = a) :
    (α.comp β h₁₂).comp γ (show a₁₂ + a₃ = a by omega) =
      α.comp (β.comp γ h₂₃) (by omega) :=
  SmallShiftedHom.comp_assoc _ _ _ _ _ _ (by omega)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ a₁₂ + a₃ = a

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ a₁ + a₂₃ = a

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ ↑a₃ + ↑a₂ + ↑a₁ = ↑a

Tactic:
omega

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem exists_unitSMul_mem_integerSet {x : mixedSpace K} (hx : x ≠ 0)
    (hx' : x ∈ mixedEmbedding K '' (Set.range (algebraMap (𝓞 K) K))) :
    ∃ u : (𝓞 K)ˣ, u • x ∈ integerSet K

Proof state:
case intro.intro.intro.intro.refl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) x)) ≠ 0
hu : u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ fundamentalCone K
⊢ ∃ u, u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ integerSet K

Tactic:
exact ⟨u, mem_integerSet.mpr ⟨hu, u * x, by simp_rw [unitSMul_smul, ← map_mul]⟩⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) x)) ≠ 0
hu : u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ fundamentalCone K
⊢ (mixedEmbedding K) ↑(↑u * x) = u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x)

Tactic:
simp_rw [unitSMul_smul, ← map_mul]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ≠ 0
hx' : x ∈ ⇑(mixedEmbedding K) '' Set.range ⇑(algebraMap (𝓞 K) K)
⊢ ∃ u, u • x ∈ integerSet K

Tactic:
replace hx : mixedEmbedding.norm x ≠ 0 :=
    (norm_eq_zero_iff' (Set.mem_range_of_mem_image (mixedEmbedding K) _ hx')).not.mpr hx

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx' : x ∈ ⇑(mixedEmbedding K) '' Set.range ⇑(algebraMap (𝓞 K) K)
hx : mixedEmbedding.norm x ≠ 0
⊢ ∃ u, u • x ∈ integerSet K

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx' : x ∈ ⇑(mixedEmbedding K) '' Set.range ⇑(algebraMap (𝓞 K) K)
hx : mixedEmbedding.norm x ≠ 0
u : (𝓞 K)ˣ
hu : u • x ∈ fundamentalCone K
⊢ ∃ u, u • x ∈ integerSet K

Tactic:
obtain ⟨_, ⟨x, rfl⟩, _, rfl⟩ := hx'

Result:
case intro.intro.intro.intro.refl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) x)) ≠ 0
hu : u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ fundamentalCone K
⊢ ∃ u, u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ integerSet K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx' : x ∈ ⇑(mixedEmbedding K) '' Set.range ⇑(algebraMap (𝓞 K) K)
hx : mixedEmbedding.norm x ≠ 0
⊢ ∃ u, u • x ∈ integerSet K

Tactic:
obtain ⟨u, hu⟩ := exists_unit_smul_mem hx

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx' : x ∈ ⇑(mixedEmbedding K) '' Set.range ⇑(algebraMap (𝓞 K) K)
hx : mixedEmbedding.norm x ≠ 0
u : (𝓞 K)ˣ
hu : u • x ∈ fundamentalCone K
⊢ ∃ u, u • x ∈ integerSet K
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem le_arcsin_iff_sin_le {x y : ℝ} (hx : x ∈ Icc (-(π / 2)) (π / 2)) (hy : y ∈ Icc (-1 : ℝ) 1) :
    x ≤ arcsin y ↔ sin x ≤ y

Proof state:
x y : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
hy : y ∈ Icc (-1) 1
⊢ x ≤ arcsin y ↔ sin x ≤ y

Tactic:
rw [← neg_le_neg_iff, ← arcsin_neg,
  arcsin_le_iff_le_sin ⟨neg_le_neg hy.2, neg_le.2 hy.1⟩ ⟨neg_le_neg hx.2, neg_le.2 hx.1⟩, sin_neg,
  neg_le_neg_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
@[simp] lemma qaryEntropy_zero (q : ℕ) : qaryEntropy q 0 = 0

Proof state:
q : ℕ
⊢ qaryEntropy q 0 = 0

Tactic:
simp [qaryEntropy]

Result:
no goals
-- Mathlib/Computability/Reduce.lean
theorem computable_of_manyOneReducible {p : α → Prop} {q : β → Prop} (h₁ : p ≤₀ q)
    (h₂ : ComputablePred q) : ComputablePred p

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ Computable fun a => decide ((fun a => (fun a => g a = true) (f a)) a)

Tactic:
simpa using hg.comp c

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ DecidablePred fun a => (fun a => g a = true) (f a)

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₁ : p ≤₀ q
h₂ : ComputablePred q
⊢ ComputablePred p

Tactic:
rcases h₁ with ⟨f, c, hf⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred p

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred p

Tactic:
rw [show p = fun a => q (f a) from Set.ext hf]

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred fun a => q (f a)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred fun a => q (f a)

Tactic:
rcases computable_iff.1 h₂ with ⟨g, hg, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ ComputablePred fun a => (fun a => g a = true) (f a)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ ComputablePred fun a => (fun a => g a = true) (f a)

Tactic:
exact ⟨by infer_instance, by simpa using hg.comp c⟩

Result:
no goals
-- Mathlib/NumberTheory/ZetaValues.lean
theorem bernoulliFun_eval_zero (k : ℕ) : bernoulliFun k 0 = bernoulli k

Proof state:
k : ℕ
⊢ bernoulliFun k 0 = ↑(bernoulli k)

Tactic:
rw [bernoulliFun, Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Exp.lean
lemma Function.Periodic.norm_qParam_le_of_one_half_le_im {ξ : ℂ} (hξ : 1 / 2 ≤ ξ.im) :
    ‖𝕢 1 ξ‖ ≤ rexp (-π)

Proof state:
ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)

Tactic:
rwa [Periodic.qParam, ofReal_one, div_one, Complex.norm_exp, Real.exp_le_exp,
  mul_right_comm, mul_I_re, neg_le_neg_iff, ← ofReal_ofNat, ← ofReal_mul, im_ofReal_mul,
  mul_comm _ π, mul_assoc, le_mul_iff_one_le_right Real.pi_pos, ← div_le_iff₀' two_pos]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_withDensity_iff_integrable_smul' {f : α → ℝ≥0∞} (hf : Measurable f)
    (hflt : ∀ᵐ x ∂μ, f x < ∞) {g : α → E} :
    Integrable g (μ.withDensity f) ↔ Integrable (fun x => (f x).toReal • g x) μ

Proof state:
case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ Measurable fun x => (f x).toNNReal

Tactic:
exact hf.ennreal_toNNReal

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x => (f x).toReal • g x) μ

Tactic:
rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
  integrable_withDensity_iff_integrable_smul]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ Integrable (fun x => (f x).toNNReal • g x) μ ↔ Integrable (fun x => (f x).toReal • g x) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ Measurable fun x => (f x).toNNReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → E
⊢ Integrable (fun x => (f x).toNNReal • g x) μ ↔ Integrable (fun x => (f x).toReal • g x) μ

Tactic:
simp_rw [NNReal.smul_def, ENNReal.toReal]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
theorem turanGraph_cliqueFree (hr : 0 < r) : (turanGraph n r).CliqueFree (r + 1)

Proof state:
case intro.mk
n r : ℕ
hr : 0 < r
f : Fin (r + 1) ↪ Fin n
ha : ∀ {a b : Fin (r + 1)}, (turanGraph n r).Adj (f a) (f b) ↔ ⊤.Adj a b
⊢ False

Tactic:
simp only [turanGraph, top_adj] at ha

Result:
case intro.mk
n r : ℕ
hr : 0 < r
f : Fin (r + 1) ↪ Fin n
ha : ∀ {a b : Fin (r + 1)}, ↑(f a) % r ≠ ↑(f b) % r ↔ a ≠ b
⊢ False

Proof state:
n r : ℕ
hr : 0 < r
h : Nonempty (⊤ ↪g turanGraph n r)
⊢ False

Tactic:
obtain ⟨f, ha⟩ := h

Result:
case intro.mk
n r : ℕ
hr : 0 < r
f : Fin (r + 1) ↪ Fin n
ha : ∀ {a b : Fin (r + 1)}, (turanGraph n r).Adj (f a) (f b) ↔ ⊤.Adj a b
⊢ False

Proof state:
case intro.mk
n r : ℕ
hr : 0 < r
f : Fin (r + 1) ↪ Fin n
ha : ∀ {a b : Fin (r + 1)}, ↑(f a) % r ≠ ↑(f b) % r ↔ a ≠ b
⊢ False

Tactic:
obtain ⟨x, y, d, c⟩ := Fintype.exists_ne_map_eq_of_card_lt (fun x ↦
  (⟨(f x).1 % r, Nat.mod_lt _ hr⟩ : Fin r)) (by simp)

Result:
case intro.mk.intro.intro.intro
n r : ℕ
hr : 0 < r
f : Fin (r + 1) ↪ Fin n
ha : ∀ {a b : Fin (r + 1)}, ↑(f a) % r ≠ ↑(f b) % r ↔ a ≠ b
x y : Fin (r + 1)
d : x ≠ y
c : ⟨↑(f x) % r, ⋯⟩ = ⟨↑(f y) % r, ⋯⟩
⊢ False

Proof state:
n r : ℕ
hr : 0 < r
h : ¬IsEmpty (⊤ ↪g turanGraph n r)
⊢ False

Tactic:
rw [not_isEmpty_iff] at h

Result:
n r : ℕ
hr : 0 < r
h : Nonempty (⊤ ↪g turanGraph n r)
⊢ False

Proof state:
n r : ℕ
hr : 0 < r
⊢ (turanGraph n r).CliqueFree (r + 1)

Tactic:
rw [cliqueFree_iff]

Result:
n r : ℕ
hr : 0 < r
⊢ IsEmpty (⊤ ↪g turanGraph n r)

Proof state:
case intro.mk.intro.intro.intro
n r : ℕ
hr : 0 < r
f : Fin (r + 1) ↪ Fin n
ha : ∀ {a b : Fin (r + 1)}, ↑(f a) % r ≠ ↑(f b) % r ↔ a ≠ b
x y : Fin (r + 1)
d : x ≠ y
c : ⟨↑(f x) % r, ⋯⟩ = ⟨↑(f y) % r, ⋯⟩
⊢ False

Tactic:
simp only [Fin.mk.injEq] at c

Result:
case intro.mk.intro.intro.intro
n r : ℕ
hr : 0 < r
f : Fin (r + 1) ↪ Fin n
ha : ∀ {a b : Fin (r + 1)}, ↑(f a) % r ≠ ↑(f b) % r ↔ a ≠ b
x y : Fin (r + 1)
d : x ≠ y
c : ↑(f x) % r = ↑(f y) % r
⊢ False

Proof state:
n r : ℕ
hr : 0 < r
f : Fin (r + 1) ↪ Fin n
ha : ∀ {a b : Fin (r + 1)}, ↑(f a) % r ≠ ↑(f b) % r ↔ a ≠ b
⊢ Fintype.card (Fin r) < Fintype.card (Fin (r + 1))

Tactic:
simp

Result:
no goals

Proof state:
case intro.mk.intro.intro.intro
n r : ℕ
hr : 0 < r
f : Fin (r + 1) ↪ Fin n
ha : ∀ {a b : Fin (r + 1)}, ↑(f a) % r ≠ ↑(f b) % r ↔ a ≠ b
x y : Fin (r + 1)
d : x ≠ y
c : ↑(f x) % r = ↑(f y) % r
⊢ False

Tactic:
exact absurd c ((@ha x y).mpr d)

Result:
no goals

Proof state:
n r : ℕ
hr : 0 < r
⊢ IsEmpty (⊤ ↪g turanGraph n r)

Tactic:
by_contra h

Result:
n r : ℕ
hr : 0 < r
h : ¬IsEmpty (⊤ ↪g turanGraph n r)
⊢ False
-- Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean
@[reassoc]
lemma mappingConeCompHomotopyEquiv_comm₁ :
    inr (map f (f ≫ g) (𝟙 X₁) g (by rw [id_comp])) ≫
      (mappingConeCompHomotopyEquiv f g).inv = (mappingConeCompTriangle f g).mor₂

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ inr (map f (f ≫ g) (𝟙 X₁) g ⋯) ≫ (mappingConeCompHomotopyEquiv f g).inv = (mappingConeCompTriangle f g).mor₂

Tactic:
simp [map, mappingConeCompHomotopyEquiv, MappingConeCompHomotopyEquiv.inv]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{?u.213487, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ f ≫ g = 𝟙 X₁ ≫ f ≫ g

Tactic:
rw [id_comp]

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem range_pullback_snd_of_left :
    Set.range (pullback.snd f g).base = (g ⁻¹ᵁ f.opensRange).1

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g).base) = (g ⁻¹ᵁ Scheme.Hom.opensRange f).carrier

Tactic:
rw [← show _ = (pullback.snd f g).base from
  PreservesPullback.iso_hom_snd Scheme.forgetToTop f g, TopCat.coe_comp, Set.range_comp,
  Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.fst f.base g.base)]

Result:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) ''
      (⇑(ConcreteCategory.hom (pullback.fst f.base g.base)) ⁻¹' Set.univ) =
    (g ⁻¹ᵁ Scheme.Hom.opensRange f).carrier

X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop f g).hom)

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop f g).hom

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop f g).hom)

Tactic:
rw [← TopCat.epi_iff_surjective]

Result:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop f g).hom

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) ''
      (⇑(ConcreteCategory.hom (pullback.fst f.base g.base)) ⁻¹' Set.univ) =
    (g ⁻¹ᵁ Scheme.Hom.opensRange f).carrier

Tactic:
erw [TopCat.pullback_snd_image_fst_preimage]

Result:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹'
      (⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) '' Set.univ) =
    (g ⁻¹ᵁ Scheme.Hom.opensRange f).carrier

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹'
      (⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) '' Set.univ) =
    (g ⁻¹ᵁ Scheme.Hom.opensRange f).carrier

Tactic:
rw [Set.image_univ]

Result:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) =
    (g ⁻¹ᵁ Scheme.Hom.opensRange f).carrier

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) =
    (g ⁻¹ᵁ Scheme.Hom.opensRange f).carrier

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomologySequenceLemmas.lean
lemma mono_homologyMap_τ₃ (i : ι)
    (h₁ : Epi (homologyMap φ.τ₁ i))
    (h₂ : Mono (homologyMap φ.τ₂ i))
    (h₃ : ∀ j, c.Rel i j → Mono (homologyMap φ.τ₁ j)) :
    Mono (homologyMap φ.τ₃ i)

Proof state:
case pos.intro
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono (homologyMap φ.τ₃ i)

Tactic:
apply mono_of_epi_of_mono_of_mono
  ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))

Result:
case pos.intro.hR₁
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ ((δlastFunctor ⋙ δlastFunctor).obj (composableArrows₅ hS₁ i j hij)).Exact

case pos.intro.hR₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ ((δlastFunctor ⋙ δlastFunctor).obj (composableArrows₅ hS₂ i j hij)).Exact

case pos.intro.h₀
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Epi (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0 ⋯)

case pos.intro.h₁
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 1 ⋯)

case pos.intro.h₃
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3 ⋯)