harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem distortion_biUnion (π : Prepartition I) (πi : ∀ J, Prepartition J) :
    (π.biUnion πi).distortion = π.boxes.sup fun J => (πi J).distortion

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnion πi).distortion = π.boxes.sup fun J => (πi J).distortion

Tactic:
classical exact sup_biUnion _ _

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnion πi).distortion = π.boxes.sup fun J => (πi J).distortion

Tactic:
exact sup_biUnion _ _

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem mul_star_self_nonneg (r : R) : 0 ≤ r * star r

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
r : R
⊢ 0 ≤ r * star r

Tactic:
simpa only [star_star] using star_mul_self_nonneg (star r)

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomial.lean
theorem HasFiniteFPowerSeriesAt.sub (hf : HasFiniteFPowerSeriesAt f pf x n)
    (hg : HasFiniteFPowerSeriesAt g pg x m) :
    HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (max n m)

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 g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
n m : ℕ
hf : HasFiniteFPowerSeriesAt f pf x n
hg : HasFiniteFPowerSeriesAt g pg x m
⊢ HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (n ⊔ m)

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem compl_mem_iff_not_mem : sᶜ ∈ f ↔ s ∉ f

Proof state:
α : Type u
f : Ultrafilter α
s : Set α
⊢ sᶜ ∈ f ↔ s ∉ f

Tactic:
rw [← compl_not_mem_iff, compl_compl]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp] lemma outsidePart_zero : outsidePart 0 = 0

Proof state:
⊢ outsidePart 0 = 0

Tactic:
simp [outsidePart]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma sub_add_cancel {a : EReal} {b : Real} : a - b + b = a

Proof state:
a : EReal
b : ℝ
⊢ a - ↑b + ↑b = a

Tactic:
rw [add_comm, ← add_sub_assoc, add_sub_cancel_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofNat_lt_ofNat {n} {x y : Nat} : BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2^n < y % 2^n

Proof state:
n x y : Nat
⊢ BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2 ^ n < y % 2 ^ n

Tactic:
simp [lt_def]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem supports_insert {K S q} :
    Supports (insert q K) S ↔ TM2.SupportsStmt S (tr q) ∧ Supports K S

Proof state:
K S : Finset Λ'
q : Λ'
⊢ Supports (insert q K) S ↔ TM2.SupportsStmt S (tr q) ∧ Supports K S

Tactic:
simp [Supports]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isLT_iff_eq_lt {o : Ordering} : o.isLT ↔ o = .lt

Proof state:
o : Ordering
⊢ o.isLT = true ↔ o = lt

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem singletonSubgraph_le_iff (v : V) (H : G.Subgraph) :
    G.singletonSubgraph v ≤ H ↔ v ∈ H.verts

Proof state:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ G.singletonSubgraph v ≤ H

Tactic:
constructor

Result:
case left
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ (G.singletonSubgraph v).verts ⊆ H.verts

case right
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, (G.singletonSubgraph v).Adj v_1 w → H.Adj v_1 w

Proof state:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
⊢ G.singletonSubgraph v ≤ H ↔ v ∈ H.verts

Tactic:
refine ⟨fun h ↦ h.1 (Set.mem_singleton v), ?_⟩

Result:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
⊢ v ∈ H.verts → G.singletonSubgraph v ≤ H

Proof state:
case right
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, (G.singletonSubgraph v).Adj v_1 w → H.Adj v_1 w

Tactic:
exact fun _ _ ↦ False.elim

Result:
no goals

Proof state:
case left
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ (G.singletonSubgraph v).verts ⊆ H.verts

Tactic:
rwa [singletonSubgraph_verts, Set.singleton_subset_iff]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
⊢ v ∈ H.verts → G.singletonSubgraph v ≤ H

Tactic:
intro h

Result:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ G.singletonSubgraph v ≤ H
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
    {v : β k} : containsKey a (replaceEntry k v l) = containsKey a l

Proof state:
case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : ¬((getEntry? k l).isSome = true ∧ (k == a) = true)
⊢ containsKey a (replaceEntry k v l) = containsKey a l

Tactic:
simp [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
⊢ containsKey a (replaceEntry k v l) = containsKey a l

Tactic:
by_cases h : (getEntry? k l).isSome ∧ k == a

Result:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : (getEntry? k l).isSome = true ∧ (k == a) = true
⊢ containsKey a (replaceEntry k v l) = containsKey a l

case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : ¬((getEntry? k l).isSome = true ∧ (k == a) = true)
⊢ containsKey a (replaceEntry k v l) = containsKey a l

Proof state:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : (getEntry? k l).isSome = true ∧ (k == a) = true
⊢ containsKey a (replaceEntry k v l) = containsKey a l

Tactic:
simp only [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, and_self, ↓reduceIte,
  Option.isSome_some, Bool.true_eq]

Result:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : (getEntry? k l).isSome = true ∧ (k == a) = true
⊢ (getEntry? a l).isSome = true

Proof state:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : (getEntry? k l).isSome = true ∧ (k == a) = true
⊢ (getEntry? a l).isSome = true

Tactic:
rw [← getEntry?_congr h.2, h.1]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem iff_symm_preimage_eq' :
    e.IsImage s t ↔ e.target ∩ e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
t : Set Y
⊢ e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t

Tactic:
rw [iff_symm_preimage_eq, ← image_source_inter_eq, ← image_source_inter_eq']

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_equiv_eq_arrow_of_lift_eq (leq : lift.{v} #α = lift.{u} #β') :
    #(α ≃ β') = #(α → β')

Proof state:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
⊢ #(α ≃ β') = #(α → β')

Tactic:
obtain ⟨e⟩ := lift_mk_eq'.mp leq

Result:
case intro
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
⊢ #(α ≃ β') = #(α → β')

Proof state:
case intro
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α ≃ β') = #(α → β')

Tactic:
rw [← e₁, ← e₂, lift_inj, mk_perm_eq_self_power, power_def]

Result:
no goals

Proof state:
case intro
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
⊢ #(α ≃ β') = #(α → β')

Tactic:
have e₁ := lift_mk_eq'.mpr ⟨.equivCongr (.refl α) e⟩

Result:
case intro
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')
⊢ #(α ≃ β') = #(α → β')

Proof state:
case intro
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = lift.{u, max u v} #(α → β')
⊢ #(α ≃ β') = #(α → β')

Tactic:
rw [lift_id'.{u,v}] at e₁ e₂

Result:
case intro
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α ≃ β') = #(α → β')

Proof state:
case intro
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')
⊢ #(α ≃ β') = #(α → β')

Tactic:
have e₂ := lift_mk_eq'.mpr ⟨.arrowCongr (.refl α) e⟩

Result:
case intro
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = lift.{u, max u v} #(α → β')
⊢ #(α ≃ β') = #(α → β')
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem coe_units_zpow (u : Mˣ) : ∀ n : ℤ, ((u ^ n : Mˣ) : M) = (u : M) ^ n
  | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, Units.val_pow_eq_pow_val]
  | -[k+1] => by
    rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv]

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
k : ℕ
⊢ ↑(u ^ -[k+1]) = ↑u ^ -[k+1]

Tactic:
rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
n : ℕ
⊢ ↑(u ^ ↑n) = ↑u ^ ↑n

Tactic:
rw [zpow_natCast, zpow_natCast, Units.val_pow_eq_pow_val]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem inter_prod : (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∩ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∩ s₂ ×ˢ t

Tactic:
simp only [← and_and_right, mem_inter_iff, mem_prod]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∩ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∩ s₂ ×ˢ t
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
theorem abs_density_star_sub_density_le_eps (hPε : ↑100 ≤ ↑4 ^ #P.parts * ε ^ 5)
    (hε₁ : ε ≤ 1) {hU : U ∈ P.parts} {hV : V ∈ P.parts} (hUV' : U ≠ V) (hUV : ¬G.IsUniform ε U V) :
    |(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id) : ℝ) -
      G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U)| ≤ ε / 5

Proof state:
case h.e'_4
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ ε / 5 = 2 * (ε / 10)

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ 0 ≤ ε / 10

Tactic:
sz_positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ |↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id)) -
        ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))| ≤
    ε / 5

Tactic:
convert abs_edgeDensity_sub_edgeDensity_le_two_mul G.Adj
  (biUnion_star_subset_nonuniformWitness hP G ε hU V)
  (biUnion_star_subset_nonuniformWitness hP G ε hV U) (by sz_positivity)
  (one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV' hUV hPε hε₁)
  (one_sub_eps_mul_card_nonuniformWitness_le_card_star hU hUV'.symm (fun hVU => hUV hVU.symm)
    hPε hε₁) using 1

Result:
case h.e'_4
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ ε / 5 = 2 * (ε / 10)
-- Mathlib/Probability/CDF.lean
/-- The measure associated to the cdf of a probability measure is the same probability measure. -/
lemma measure_cdf [IsProbabilityMeasure μ] : (cdf μ).measure = μ

Proof state:
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
a : ℝ
⊢ (cdf μ).measure (Iic a) = μ (Iic a)

Tactic:
rw [StieltjesFunction.measure_Iic _ (tendsto_cdf_atBot μ), sub_zero, ofReal_cdf]

Result:
no goals

Proof state:
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
⊢ (cdf μ).measure = μ

Tactic:
refine Measure.ext_of_Iic (cdf μ).measure μ (fun a ↦ ?_)

Result:
μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
a : ℝ
⊢ (cdf μ).measure (Iic a) = μ (Iic a)
-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem support_sum {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [∀ i₁, Zero (β₁ i₁)]
    [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)]
    [∀ (i) (x : β i), Decidable (x ≠ 0)] {f : Π₀ i₁, β₁ i₁} {g : ∀ i₁, β₁ i₁ → Π₀ i, β i} :
    (f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support

Proof state:
ι : Type u
β : ι → Type v
inst✝⁵ : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
this : ∀ (i₁ : ι), (f.sum fun i b => (g i b) i₁) ≠ 0 → ∃ i, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0
⊢ (f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support

Tactic:
simpa [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply] using this

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝⁵ : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
⊢ (f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support

Tactic:
have :
  ∀ i₁ : ι,
    (f.sum fun (i : ι₁) (b : β₁ i) => (g i b) i₁) ≠ 0 → ∃ i : ι₁, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0 :=
  fun i₁ h =>
  let ⟨i, hi, Ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
  ⟨i, mem_support_iff.1 hi, Ne⟩

Result:
ι : Type u
β : ι → Type v
inst✝⁵ : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
this : ∀ (i₁ : ι), (f.sum fun i b => (g i b) i₁) ≠ 0 → ∃ i, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0
⊢ (f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
/-- Formula for `Λ₀ 1`, where `Λ₀` is the entire function satisfying
`Λ₀ s = π ^ (-s / 2) Γ(s / 2) ζ(s) + 1 / s + 1 / (1 - s)` away from `s = 0, 1`.

Note that `s = 1` is _not_ a pole of `Λ₀`, so this statement (unlike `riemannZeta_one`) is
a mathematically meaningful statement and is not dependent on Mathlib's particular conventions for
division by zero. -/
lemma _root_.completedRiemannZeta₀_one :
    completedRiemannZeta₀ 1 = (γ - Complex.log (4 * ↑π)) / 2 + 1

Proof state:
⊢ completedRiemannZeta₀ 1 = (↑γ - Complex.log (4 * ↑π)) / 2 + 1

Tactic:
have := completedRiemannZeta_eq 1

Result:
this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 1 / (1 - 1)
⊢ completedRiemannZeta₀ 1 = (↑γ - Complex.log (4 * ↑π)) / 2 + 1

Proof state:
this : completedRiemannZeta 1 + 1 = completedRiemannZeta₀ 1
⊢ completedRiemannZeta₀ 1 = (↑γ - Complex.log (4 * ↑π)) / 2 + 1

Tactic:
rw [← this, completedRiemannZeta_one]

Result:
no goals

Proof state:
this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 1 / (1 - 1)
⊢ completedRiemannZeta₀ 1 = (↑γ - Complex.log (4 * ↑π)) / 2 + 1

Tactic:
rw [sub_self, div_zero, div_one, sub_zero, eq_sub_iff_add_eq] at this

Result:
this : completedRiemannZeta 1 + 1 = completedRiemannZeta₀ 1
⊢ completedRiemannZeta₀ 1 = (↑γ - Complex.log (4 * ↑π)) / 2 + 1
-- Mathlib/Data/Matrix/Kronecker.lean
theorem kroneckerMap_reindex (f : α → β → γ) (el : l ≃ l') (em : m ≃ m') (en : n ≃ n') (ep : p ≃ p')
    (M : Matrix l m α) (N : Matrix n p β) :
    kroneckerMap f (reindex el em M) (reindex en ep N) =
      reindex (el.prodCongr en) (em.prodCongr ep) (kroneckerMap f M N)

Proof state:
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
⊢ kroneckerMap f ((reindex el em) M) ((reindex en ep) N) =
    (reindex (el.prodCongr en) (em.prodCongr ep)) (kroneckerMap f M N)

Tactic:
ext ⟨i, i'⟩ ⟨j, j'⟩

Result:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
i : l'
i' : n'
j : m'
j' : p'
⊢ kroneckerMap f ((reindex el em) M) ((reindex en ep) N) (i, i') (j, j') =
    (reindex (el.prodCongr en) (em.prodCongr ep)) (kroneckerMap f M N) (i, i') (j, j')

Proof state:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
l' : Type u_14
m' : Type u_15
n' : Type u_16
p' : Type u_17
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
i : l'
i' : n'
j : m'
j' : p'
⊢ kroneckerMap f ((reindex el em) M) ((reindex en ep) N) (i, i') (j, j') =
    (reindex (el.prodCongr en) (em.prodCongr ep)) (kroneckerMap f M N) (i, i') (j, j')

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Endofunctor/Algebra.lean
theorem Algebra.homEquiv_naturality_str (adj : F ⊣ G) (A₁ A₂ : Algebra F) (f : A₁ ⟶ A₂) :
    (adj.homEquiv A₁.a A₁.a) A₁.str ≫ G.map f.f = f.f ≫ (adj.homEquiv A₂.a A₂.a) A₂.str

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ (adj.homEquiv A₁.a A₁.a) A₁.str ≫ G.map f.f = f.f ≫ (adj.homEquiv A₂.a A₂.a) A₂.str

Tactic:
rw [← Adjunction.homEquiv_naturality_right, ← Adjunction.homEquiv_naturality_left, f.h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_alterKey {k k' : α} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a))
    (hl : DistinctKeys l) :
    getKey? k' (alterKey k f l) =
      if k == k' then
        if (f (getValueCast? k l)).isSome then some k else none
      else
        getKey? k' l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
x✝ : Option (β k)
v✝ : β k
heq : f (getValueCast? k l) = some v✝
⊢ getKey? k' (insertEntry k v✝ l) =
    if (k == k') = true then if (f (getValueCast? k l)).isSome = true then some k else none else getKey? k' l

Tactic:
simp [hl, heq, getKey?_eraseKey, getKey?_insertEntry]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getKey? k' (alterKey k f l) =
    if (k == k') = true then if (f (getValueCast? k l)).isSome = true then some k else none else getKey? k' l

Tactic:
rw [alterKey]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getKey? k'
      (match f (getValueCast? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    if (k == k') = true then if (f (getValueCast? k l)).isSome = true then some k else none else getKey? k' l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getKey? k'
      (match f (getValueCast? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    if (k == k') = true then if (f (getValueCast? k l)).isSome = true then some k else none else getKey? k' l

Tactic:
split <;> next heq => simp [hl, heq, getKey?_eraseKey, getKey?_insertEntry]

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem inv_natCast_den (a : ℕ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a

Proof state:
a : ℕ
⊢ (↑a)⁻¹.den = if a = 0 then 1 else a

Tactic:
simpa [-inv_intCast_den, ofInt_eq_cast] using inv_intCast_den a

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mem_nthRootsFinset {n : ℕ} (h : 0 < n) {x : R} :
    x ∈ nthRootsFinset n R ↔ x ^ (n : ℕ) = 1

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : 0 < n
x : R
⊢ x ∈ nthRootsFinset n R ↔ x ^ n = 1

Tactic:
rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots h]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : 0 < n
x : R
⊢ x ∈ nthRootsFinset n R ↔ x ^ n = 1

Tactic:
classical
rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots h]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem coe_cycleRange_of_le {n : ℕ} {i j : Fin n} (h : j ≤ i) :
    (cycleRange i j : ℕ) = if j = i then 0 else (j : ℕ) + 1

Proof state:
case succ
n : ℕ
i j : Fin (n + 1)
h : j ≤ i
⊢ ↑(i.cycleRange j) = if j = i then 0 else ↑j + 1

Tactic:
rw [cycleRange_of_le h]

Result:
case succ
n : ℕ
i j : Fin (n + 1)
h : j ≤ i
⊢ ↑(if j = i then 0 else j + 1) = if j = i then 0 else ↑j + 1

Proof state:
case succ
n : ℕ
i j : Fin (n + 1)
h : j ≤ i
⊢ ↑(if j = i then 0 else j + 1) = if j = i then 0 else ↑j + 1

Tactic:
split_ifs with h'

Result:
case pos
n : ℕ
i j : Fin (n + 1)
h : j ≤ i
h' : j = i
⊢ ↑0 = 0

case neg
n : ℕ
i j : Fin (n + 1)
h : j ≤ i
h' : ¬j = i
⊢ ↑(j + 1) = ↑j + 1

Proof state:
case neg
n : ℕ
i j : Fin (n + 1)
h : j ≤ i
h' : ¬j = i
⊢ ↑(j + 1) = ↑j + 1

Tactic:
exact
  val_add_one_of_lt
    (calc
      (j : ℕ) < i := Fin.lt_iff_val_lt_val.mp (lt_of_le_of_ne h h')
      _ ≤ n := Nat.lt_succ_iff.mp i.2)

Result:
no goals

Proof state:
case pos
n : ℕ
i j : Fin (n + 1)
h : j ≤ i
h' : j = i
⊢ ↑0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case zero
i j : Fin 0
h : j ≤ i
⊢ ↑(i.cycleRange j) = if j = i then 0 else ↑j + 1

Tactic:
exact absurd le_rfl i.pos.not_le

Result:
no goals

Proof state:
n : ℕ
i j : Fin n
h : j ≤ i
⊢ ↑(i.cycleRange j) = if j = i then 0 else ↑j + 1

Tactic:
rcases n with - | n

Result:
case zero
i j : Fin 0
h : j ≤ i
⊢ ↑(i.cycleRange j) = if j = i then 0 else ↑j + 1

case succ
n : ℕ
i j : Fin (n + 1)
h : j ≤ i
⊢ ↑(i.cycleRange j) = if j = i then 0 else ↑j + 1