harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = True) (h₂ : q (of_eq_true h₁) = q') : (∀ hp : p, q hp) = q'

Proof state:
case a.mp
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
h' : ∀ (hp : p), q hp
⊢ q'

Tactic:
exact Eq.mp h₂ (h' (of_eq_true h₁))

Result:
no goals

Proof state:
case a.mpr
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
h' : q'
hp✝ : p
⊢ q hp✝

Tactic:
exact Eq.mpr h₂ h'

Result:
no goals

Proof state:
case a
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
⊢ (∀ (hp : p), q hp) ↔ q'

Tactic:
apply Iff.intro

Result:
case a.mp
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
⊢ (∀ (hp : p), q hp) → q'

case a.mpr
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
⊢ q' → ∀ (hp : p), q hp

Proof state:
case a.mpr
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
⊢ q' → ∀ (hp : p), q hp

Tactic:
intro h'

Result:
case a.mpr
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
h' : q'
⊢ ∀ (hp : p), q hp

Proof state:
case a.mpr
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
h' : q'
⊢ ∀ (hp : p), q hp

Tactic:
intros

Result:
case a.mpr
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
h' : q'
hp✝ : p
⊢ q hp✝

Proof state:
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
⊢ (∀ (hp : p), q hp) = q'

Tactic:
apply propext

Result:
case a
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
⊢ (∀ (hp : p), q hp) ↔ q'

Proof state:
case a.mp
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
⊢ (∀ (hp : p), q hp) → q'

Tactic:
intro h'

Result:
case a.mp
p : Prop
q : p → Prop
q' : Prop
h₁ : p = True
h₂ : q ⋯ = q'
h' : ∀ (hp : p), q hp
⊢ q'
-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem Abelian.tfae_epi {X Y : C} (f : X ⟶ Y) (Z : C ) :
    TFAE [Epi f, cokernel.π f = 0, (ShortComplex.mk f (0 : Y ⟶ Z) comp_zero).Exact]

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
x✝ : Epi f
⊢ cokernel.π f = 0

Tactic:
rw [← cancel_epi f, cokernel.condition, comp_zero]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
⊢ [Epi f, cokernel.π f = 0, (ShortComplex.mk f 0 ⋯).Exact].TFAE

Tactic:
tfae_have 1 → 2
| _ => by rw [← cancel_epi f, cokernel.condition, comp_zero]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
tfae_1_to_2 : Epi f → cokernel.π f = 0
⊢ [Epi f, cokernel.π f = 0, (ShortComplex.mk f 0 ⋯).Exact].TFAE

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
tfae_1_to_2 : Epi f → cokernel.π f = 0
⊢ [Epi f, cokernel.π f = 0, (ShortComplex.mk f 0 ⋯).Exact].TFAE

Tactic:
tfae_have 3 ↔ 1 := ShortComplex.exact_iff_epi _ (by simp)

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
tfae_1_to_2 : Epi f → cokernel.π f = 0
tfae_3_iff_1 : (ShortComplex.mk f 0 ⋯).Exact ↔ Epi f
⊢ [Epi f, cokernel.π f = 0, (ShortComplex.mk f 0 ⋯).Exact].TFAE

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
⊢ [Epi f, cokernel.π f = 0, (ShortComplex.mk f 0 ⋯).Exact].TFAE

Tactic:
tfae_have 2 → 1 := epi_of_cokernel_π_eq_zero _

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
⊢ [Epi f, cokernel.π f = 0, (ShortComplex.mk f 0 ⋯).Exact].TFAE

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
tfae_1_to_2 : Epi f → cokernel.π f = 0
tfae_3_iff_1 : (ShortComplex.mk f 0 ⋯).Exact ↔ Epi f
⊢ [Epi f, cokernel.π f = 0, (ShortComplex.mk f 0 ⋯).Exact].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
tfae_1_to_2 : Epi f → cokernel.π f = 0
⊢ (ShortComplex.mk f 0 ⋯).g = 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem BilinMap.isSymm_iff_eq_flip {N : Type*} [AddCommMonoid N] [Module R N]
    {B : LinearMap.BilinMap R M N} : (∀ x y, B x y = B y x) ↔ B = B.flip

Proof state:
R : Type u_1
M : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_20
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
B : LinearMap.BilinMap R M N
⊢ (∀ (x y : M), (B x) y = (B y) x) ↔ B = flip B

Tactic:
simp [LinearMap.ext_iff₂]

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
lemma eval_image_piFinset_const {β} [DecidableEq β] (t : Finset β) (a : α) :
    ((piFinset fun _i : α ↦ t).image fun f ↦ f a) = t

Proof state:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
this : Nonempty α
⊢ image (fun f => f a) (piFinset fun _i => ∅) = ∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
⊢ image (fun f => f a) (piFinset fun _i => t) = t

Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty

Result:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
⊢ image (fun f => f a) (piFinset fun _i => ∅) = ∅

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun f => f a) (piFinset fun _i => t) = t

Proof state:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun f => f a) (piFinset fun _i => t) = t

Tactic:
exact eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
⊢ image (fun f => f a) (piFinset fun _i => ∅) = ∅

Tactic:
haveI : Nonempty α := ⟨a⟩

Result:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
this : Nonempty α
⊢ image (fun f => f a) (piFinset fun _i => ∅) = ∅
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_eq_zero_iff_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : Integrable f μ) :
    ∫ x, f x ∂μ = 0 ↔ f =ᵐ[μ] 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ AEMeasurable (fun a => ENNReal.ofReal (f a)) μ

Tactic:
exact (ENNReal.measurable_ofReal.comp_aemeasurable hfi.1.aemeasurable)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ (∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x) = 0 x) ↔ ∀ᵐ (x : α) ∂μ, f x ≤ 0 x

Tactic:
simp only [Pi.zero_apply, ofReal_eq_zero]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ (fun a => ENNReal.ofReal (f a)) =ᶠ[ae μ] 0 ↔ f =ᶠ[ae μ] 0

Tactic:
rw [← hf.le_iff_eq, Filter.EventuallyEq, Filter.EventuallyLE]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ (∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x) = 0 x) ↔ ∀ᵐ (x : α) ∂μ, f x ≤ 0 x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
rw [lintegral_eq_zero_iff']

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ (fun a => ENNReal.ofReal (f a)) =ᶠ[ae μ] 0 ↔ f =ᶠ[ae μ] 0

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ AEMeasurable (fun a => ENNReal.ofReal (f a)) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ ∫ (x : α), f x ∂μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
simp_rw [integral_eq_lintegral_of_nonneg_ae hf hfi.1, ENNReal.toReal_eq_zero_iff,
  ← ENNReal.not_lt_top, ← hasFiniteIntegral_iff_ofReal hf, hfi.2, not_true_eq_false, or_false]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = 0 ↔ f =ᶠ[ae μ] 0
-- Mathlib/Data/Finsupp/AList.lean
theorem singleton_lookupFinsupp (a : α) (m : M) :
    (singleton a m).lookupFinsupp = Finsupp.single a m

Proof state:
α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
⊢ (singleton a m).lookupFinsupp = Finsupp.single a m

Tactic:
simp [← AList.insert_empty]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
⊢ (singleton a m).lookupFinsupp = Finsupp.single a m

Tactic:
classical
simp [← AList.insert_empty]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem split_apply (i : ι) (x : αs i) : split l i x = l ⟨i, x⟩

Proof state:
ι : Type u_4
M : Type u_5
αs : ι → Type u_13
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
x : αs i
⊢ (l.split i) x = l ⟨i, x⟩

Tactic:
dsimp only [split]

Result:
ι : Type u_4
M : Type u_5
αs : ι → Type u_13
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
x : αs i
⊢ (comapDomain (Sigma.mk i) l ⋯) x = l ⟨i, x⟩

Proof state:
ι : Type u_4
M : Type u_5
αs : ι → Type u_13
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
x : αs i
⊢ (comapDomain (Sigma.mk i) l ⋯) x = l ⟨i, x⟩

Tactic:
rw [comapDomain_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
@[simp]
lemma Basis.baseChange_repr_tmul (b : Basis ι R M) (x y i) :
    (b.baseChange S).repr (x ⊗ₜ y) i = b.repr y i • x

Proof state:
R : Type u_1
M : Type u_3
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_7
inst✝¹ : Semiring S
inst✝ : Algebra R S
b : Basis ι R M
x : S
y : M
i : ι
⊢ ((baseChange S b).repr (x ⊗ₜ[R] y)) i = (b.repr y) i • x

Tactic:
simp [Basis.baseChange, Basis.tensorProduct]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem edist_inequality (hf : ContractingWith K f) {x y} (h : edist x y ≠ ∞) :
    edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - K) :=
  suffices edist x y ≤ edist x (f x) + edist y (f y) + K * edist x y by
    rwa [ENNReal.le_div_iff_mul_le (Or.inl hf.one_sub_K_ne_zero) (Or.inl one_sub_K_ne_top),
      mul_comm, ENNReal.sub_mul fun _ _ ↦ h, one_mul, tsub_le_iff_right]
  calc
    edist x y ≤ edist x (f x) + edist (f x) (f y) + edist (f y) y := edist_triangle4 _ _ _ _
    _ = edist x (f x) + edist y (f y) + edist (f x) (f y)

Proof state:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ⊤
this : edist x y ≤ edist x (f x) + edist y (f y) + ↑K * edist x y
⊢ edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - ↑K)

Tactic:
rwa [ENNReal.le_div_iff_mul_le (Or.inl hf.one_sub_K_ne_zero) (Or.inl one_sub_K_ne_top),
  mul_comm, ENNReal.sub_mul fun _ _ ↦ h, one_mul, tsub_le_iff_right]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ⊤
⊢ edist x (f x) + edist (f x) (f y) + edist (f y) y = edist x (f x) + edist y (f y) + edist (f x) (f y)

Tactic:
rw [edist_comm y, add_right_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₂_of_isCharTwoJNeZeroNF_of_char_two : W.b₂ = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 1 + 4 * W.a₂ = 1

Tactic:
linear_combination 2 * W.a₂ * CharP.cast_eq_zero R 2

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.b₂ = 1

Tactic:
rw [b₂_of_isCharTwoJNeZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 1 + 4 * W.a₂ = 1
-- Mathlib/GroupTheory/QuotientGroup/Defs.lean
theorem ker_le_range_iff {I : Type w} [Group I] (f : G →* H) [f.range.Normal] (g : H →* I) :
    g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 1 :=
  ⟨fun h => MonoidHom.ext fun ⟨_, hx⟩ => (eq_one_iff _).mpr <| h hx,
    fun h x hx => (eq_one_iff _).mp <| by exact DFunLike.congr_fun h ⟨x, hx⟩⟩

Proof state:
G : Type u
inst✝³ : Group G
H : Type v
inst✝² : Group H
I : Type w
inst✝¹ : Group I
f : G →* H
inst✝ : f.range.Normal
g : H →* I
h : (mk' f.range).comp g.ker.subtype = 1
x : H
hx : x ∈ g.ker
⊢ ↑x = 1

Tactic:
exact DFunLike.congr_fun h ⟨x, hx⟩

Result:
no goals
-- Mathlib/Probability/CondVar.lean
lemma condVar_bot_ae_eq (X : Ω → ℝ) :
    Var[X; μ | ⊥] =ᵐ[μ] fun _ ↦ ⨍ ω, (X ω - ⨍ ω', X ω' ∂μ) ^ 2 ∂μ

Proof state:
case inl
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ Var[X; 0 | ⊥] =ᶠ[⊥] fun x => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂0) ^ 2 ∂0

Tactic:
exact eventually_bot

Result:
no goals

Proof state:
case inr
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hμ : NeZero μ
⊢ Var[X; μ | ⊥] =ᶠ[ae μ] fun x => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂μ) ^ 2 ∂μ

Tactic:
exact .of_forall <| congr_fun (condVar_bot' X)

Result:
no goals

Proof state:
case inl
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ Var[X; 0 | ⊥] =ᶠ[ae 0] fun x => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂0) ^ 2 ∂0

Tactic:
rw [ae_zero]

Result:
case inl
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ Var[X; 0 | ⊥] =ᶠ[⊥] fun x => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂0) ^ 2 ∂0

Proof state:
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
⊢ Var[X; μ | ⊥] =ᶠ[ae μ] fun x => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂μ) ^ 2 ∂μ

Tactic:
obtain rfl | hμ := eq_zero_or_neZero μ

Result:
case inl
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ Var[X; 0 | ⊥] =ᶠ[ae 0] fun x => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂0) ^ 2 ∂0

case inr
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hμ : NeZero μ
⊢ Var[X; μ | ⊥] =ᶠ[ae μ] fun x => ⨍ (ω : Ω), (X ω - ⨍ (ω' : Ω), X ω' ∂μ) ^ 2 ∂μ
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem partition_eq_of_isConj {σ τ : Perm α} : IsConj σ τ ↔ σ.partition = τ.partition

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ σ.cycleType = τ.cycleType ↔ σ.partition = τ.partition

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.partition = τ.partition

case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.partition = τ.partition
⊢ σ.cycleType = τ.cycleType

Proof state:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.partition = τ.partition

Tactic:
rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
  h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ IsConj σ τ ↔ σ.partition = τ.partition

Tactic:
rw [isConj_iff_cycleType_eq]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ σ.cycleType = τ.cycleType ↔ σ.partition = τ.partition

Proof state:
case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.partition = τ.partition
⊢ σ.cycleType = τ.cycleType

Tactic:
rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_target_mem_nhds [I.Boundaryless] (x : M) :
    (extChartAt I x).target ∈ 𝓝 (extChartAt I x x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ (extChartAt I x).target ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
convert extChartAt_target_mem_nhdsWithin x

Result:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ 𝓝 (↑(extChartAt I x) x) = 𝓝[range ↑I] ↑(extChartAt I x) x

Proof state:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ 𝓝 (↑(extChartAt I x) x) = 𝓝[range ↑I] ↑(extChartAt I x) x

Tactic:
simp only [I.range_eq_univ, nhdsWithin_univ]

Result:
no goals
-- Mathlib/Data/Nat/WithBot.lean
theorem add_one_le_of_lt {n m : WithBot ℕ} (h : n < m) : n + 1 ≤ m

Proof state:
case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ < ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝

Tactic:
rwa [WithBot.coe_lt_coe, ← Nat.add_one_le_iff, ← WithBot.coe_le_coe, WithBot.coe_add,
  WithBot.coe_one] at h

Result:
no goals

Proof state:
case coe.bot
a✝ : ℕ
h : ↑a✝ < ⊥
⊢ ↑a✝ + 1 ≤ ⊥

Tactic:
exact (not_lt_bot h).elim

Result:
no goals

Proof state:
n m : WithBot ℕ
h : n < m
⊢ n + 1 ≤ m

Tactic:
cases n

Result:
case bot
m : WithBot ℕ
h : ⊥ < m
⊢ ⊥ + 1 ≤ m

case coe
m : WithBot ℕ
a✝ : ℕ
h : ↑a✝ < m
⊢ ↑a✝ + 1 ≤ m

Proof state:
case coe
m : WithBot ℕ
a✝ : ℕ
h : ↑a✝ < m
⊢ ↑a✝ + 1 ≤ m

Tactic:
cases m

Result:
case coe.bot
a✝ : ℕ
h : ↑a✝ < ⊥
⊢ ↑a✝ + 1 ≤ ⊥

case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ < ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝

Proof state:
case bot
m : WithBot ℕ
h : ⊥ < m
⊢ ⊥ + 1 ≤ m

Tactic:
simp only [WithBot.bot_add, bot_le]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
lemma not_ne_self : ∀ b : Bool, (!b) ≠ b

Proof state:
⊢ ∀ (b : Bool), (!b) ≠ b

Tactic:
decide

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem even_odd {a : ℤ} {b : ℕ} (ha2 : a % 2 = 0) (hb2 : b % 2 = 1) :
    (if b % 8 = 3 ∨ b % 8 = 5 then -J(a / 2 | b) else J(a / 2 | b)) = J(a | b)

Proof state:
case intro
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(2 * a / 2 | b) else J(2 * a / 2 | b)) = J(2 * a | b)

Tactic:
rw [Int.mul_ediv_cancel_left _ (by decide), jacobiSym.mul_left,
  jacobiSym.at_two (Nat.odd_iff.mpr hb2), ZMod.χ₈_nat_eq_if_mod_eight,
  if_neg (Nat.mod_two_ne_zero.mpr hb2)]

Result:
case intro
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = (if b % 8 = 1 ∨ b % 8 = 7 then 1 else -1) * J(a | b)

Proof state:
case intro
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = (if b % 8 = 1 ∨ b % 8 = 7 then 1 else -1) * J(a | b)

Tactic:
have := Nat.mod_lt b (by decide : 0 < 8)

Result:
case intro
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
this : b % 8 < 8
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = (if b % 8 = 1 ∨ b % 8 = 7 then 1 else -1) * J(a | b)

Proof state:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ 2 ≠ 0

Tactic:
decide

Result:
no goals

Proof state:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ 0 < 8

Tactic:
decide

Result:
no goals

Proof state:
case intro.«6»
b : ℕ
hb2 : b % 2 = 1
a : ℤ
h : b % 8 = 6
this : 6 % 2 = 1
⊢ J(a | b) = -J(a | b)

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.«6»
b : ℕ
hb2 : b % 2 = 1
a : ℤ
h : b % 8 = 6
⊢ J(a | b) = -J(a | b)

Tactic:
have := hb2 ▸ h ▸ Nat.mod_mod_of_dvd b (by decide : 2 ∣ 8)

Result:
case intro.«6»
b : ℕ
hb2 : b % 2 = 1
a : ℤ
h : b % 8 = 6
this : 6 % 2 = 1
⊢ J(a | b) = -J(a | b)

Proof state:
a : ℤ
b : ℕ
ha2 : a % 2 = 0
hb2 : b % 2 = 1
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a / 2 | b) else J(a / 2 | b)) = J(a | b)

Tactic:
obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha2

Result:
case intro
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(2 * a / 2 | b) else J(2 * a / 2 | b)) = J(2 * a | b)

Proof state:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
h : b % 8 = 6
⊢ 2 ∣ 8

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem orElse_none (x : Option α) : (x <|> none) = x

Proof state:
α : Type u_1
x : Option α
⊢ (x <|> none) = x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem Prime.prod_properDivisors {α : Type*} [CommMonoid α] {p : ℕ} {f : ℕ → α} (h : p.Prime) :
    ∏ x ∈ p.properDivisors, f x = f 1

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ p.properDivisors, f x = f 1

Tactic:
simp [h.properDivisors]

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem HasLineDerivWithinAt.mono_of_mem_nhdsWithin
    (h : HasLineDerivWithinAt 𝕜 f f' t x v) (hst : t ∈ 𝓝[s] x) :
    HasLineDerivWithinAt 𝕜 f f' s x v

Proof state:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ Continuous fun t => x + t • v

Tactic:
fun_prop

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ (fun t => x + t • v) ⁻¹' t ∈ 𝓝[(fun t => x + t • v) ⁻¹' s] 0

Tactic:
apply ContinuousWithinAt.preimage_mem_nhdsWithin'' _ hst (by simp)

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ ContinuousWithinAt (fun t => x + t • v) ((fun t => x + t • v) ⁻¹' s) 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ ContinuousWithinAt (fun t => x + t • v) ((fun t => x + t • v) ⁻¹' s) 0

Tactic:
apply Continuous.continuousWithinAt

Result:
case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ Continuous fun t => x + t • v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ x = x + 0 • v

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ HasLineDerivWithinAt 𝕜 f f' s x v

Tactic:
apply HasDerivWithinAt.mono_of_mem_nhdsWithin h

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' t x v
hst : t ∈ 𝓝[s] x
⊢ (fun t => x + t • v) ⁻¹' t ∈ 𝓝[(fun t => x + t • v) ⁻¹' s] 0