harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Sigma.lean
theorem dlookup_append (l₁ l₂ : List (Sigma β)) (a : α) :
    (l₁ ++ l₂).dlookup a = (l₁.dlookup a).or (l₂.dlookup a)

Proof state:
case cons.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
x : Sigma β
l₁ : List (Sigma β)
IH : dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)
hb : a ≠ x.fst
⊢ dlookup a (x :: (l₁ ++ l₂)) = (dlookup a (x :: l₁)).or (dlookup a l₂)

Tactic:
rw [dlookup_cons_ne _ _ hb, dlookup_cons_ne _ _ hb, IH]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
⊢ dlookup a ([] ++ l₂) = (dlookup a []).or (dlookup a l₂)

Tactic:
rfl

Result:
no goals

Proof state:
case cons.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
x : Sigma β
l₁ : List (Sigma β)
IH : dlookup x.fst (l₁ ++ l₂) = (dlookup x.fst l₁).or (dlookup x.fst l₂)
⊢ dlookup x.fst (x :: (l₁ ++ l₂)) = (dlookup x.fst (x :: l₁)).or (dlookup x.fst l₂)

Tactic:
rw [dlookup_cons_eq, dlookup_cons_eq, Option.or]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
x : Sigma β
l₁ : List (Sigma β)
IH : dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)
⊢ dlookup a (x :: (l₁ ++ l₂)) = (dlookup a (x :: l₁)).or (dlookup a l₂)

Tactic:
obtain rfl | hb := Decidable.eq_or_ne a x.1

Result:
case cons.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
x : Sigma β
l₁ : List (Sigma β)
IH : dlookup x.fst (l₁ ++ l₂) = (dlookup x.fst l₁).or (dlookup x.fst l₂)
⊢ dlookup x.fst (x :: (l₁ ++ l₂)) = (dlookup x.fst (x :: l₁)).or (dlookup x.fst l₂)

case cons.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
x : Sigma β
l₁ : List (Sigma β)
IH : dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)
hb : a ≠ x.fst
⊢ dlookup a (x :: (l₁ ++ l₂)) = (dlookup a (x :: l₁)).or (dlookup a l₂)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
x : Sigma β
l₁ : List (Sigma β)
IH : dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)
⊢ dlookup a (x :: l₁ ++ l₂) = (dlookup a (x :: l₁)).or (dlookup a l₂)

Tactic:
rw [cons_append]

Result:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
x : Sigma β
l₁ : List (Sigma β)
IH : dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)
⊢ dlookup a (x :: (l₁ ++ l₂)) = (dlookup a (x :: l₁)).or (dlookup a l₂)
-- Mathlib/Algebra/Lie/Submodule.lean
theorem lieSpan_le {N} : lieSpan R L s ≤ N ↔ s ⊆ N

Proof state:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : m ∈ lieSpan R L s
⊢ m ∈ N

Tactic:
rw [mem_lieSpan] at hm

Result:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : ∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N
⊢ m ∈ N

Proof state:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N → s ⊆ ↑N

Tactic:
exact Subset.trans subset_lieSpan

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N ↔ s ⊆ ↑N

Tactic:
constructor

Result:
case mp
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
⊢ lieSpan R L s ≤ N → s ⊆ ↑N

case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
⊢ s ⊆ ↑N → lieSpan R L s ≤ N

Proof state:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
⊢ s ⊆ ↑N → lieSpan R L s ≤ N

Tactic:
intro hs m hm

Result:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : m ∈ lieSpan R L s
⊢ m ∈ N

Proof state:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : ∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N
⊢ m ∈ N

Tactic:
exact hm _ hs

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_mul_C_eq_of_mul_eq_one {ai : R} (au : a * ai = 1) :
    (p * C a).natDegree = p.natDegree :=
  le_antisymm (natDegree_mul_C_le p a)
    (calc
      p.natDegree = (p * 1).natDegree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ p.natDegree = (p * 1).natDegree

Tactic:
nth_rw 1 [← mul_one p]

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ (p * 1).natDegree = (p * C a * C ai).natDegree

Tactic:
rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropOn_indep_chart [HasGroupoid M G] [HasGroupoid M' G'] (he : e ∈ G.maximalAtlas M)
    (hf : f ∈ G'.maximalAtlas M') (h : LiftPropOn P g s) {y : H}
    (hy : y ∈ e.target ∩ e.symm ⁻¹' (s ∩ g ⁻¹' f.source)) :
    P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) y

Proof state:
case h.e'_3
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : PartialHomeomorph M H
f : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
inst✝¹ : HasGroupoid M G
inst✝ : HasGroupoid M' G'
he : e ∈ maximalAtlas M G
hf : f ∈ maximalAtlas M' G'
h : LiftPropOn P g s
y : H
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ g ⁻¹' f.source)
⊢ y = ↑e (↑e.symm y)

Tactic:
rw [e.right_inv hy.1]

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : PartialHomeomorph M H
f : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
inst✝¹ : HasGroupoid M G
inst✝ : HasGroupoid M' G'
he : e ∈ maximalAtlas M G
hf : f ∈ maximalAtlas M' G'
h : LiftPropOn P g s
y : H
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ g ⁻¹' f.source)
⊢ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) y

Tactic:
convert ((hG.liftPropWithinAt_indep_chart he (e.symm_mapsTo hy.1) hf hy.2.2).1 (h _ hy.2.1)).2

Result:
case h.e'_3
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : PartialHomeomorph M H
f : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
inst✝¹ : HasGroupoid M G
inst✝ : HasGroupoid M' G'
he : e ∈ maximalAtlas M G
hf : f ∈ maximalAtlas M' G'
h : LiftPropOn P g s
y : H
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ g ⁻¹' f.source)
⊢ y = ↑e (↑e.symm y)
-- Mathlib/Order/Filter/Map.lean
theorem comap_map {f : Filter α} {m : α → β} (h : Injective m) : comap m (map m f) = f :=
  le_antisymm
    (fun s hs =>
      mem_of_superset (preimage_mem_comap <| image_mem_map hs) <| by
        simp only [preimage_image_eq s h, Subset.rfl])
    le_comap_map

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
h : Injective m
s : Set α
hs : s ∈ f
⊢ m ⁻¹' (m '' s) ⊆ s

Tactic:
simp only [preimage_image_eq s h, Subset.rfl]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem ball_zero : ball x 0 = ∅

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ ball x 0 = ∅

Tactic:
rw [ball_eq_empty]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem contSupp_cons₁ (fs k) :
    contSupp (Cont'.cons₁ fs k) =
      trStmts₁
          (move₂ (fun _ => false) main aux <|
            move₂ (fun s => s = Γ'.consₗ) stack main <|
              move₂ (fun _ => false) aux stack <| trNormal fs (Cont'.cons₂ k)) ∪
        codeSupp fs (Cont'.cons₂ k)

Proof state:
fs : Code
k : Cont'
⊢ contSupp (Cont'.cons₁ fs k) =
    trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal fs k.cons₂)))) ∪
      codeSupp fs k.cons₂

Tactic:
simp [codeSupp, codeSupp', contSupp, Finset.union_assoc]

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem CPolynomialOn.continuous {f : E → F} (fa : CPolynomialOn 𝕜 f univ) : Continuous f

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
fa : CPolynomialOn 𝕜 f univ
⊢ Continuous f

Tactic:
rw [continuous_iff_continuousOn_univ]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
fa : CPolynomialOn 𝕜 f univ
⊢ ContinuousOn f univ

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
fa : CPolynomialOn 𝕜 f univ
⊢ ContinuousOn f univ

Tactic:
exact fa.continuousOn

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem coeff_sub {x y : HahnSeries Γ R} {a : Γ} : (x - y).coeff a = x.coeff a - y.coeff a

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x y : HahnSeries Γ R
a : Γ
⊢ (x - y).coeff a = x.coeff a - y.coeff a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.finite_of_compl {s : Set α} (hs : s.Finite) (hsc : sᶜ.Finite) : Finite α

Proof state:
α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ (s ∪ sᶜ).Finite

Tactic:
exact hs.union hsc

Result:
no goals

Proof state:
α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ Finite α

Tactic:
rw [← finite_univ_iff, ← union_compl_self s]

Result:
α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ (s ∪ sᶜ).Finite
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem Set.Countable.measurableSet {s : Set α} (hs : s.Countable) : MeasurableSet s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet (⋃ x ∈ s, {x})

Tactic:
exact .biUnion hs fun b _ => .singleton b

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet s

Tactic:
rw [← biUnion_of_singleton s]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet (⋃ x ∈ s, {x})
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_union'' (hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f))
    (hs : (s ∩ mulSupport f).Finite) (ht : (t ∩ mulSupport f).Finite) :
    ∏ᶠ i ∈ s ∪ t, f i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
  finprod_mem_union hst hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_uIcc : #(uIcc a b) = (b - a : ℤ).natAbs + 1

Proof state:
n : ℕ
a b : Fin n
⊢ #(uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]

Result:
no goals
-- Mathlib/Algebra/CharZero/Defs.lean
theorem charZero_of_inj_zero [AddGroupWithOne R] (H : ∀ n : ℕ, (n : R) = 0 → n = 0) :
    CharZero R :=
  ⟨@fun m n h => by
    induction m generalizing n with
    | zero => rw [H n]; rw [← h, Nat.cast_zero]
    | succ m ih =>
      cases n
      · apply H; rw [h, Nat.cast_zero]
      · simp only [Nat.cast_succ, add_right_cancel_iff] at h; rwa [ih]⟩

Proof state:
case succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n : ℕ
h : ↑(m + 1) = ↑n
⊢ m + 1 = n

Tactic:
cases n

Result:
case succ.zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(m + 1) = ↑0
⊢ m + 1 = 0

case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑(m + 1) = ↑(n✝ + 1)
⊢ m + 1 = n✝ + 1

Proof state:
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ 0 = n

Tactic:
rw [H n]

Result:
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ ↑n = 0

Proof state:
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ ↑n = 0

Tactic:
rw [← h, Nat.cast_zero]

Result:
no goals

Proof state:
case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑m = ↑n✝
⊢ m + 1 = n✝ + 1

Tactic:
rwa [ih]

Result:
no goals

Proof state:
case succ.zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(m + 1) = ↑0
⊢ m + 1 = 0

Tactic:
apply H

Result:
case succ.zero.a
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(m + 1) = ↑0
⊢ ↑(m + 1) = 0

Proof state:
case succ.zero.a
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(m + 1) = ↑0
⊢ ↑(m + 1) = 0

Tactic:
rw [h, Nat.cast_zero]

Result:
no goals

Proof state:
case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑(m + 1) = ↑(n✝ + 1)
⊢ m + 1 = n✝ + 1

Tactic:
simp only [Nat.cast_succ, add_right_cancel_iff] at h

Result:
case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑m = ↑n✝
⊢ m + 1 = n✝ + 1
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp] lemma insidePart_zero : insidePart 0 = 0

Proof state:
⊢ insidePart 0 = 0

Tactic:
simp [insidePart]

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Defs.lean
theorem mul_inv_cancel_assoc (h : Commute a b) : a * (b * a⁻¹) = b

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a * (b * a⁻¹) = b

Tactic:
rw [← mul_assoc, h.mul_inv_cancel]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_C_mul_X_pow' (n : ℕ) (c : R) : Polynomial.support (C c * X ^ n) ⊆ singleton n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
c : R
⊢ (C c * X ^ n).support ⊆ {n}

Tactic:
simpa only [C_mul_X_pow_eq_monomial] using support_monomial' n c

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem eq_singleton_right_prod_subset_idRel {X : Type*} {S T : Set X} (hS : S.Nonempty)
    (hT : T.Nonempty) (h_diag : S ×ˢ T ⊆ idRel) : ∃ x, T = {x}

Proof state:
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
⊢ ∃ x, T = {x}

Tactic:
rw [Set.prod_subset_iff] at h_diag

Result:
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : ∀ x ∈ S, ∀ y ∈ T, (x, y) ∈ idRel
⊢ ∃ x, T = {x}

Proof state:
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : ∀ x ∈ S, ∀ y ∈ T, (x, y) ∈ idRel
⊢ ∃ x, T = {x}

Tactic:
replace h_diag := fun x hx y hy => (h_diag y hy x hx).symm

Result:
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : ∀ x ∈ T, ∀ y ∈ S, (y, x).2 = (y, x).1
⊢ ∃ x, T = {x}

Proof state:
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : ∀ x ∈ T, ∀ y ∈ S, (y, x).2 = (y, x).1
⊢ ∃ x, T = {x}

Tactic:
exact eq_singleton_left_of_prod_subset_idRel hT hS (prod_subset_iff.mpr h_diag)

Result:
no goals
-- Mathlib/Data/Fintype/Fin.lean
theorem map_valEmbedding_univ : (Finset.univ : Finset (Fin n)).map Fin.valEmbedding = Iio n

Proof state:
n : ℕ
⊢ map valEmbedding univ = Iio n

Tactic:
ext

Result:
case h
n a✝ : ℕ
⊢ a✝ ∈ map valEmbedding univ ↔ a✝ ∈ Iio n

Proof state:
case h
n a✝ : ℕ
⊢ a✝ ∈ map valEmbedding univ ↔ a✝ ∈ Iio n

Tactic:
simp [orderIsoSubtype.symm.surjective.exists, OrderIso.symm]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma iInf_mul_iInf {f g : ι → ℝ≥0∞} (hf : ∃ i, f i ≠ ∞) (hg : ∃ j, g j ≠ ∞)
    (h : ∀ i j, ∃ k, f k * g k ≤ f i * g j) : (⨅ i, f i) * ⨅ i, g i = ⨅ i, f i * g i

Proof state:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
h : ∀ (i j : ι), ∃ k, f k * g k ≤ f i * g j
i j : ι
⊢ ⨅ i, f i * g i ≤ f i * g j

Tactic:
obtain ⟨k, hk⟩ := h i j

Result:
case intro
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
h : ∀ (i j : ι), ∃ k, f k * g k ≤ f i * g j
i j k : ι
hk : f k * g k ≤ f i * g j
⊢ ⨅ i, f i * g i ≤ f i * g j

Proof state:
case intro
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
h : ∀ (i j : ι), ∃ k, f k * g k ≤ f i * g j
i j k : ι
hk : f k * g k ≤ f i * g j
⊢ ⨅ i, f i * g i ≤ f i * g j

Tactic:
exact iInf_le_of_le k hk

Result:
no goals

Proof state:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
h : ∀ (i j : ι), ∃ k, f k * g k ≤ f i * g j
⊢ (⨅ i, f i) * ⨅ i, g i = ⨅ i, f i * g i

Tactic:
refine le_antisymm (le_iInf fun i ↦ mul_le_mul' (iInf_le ..) (iInf_le ..))
  (le_iInf_mul_iInf hf hg fun i j ↦ ?_)

Result:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
h : ∀ (i j : ι), ∃ k, f k * g k ≤ f i * g j
i j : ι
⊢ ⨅ i, f i * g i ≤ f i * g j
-- Mathlib/Logic/Function/Basic.lean
/-- A symmetric relation `r : α → α → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some involutive function `f`. -/
protected lemma Symmetric.forall_existsUnique_iff {r : α → α → Prop} (hr : Symmetric r) :
    (∀ a, ∃! b, r a b) ↔ ∃ f : α → α, Involutive f ∧ ∀ {a b}, r a b ↔ f a = b

Proof state:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b

Tactic:
simp [hr.forall_existsUnique_iff', funext_iff]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
@[simp, nolint simpNF] lemma natCast_pos {n : ℕ} : (0 : ℤ) < n ↔ 0 < n

Proof state:
n : ℕ
⊢ 0 < ↑n ↔ 0 < n

Tactic:
omega

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma adj_toSubgraph_mapLe {G' : SimpleGraph V} {w x : V} {p : G.Walk u v} (h : G ≤ G') :
    (p.mapLe h).toSubgraph.Adj w x ↔ p.toSubgraph.Adj w x

Proof state:
V : Type u
G : SimpleGraph V
u v : V
G' : SimpleGraph V
w x : V
p : G.Walk u v
h : G ≤ G'
⊢ (mapLe h p).toSubgraph.Adj w x ↔ p.toSubgraph.Adj w x

Tactic:
simp only [toSubgraph_map, Subgraph.map_adj]

Result:
V : Type u
G : SimpleGraph V
u v : V
G' : SimpleGraph V
w x : V
p : G.Walk u v
h : G ≤ G'
⊢ Relation.Map p.toSubgraph.Adj (⇑(Hom.mapSpanningSubgraphs h)) (⇑(Hom.mapSpanningSubgraphs h)) w x ↔
    p.toSubgraph.Adj w x

Proof state:
V : Type u
G : SimpleGraph V
u v : V
G' : SimpleGraph V
w x : V
p : G.Walk u v
h : G ≤ G'
⊢ Relation.Map p.toSubgraph.Adj (⇑(Hom.mapSpanningSubgraphs h)) (⇑(Hom.mapSpanningSubgraphs h))
      ((Hom.mapSpanningSubgraphs h) w) ((Hom.mapSpanningSubgraphs h) x) ↔
    p.toSubgraph.Adj w x

Tactic:
rw [Relation.map_apply_apply (Hom.mapSpanningSubgraphs_injective h)
  (Hom.mapSpanningSubgraphs_injective h)]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
G' : SimpleGraph V
w x : V
p : G.Walk u v
h : G ≤ G'
⊢ Relation.Map p.toSubgraph.Adj (⇑(Hom.mapSpanningSubgraphs h)) (⇑(Hom.mapSpanningSubgraphs h)) w x ↔
    p.toSubgraph.Adj w x

Tactic:
nth_rewrite 1 [← Hom.mapSpanningSubgraphs_apply h w, ← Hom.mapSpanningSubgraphs_apply h x]

Result:
V : Type u
G : SimpleGraph V
u v : V
G' : SimpleGraph V
w x : V
p : G.Walk u v
h : G ≤ G'
⊢ Relation.Map p.toSubgraph.Adj (⇑(Hom.mapSpanningSubgraphs h)) (⇑(Hom.mapSpanningSubgraphs h))
      ((Hom.mapSpanningSubgraphs h) w) ((Hom.mapSpanningSubgraphs h) x) ↔
    p.toSubgraph.Adj w x
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_le_pi_div_two_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) :
    ∠ p₂ p₃ p₁ ≤ π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) ≤ π / 2

Tactic:
exact angle_add_le_pi_div_two_of_inner_eq_zero h

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ ∠ p₂ p₃ p₁ ≤ π / 2

Tactic:
rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) ≤ π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ ∠ p₂ p₃ p₁ ≤ π / 2

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ ∠ p₂ p₃ p₁ ≤ π / 2
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem isometry_vertical_line (a : ℝ) : Isometry fun y => mk ⟨a, exp y⟩ (exp_pos y)

Proof state:
a y₁ y₂ : ℝ
⊢ dist (log (mk { re := a, im := rexp y₁ } ⋯).im) (log (mk { re := a, im := rexp y₂ } ⋯).im) = dist y₁ y₂

a y₁ y₂ : ℝ
⊢ (mk { re := a, im := rexp y₁ } ⋯).re = (mk { re := a, im := rexp y₂ } ⋯).re

Tactic:
exacts [congr_arg₂ _ (log_exp _) (log_exp _), rfl]

Result:
no goals

Proof state:
a y₁ y₂ : ℝ
⊢ dist (mk { re := a, im := rexp y₁ } ⋯) (mk { re := a, im := rexp y₂ } ⋯) = dist y₁ y₂

Tactic:
rw [dist_of_re_eq]

Result:
a y₁ y₂ : ℝ
⊢ dist (log (mk { re := a, im := rexp y₁ } ⋯).im) (log (mk { re := a, im := rexp y₂ } ⋯).im) = dist y₁ y₂

a y₁ y₂ : ℝ
⊢ (mk { re := a, im := rexp y₁ } ⋯).re = (mk { re := a, im := rexp y₂ } ⋯).re

Proof state:
a : ℝ
⊢ Isometry fun y => mk { re := a, im := rexp y } ⋯

Tactic:
refine Isometry.of_dist_eq fun y₁ y₂ => ?_

Result:
a y₁ y₂ : ℝ
⊢ dist (mk { re := a, im := rexp y₁ } ⋯) (mk { re := a, im := rexp y₂ } ⋯) = dist y₁ y₂
-- Mathlib/Data/Set/Image.lean
theorem image_comm {β'} {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ}
    (h_comm : ∀ a, f (g a) = g' (f' a)) : (s.image g).image f = (s.image f').image g'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
β' : Type u_5
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ f '' (g '' s) = g' '' (f' '' s)

Tactic:
simp_rw [image_image, h_comm]

Result:
no goals