harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Finset.ciInf_eq_min'_image {s : Finset ι} (h : ∃ x ∈ s, f x ≤ sInf ∅)
    (h' : (s.image f).Nonempty

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : autoParam (image f s).Nonempty _auto✝
⊢ ⨆ i ∈ s, OrderDual.toDual (f i) = (image (⇑OrderDual.toDual) (image f s)).max' ⋯

Tactic:
rw [ciSup_eq_max'_image _ h]

Result:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : autoParam (image f s).Nonempty _auto✝
⊢ (image (fun i => OrderDual.toDual (f i)) s).max' ⋯ = (image (⇑OrderDual.toDual) (image f s)).max' ⋯

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : autoParam (image f s).Nonempty _auto✝
⊢ ⨆ i, OrderDual.toDual (⨅ (_ : i ∈ s), f i) = (image (⇑OrderDual.toDual) (image f s)).max' ⋯

Tactic:
simp only [Function.comp_apply, toDual_iInf]

Result:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : autoParam (image f s).Nonempty _auto✝
⊢ ⨆ i ∈ s, OrderDual.toDual (f i) = (image (⇑OrderDual.toDual) (image f s)).max' ⋯

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : autoParam (image f s).Nonempty _auto✝
⊢ ⨅ i ∈ s, f i = (image f s).min' h'

Tactic:
rw [← OrderDual.toDual_inj, toDual_min', toDual_iInf]

Result:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : autoParam (image f s).Nonempty _auto✝
⊢ ⨆ i, OrderDual.toDual (⨅ (_ : i ∈ s), f i) = (image (⇑OrderDual.toDual) (image f s)).max' ⋯

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : autoParam (image f s).Nonempty _auto✝
⊢ ⨅ i ∈ s, f i = (image f s).min' h'

Tactic:
classical
rw [← OrderDual.toDual_inj, toDual_min', toDual_iInf]
simp only [Function.comp_apply, toDual_iInf]
rw [ciSup_eq_max'_image _ h]
simp only [image_image]
congr

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : autoParam (image f s).Nonempty _auto✝
⊢ (image (fun i => OrderDual.toDual (f i)) s).max' ⋯ = (image (⇑OrderDual.toDual) (image f s)).max' ⋯

Tactic:
simp only [image_image]

Result:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : autoParam (image f s).Nonempty _auto✝
⊢ (image (fun i => OrderDual.toDual (f i)) s).max' ⋯ = (image (⇑OrderDual.toDual ∘ f) s).max' ⋯

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : autoParam (image f s).Nonempty _auto✝
⊢ (image (fun i => OrderDual.toDual (f i)) s).max' ⋯ = (image (⇑OrderDual.toDual ∘ f) s).max' ⋯

Tactic:
congr

Result:
no goals
-- Mathlib/Analysis/Convex/Integral.lean
theorem ae_eq_const_or_norm_average_lt_of_norm_le_const [StrictConvexSpace ℝ E]
    (h_le : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ ‖⨍ x, f x ∂μ‖ < C

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

Tactic:
rcases le_or_lt C 0 with hC0 | hC0

Result:
case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : C ≤ 0
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

case inr
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
hμt : μ univ < ⊤
this : IsFiniteMeasure μ
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closedBall 0 C

Tactic:
simpa only [mem_closedBall_zero_iff]

Result:
no goals

Proof state:
case inr
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

Tactic:
by_cases hfi : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : ¬Integrable f μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem ker_eq_bot_of_cancel {f : M →ₛₗ[τ₁₂] M₂}
    (h : ∀ u v : ker f →ₗ[R] M, f.comp u = f.comp v → u = v) : ker f = ⊥

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥(ker f) →ₗ[R] M), f.comp u = f.comp v → u = v
h₁ : f.comp 0 = 0
⊢ range 0 = ⊥

Tactic:
exact range_zero

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥(ker f) →ₗ[R] M), f.comp u = f.comp v → u = v
⊢ ker f = ⊥

Tactic:
have h₁ : f.comp (0 : ker f →ₗ[R] M) = 0 := comp_zero _

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥(ker f) →ₗ[R] M), f.comp u = f.comp v → u = v
h₁ : f.comp 0 = 0
⊢ ker f = ⊥

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥(ker f) →ₗ[R] M), f.comp u = f.comp v → u = v
h₁ : f.comp 0 = 0
⊢ ker f = ⊥

Tactic:
rw [← Submodule.range_subtype (ker f),
  ← h 0 f.ker.subtype (Eq.trans h₁ (comp_ker_subtype f).symm)]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥(ker f) →ₗ[R] M), f.comp u = f.comp v → u = v
h₁ : f.comp 0 = 0
⊢ range 0 = ⊥
-- Mathlib/NumberTheory/FLT/Three.lean
theorem fermatLastTheoremThree : FermatLastTheoremFor 3

Proof state:
K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) ↑3 := IsCyclotomicExtension.zeta_spec 3 ℚ K
this : NumberField K
a b c : NumberField.RingOfIntegers K
u : (NumberField.RingOfIntegers K)ˣ
hc : c ≠ 0
ha : ¬hζ.toInteger - 1 ∣ a
hb : ¬hζ.toInteger - 1 ∣ b
hcdvd : hζ.toInteger - 1 ∣ c
coprime : IsCoprime a b
H : a ^ 3 + b ^ 3 = ↑u * c ^ 3
S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H }
⊢ False

Tactic:
obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'

Result:
case intro
K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) ↑3 := IsCyclotomicExtension.zeta_spec 3 ℚ K
this : NumberField K
a b c : NumberField.RingOfIntegers K
u : (NumberField.RingOfIntegers K)ˣ
hc : c ≠ 0
ha : ¬hζ.toInteger - 1 ∣ a
hb : ¬hζ.toInteger - 1 ∣ b
hcdvd : hζ.toInteger - 1 ∣ c
coprime : IsCoprime a b
H : a ^ 3 + b ^ 3 = ↑u * c ^ 3
S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H }
S : FermatLastTheoremForThreeGen.Solution hζ
⊢ False
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem exists_positive_of_not_mutuallySingular (μ ν : Measure α) [IsFiniteMeasure μ]
    [IsFiniteMeasure ν] (h : ¬ μ ⟂ₘ ν) :
    ∃ ε : ℝ≥0, 0 < ε ∧
      ∃ E : Set α, MeasurableSet E ∧ 0 < ν E
        ∧ ∀ A, MeasurableSet A → ε * ν (A ∩ E) ≤ μ (A ∩ E)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA : ℝ≥0
hA₃✝¹ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ν A
νA : ℝ≥0
hA₃✝ hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
c : ℝ≥0
hc : 0 < c
n : ℕ
hn : 1 / (↑n + 1) < ↑c * (↑νA)⁻¹
⊢ 0 < ↑νA

Tactic:
exact hb

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA : ℝ≥0
hA₃✝¹ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ν A
νA : ℝ≥0
hA₃✝ hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
⊢ ∀ (b : ℝ≥0), 0 < b → μA ≤ b

Tactic:
intro c hc

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA : ℝ≥0
hA₃✝¹ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ν A
νA : ℝ≥0
hA₃✝ hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
c : ℝ≥0
hc : 0 < c
⊢ μA ≤ c
-- Mathlib/Data/Finmap.lean
theorem AList.toFinmap_eq {s₁ s₂ : AList β} :
    toFinmap s₁ = toFinmap s₂ ↔ s₁.entries ~ s₂.entries

Proof state:
case mk
α : Type u
β : α → Type v
s₂ : AList β
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ = ⟦s₂⟧ ↔
    { entries := entries✝, nodupKeys := nodupKeys✝ }.entries ~ s₂.entries

Tactic:
cases s₂

Result:
case mk.mk
α : Type u
β : α → Type v
entries✝¹ : List (Sigma β)
nodupKeys✝¹ : entries✝¹.NodupKeys
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝¹, nodupKeys := nodupKeys✝¹ }⟧ = ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ ↔
    { entries := entries✝¹, nodupKeys := nodupKeys✝¹ }.entries ~
      { entries := entries✝, nodupKeys := nodupKeys✝ }.entries

Proof state:
case mk.mk
α : Type u
β : α → Type v
entries✝¹ : List (Sigma β)
nodupKeys✝¹ : entries✝¹.NodupKeys
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝¹, nodupKeys := nodupKeys✝¹ }⟧ = ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ ↔
    { entries := entries✝¹, nodupKeys := nodupKeys✝¹ }.entries ~
      { entries := entries✝, nodupKeys := nodupKeys✝ }.entries

Tactic:
simp [AList.toFinmap]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
s₁ s₂ : AList β
⊢ ⟦s₁⟧ = ⟦s₂⟧ ↔ s₁.entries ~ s₂.entries

Tactic:
cases s₁

Result:
case mk
α : Type u
β : α → Type v
s₂ : AList β
entries✝ : List (Sigma β)
nodupKeys✝ : entries✝.NodupKeys
⊢ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ = ⟦s₂⟧ ↔
    { entries := entries✝, nodupKeys := nodupKeys✝ }.entries ~ s₂.entries
-- Mathlib/RingTheory/Localization/Integer.lean
theorem isInteger_smul {a : R} {b : S} (hb : IsInteger R b) : IsInteger R (a • b)

Proof state:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S) b' = b
⊢ (algebraMap R S) (a * b') = a • b

Tactic:
rw [← hb, (algebraMap R S).map_mul, Algebra.smul_def]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
hb : IsInteger R b
⊢ IsInteger R (a • b)

Tactic:
rcases hb with ⟨b', hb⟩

Result:
case intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S) b' = b
⊢ IsInteger R (a • b)

Proof state:
case intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S) b' = b
⊢ IsInteger R (a • b)

Tactic:
use a * b'

Result:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S) b' = b
⊢ (algebraMap R S) (a * b') = a • b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertList_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 toInsert : List ((a : α) × β a)}
    (h : Perm l1 l2) (distinct : DistinctKeys l1) :
    Perm (insertList l1 toInsert) (insertList l2 toInsert)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l1 l2 : List ((a : α) × β a)}, l1.Perm l2 → DistinctKeys l1 → (insertList l1 tl).Perm (insertList l2 tl)
l1 l2 : List ((a : α) × β a)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertList (insertEntry hd.fst hd.snd l1) tl).Perm (insertList (insertEntry hd.fst hd.snd l2) tl)

Tactic:
apply ih (insertEntry_of_perm distinct h) (DistinctKeys.insertEntry distinct)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l1 l2 toInsert : List ((a : α) × β a)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertList l1 toInsert).Perm (insertList l2 toInsert)

Tactic:
induction toInsert generalizing l1 l2 with
| nil => simp [insertList, h]
| cons hd tl ih =>
  simp only [insertList]
  apply ih (insertEntry_of_perm distinct h) (DistinctKeys.insertEntry distinct)

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l1 l2 : List ((a : α) × β a)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertList l1 []).Perm (insertList l2 [])

Tactic:
simp [insertList, h]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l1 l2 : List ((a : α) × β a)}, l1.Perm l2 → DistinctKeys l1 → (insertList l1 tl).Perm (insertList l2 tl)
l1 l2 : List ((a : α) × β a)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertList l1 (hd :: tl)).Perm (insertList l2 (hd :: tl))

Tactic:
simp only [insertList]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l1 l2 : List ((a : α) × β a)}, l1.Perm l2 → DistinctKeys l1 → (insertList l1 tl).Perm (insertList l2 tl)
l1 l2 : List ((a : α) × β a)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertList (insertEntry hd.fst hd.snd l1) tl).Perm (insertList (insertEntry hd.fst hd.snd l2) tl)
-- Mathlib/Algebra/Lie/Submodule.lean
theorem ker_incl : I.incl.ker = ⊥

Proof state:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
m✝ : ↥I
⊢ m✝ ∈ I.incl.ker ↔ m✝ ∈ ⊥

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ I.incl.ker = ⊥

Tactic:
ext

Result:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
m✝ : ↥I
⊢ m✝ ∈ I.incl.ker ↔ m✝ ∈ ⊥
-- Mathlib/ModelTheory/Semantics.lean
theorem _root_.FirstOrder.Language.Formula.realize_iExs
    [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} : (φ.iExs γ).Realize v ↔
      ∃ (i : γ → M), φ.Realize (Sum.elim v i)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (∃ xs,
      Realize φ (fun x => Sum.elim (fun x => v x) (fun x => xs (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x =>
        xs (natAdd (Classical.choose ⋯) x)) ↔
    ∃ i, φ.Realize (Sum.elim v i)

Tactic:
refine Equiv.exists_congr ?_ ?_

Result:
case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Fin (Classical.choose ⋯) → M) ≃ (γ → M)

case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ ∀ (a : Fin (Classical.choose ⋯) → M),
    (Realize φ (fun x => Sum.elim (fun x => v x) (fun x => a (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x =>
        a (natAdd (Classical.choose ⋯) x)) ↔
      φ.Realize (Sum.elim v (?refine_1 a))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y = .ofNat n ((2^n - y % 2^n) + x)

Proof state:
n x y : Nat
⊢ BitVec.ofNat n x - BitVec.ofNat n y = BitVec.ofNat n (2 ^ n - y % 2 ^ n + x)

Tactic:
apply eq_of_toNat_eq

Result:
case a
n x y : Nat
⊢ (BitVec.ofNat n x - BitVec.ofNat n y).toNat = (BitVec.ofNat n (2 ^ n - y % 2 ^ n + x)).toNat

Proof state:
case a
n x y : Nat
⊢ (BitVec.ofNat n x - BitVec.ofNat n y).toNat = (BitVec.ofNat n (2 ^ n - y % 2 ^ n + x)).toNat

Tactic:
simp [BitVec.ofNat, Fin.ofNat'_sub]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem id_comp (f : α →. β) : (PFun.id β).comp f = f :=
  ext fun _ _ => by simp

Proof state:
α : Type u_1
β : Type u_2
f : α →. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ (PFun.id β).comp f x✝¹ ↔ x✝ ∈ f x✝¹

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
⊢ ∀ (a : P) (ha : a ∈ S),
    ((-1) ^ ↑a.2 • X.δ a.2) ≫ ((-1) ^ ↑a.1 • X.δ a.1) =
      -((-1) ^ ↑(φ a ha).2 • X.δ (φ a ha).2) ≫ ((-1) ^ ↑(φ a ha).1 • X.δ (φ a ha).1)

Tactic:
rintro ⟨i, j⟩ hij

Result:
case h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑(i, j).2 • X.δ (i, j).2) ≫ ((-1) ^ ↑(i, j).1 • X.δ (i, j).1) =
    -((-1) ^ ↑(φ (i, j) hij).2 • X.δ (φ (i, j) hij).2) ≫ ((-1) ^ ↑(φ (i, j) hij).1 • X.δ (φ (i, j) hij).1)
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem closedBall_subset_cthickening_singleton {α : Type*} [PseudoMetricSpace α] (x : α) (δ : ℝ) :
    closedBall x δ ⊆ cthickening δ ({x} : Set α)

Proof state:
case inl
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : δ < 0
⊢ closedBall x δ ⊆ cthickening δ {x}

Tactic:
simp only [closedBall_eq_empty.mpr hδ, empty_subset]

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ closedBall x δ ⊆ cthickening δ {x}

Tactic:
simp only [cthickening_singleton x hδ, Subset.rfl]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ {x}

Tactic:
rcases lt_or_le δ 0 with (hδ | hδ)

Result:
case inl
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : δ < 0
⊢ closedBall x δ ⊆ cthickening δ {x}

case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ closedBall x δ ⊆ cthickening δ {x}
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_rpow_of_exponent_ge_of_imp (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hyz : z ≤ y)
    (h : x = 0 → y = 0 → z = 0) :
    x ^ y ≤ x ^ z

Proof state:
case inl.inl
z : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hyz : z ≤ 0
h : 0 = 0 → 0 = 0 → z = 0
⊢ 0 ^ 0 ≤ 0 ^ z

Tactic:
rw [h rfl rfl]

Result:
no goals

Proof state:
case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ^ y ≤ 0 ^ z

Tactic:
rw [zero_rpow hy0]

Result:
case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ≤ 0 ^ z

Proof state:
case inr
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z

Tactic:
exact rpow_le_rpow_of_exponent_ge hx0' hx1 hyz

Result:
no goals

Proof state:
case inl
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
⊢ 0 ^ y ≤ 0 ^ z

Tactic:
rcases eq_or_ne y 0 with rfl | hy0

Result:
case inl.inl
z : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hyz : z ≤ 0
h : 0 = 0 → 0 = 0 → z = 0
⊢ 0 ^ 0 ≤ 0 ^ z

case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ^ y ≤ 0 ^ z

Proof state:
case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ≤ 0 ^ z

Tactic:
apply zero_rpow_nonneg

Result:
no goals

Proof state:
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
⊢ x ^ y ≤ x ^ z

Tactic:
rcases eq_or_lt_of_le hx0 with (rfl | hx0')

Result:
case inl
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
⊢ 0 ^ y ≤ 0 ^ z

case inr
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z