harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem count_roots [DecidableEq R] (p : R[X]) : p.roots.count a = rootMultiplicity a p

Proof state:
case neg
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a p.roots = rootMultiplicity a p

Tactic:
rw [roots_def, dif_neg hp]

Result:
case neg
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a (Classical.choose ⋯) = rootMultiplicity a p

Proof state:
case neg
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a (Classical.choose ⋯) = rootMultiplicity a p

Tactic:
exact (Classical.choose_spec (exists_multiset_roots hp)).2 a

Result:
no goals

Proof state:
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
⊢ count a p.roots = rootMultiplicity a p

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p = 0
⊢ count a p.roots = rootMultiplicity a p

case neg
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a p.roots = rootMultiplicity a p

Proof state:
case pos
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p = 0
⊢ count a p.roots = rootMultiplicity a p

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem inclusion_inclusion {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : H) :
    inclusion hKL (inclusion hHK x) = inclusion (hHK.trans hKL) x

Proof state:
case mk
G : Type u_1
inst✝² : Group G
S : Type u_4
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
L : S
hHK : H ≤ K
hKL : K ≤ L
val✝ : G
property✝ : val✝ ∈ H
⊢ (inclusion hKL) ((inclusion hHK) ⟨val✝, property✝⟩) = (inclusion ⋯) ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_4
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
L : S
hHK : H ≤ K
hKL : K ≤ L
x : ↥H
⊢ (inclusion hKL) ((inclusion hHK) x) = (inclusion ⋯) x

Tactic:
cases x

Result:
case mk
G : Type u_1
inst✝² : Group G
S : Type u_4
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
L : S
hHK : H ≤ K
hKL : K ≤ L
val✝ : G
property✝ : val✝ ∈ H
⊢ (inclusion hKL) ((inclusion hHK) ⟨val✝, property✝⟩) = (inclusion ⋯) ⟨val✝, property✝⟩
-- Mathlib/Data/Matrix/Mul.lean
theorem mul_mul_apply [Fintype n] (A B C : Matrix n n α) (i j : n) :
    (A * B * C) i j = A i ⬝ᵥ B *ᵥ (Cᵀ j)

Proof state:
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A * B * C) i j = A i ⬝ᵥ B *ᵥ Cᵀ j

Tactic:
rw [Matrix.mul_assoc]

Result:
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A * (B * C)) i j = A i ⬝ᵥ B *ᵥ Cᵀ j

Proof state:
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A * (B * C)) i j = A i ⬝ᵥ B *ᵥ Cᵀ j

Tactic:
simp only [mul_apply, dotProduct, mulVec]

Result:
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ ∑ x : n, A i x * ∑ j_1 : n, B x j_1 * C j_1 j = ∑ x : n, A i x * ∑ x_1 : n, B x x_1 * Cᵀ j x_1

Proof state:
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ ∑ x : n, A i x * ∑ j_1 : n, B x j_1 * C j_1 j = ∑ x : n, A i x * ∑ x_1 : n, B x x_1 * Cᵀ j x_1

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem disjoint_right_comm : Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b

Tactic:
simp_rw [disjoint_iff_inf_le, inf_right_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableOn.restrict_toMeasurable (hf : IntegrableOn f s μ) (h's : ∀ x ∈ s, f x ≠ 0) :
    μ.restrict (toMeasurable μ s) = μ.restrict s

Proof state:
case intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖}
A : ∀ (n : ℕ), μ (s ∩ v n) ≠ ⊤
x : α
hx : x ∈ s
this : 0 < ‖f x‖
n : ℕ
hn : u n < ‖f x‖
⊢ x ∈ ⋃ n, v n

Tactic:
exact mem_iUnion.2 ⟨n, subset_toMeasurable _ _ hn.le⟩

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖}
n : ℕ
⊢ μ (s ∩ v n) ≠ ⊤

Tactic:
rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _),
  measure_toMeasurable]

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, f x ≠ 0
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n => toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖}
n : ℕ
⊢ (μ.restrict s) {x | u n ≤ ‖f x‖} ≠ ⊤
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem measurable_of_Iio {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Iio x)) : Measurable f

Proof state:
case h.e'_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ mα = MeasurableSpace.generateFrom ?convert_2

Tactic:
exact BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Iio _)

Result:
no goals

Proof state:
case convert_4.intro
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
x : α
⊢ MeasurableSet (f ⁻¹' Iio x)

Tactic:
exact hf x

Result:
no goals

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ Measurable f

Tactic:
convert measurable_generateFrom (α := δ) _

Result:
case h.e'_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ mα = MeasurableSpace.generateFrom ?convert_2

case convert_2
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ Set (Set α)

case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ ∀ t ∈ ?convert_2, MeasurableSet (f ⁻¹' t)

Proof state:
case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ ∀ t ∈ range Iio, MeasurableSet (f ⁻¹' t)

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case convert_4.intro
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
x : α
⊢ MeasurableSet (f ⁻¹' Iio x)
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticCharFun_eq_zero_iff {a : F} : quadraticCharFun F a = 0 ↔ a = 0

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ quadraticCharFun F a = 0 ↔ a = 0

Tactic:
simp only [quadraticCharFun]

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (if IsSquare a then 1 else -1) = 0 ↔ False

Tactic:
split_ifs <;> simp only [neg_eq_zero, one_ne_zero, not_false_iff]

Result:
no goals

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0

Tactic:
simp only [ha, if_false]

Result:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (if IsSquare a then 1 else -1) = 0 ↔ False

Proof state:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0

Tactic:
simp only [ha, if_true]

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0

Tactic:
by_cases ha : a = 0

Result:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0

case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem mem_pairSelfAdjointMatricesSubmodule' :
    A ∈ pairSelfAdjointMatricesSubmodule J J₃ ↔ Matrix.IsAdjointPair J J₃ A A

Proof state:
R₂ : Type u_3
inst✝² : CommRing R₂
n : Type u_5
inst✝¹ : Fintype n
J J₃ A : Matrix n n R₂
inst✝ : DecidableEq n
⊢ A ∈ pairSelfAdjointMatricesSubmodule J J₃ ↔ J.IsAdjointPair J₃ A A

Tactic:
simp only [mem_pairSelfAdjointMatricesSubmodule]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_union :
    ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
⊢ ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_union, tendsto_sup]

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem dist_convolution_le' {x₀ : G} {R ε : ℝ} {z₀ : E'} (hε : 0 ≤ ε) (hif : Integrable f μ)
    (hf : support f ⊆ ball (0 : G) R) (hmg : AEStronglyMeasurable g μ)
    (hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε) :
    dist ((f ⋆[L, μ] g : G → F) x₀) (∫ t, L (f t) z₀ ∂μ) ≤ (‖L‖ * ∫ x, ‖f x‖ ∂μ) * ε

Proof state:
case pos
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∈ support f
⊢ dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε

Tactic:
have h2t := hf ht

Result:
case pos
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : t ∈ support f
h2t : t ∈ ball 0 R
⊢ dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε
-- Mathlib/Data/Finset/Option.lean
theorem eraseNone_none : eraseNone ({none} : Finset (Option α)) = ∅

Proof state:
case h
α : Type u_1
a✝ : α
⊢ a✝ ∈ eraseNone {none} ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
⊢ eraseNone {none} = ∅

Tactic:
ext

Result:
case h
α : Type u_1
a✝ : α
⊢ a✝ ∈ eraseNone {none} ↔ a✝ ∈ ∅
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
/-- A variant of `mul_inv_eq_iff_eq_mul₀` that moves the nonzero hypothesis to another variable. -/
lemma eq_mul_of_mul_inv_eq₀ (hb : b ≠ 0) (h : a * c⁻¹ = b) : a = b * c

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
hb : b ≠ 0
h : a * 0⁻¹ = b
⊢ False

Tactic:
simp [hb.symm] at h

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : a * c⁻¹ = b
⊢ c ≠ 0

Tactic:
rintro rfl

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
hb : b ≠ 0
h : a * 0⁻¹ = b
⊢ False

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : a * c⁻¹ = b
⊢ a = b * c

Tactic:
rwa [← mul_inv_eq_iff_eq_mul₀]

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : a * c⁻¹ = b
⊢ c ≠ 0
-- Mathlib/Algebra/Polynomial/Div.lean
lemma sub_modByMonic (p₁ p₂ q : R[X]) : (p₁ - p₂) %ₘ q = p₁ %ₘ q - p₂ %ₘ q

Proof state:
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
⊢ (p₁ - p₂) %ₘ q = p₁ %ₘ q - p₂ %ₘ q

Tactic:
simp [sub_eq_add_neg, add_modByMonic, neg_modByMonic]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
    ReadyForRupAdd f → ReadyForRupAdd (insert f c)

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb :
  hasAssignment b
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }.assignments[i.val] =
    true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ i.val < f.assignments.size

Tactic:
rw [f_readyForRupAdd.2.1]

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb :
  hasAssignment b
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }.assignments[i.val] =
    true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ i.val < n

Proof state:
case h_1.inr
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
heq✝ : c.isUnit = none
i : PosFin n
b : Bool
hb :
  hasAssignment b
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }.assignments[i.val] =
    true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = unit (i, b)
⊢ (some (unit (i, b)) ∈ f.clauses.toList ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = unit (i, b)

Tactic:
exact Or.inr hf

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Orthogonality.lean
theorem sum_characters_eq (a : ZMod n) :
    ∑ χ : DirichletCharacter R n, χ a = if a = 1 then (n.totient : R) else 0

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a = 1
⊢ ∑ χ : DirichletCharacter R n, χ a = ↑n.totient

Tactic:
simpa only [ha, map_one, Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one,
  ← Nat.card_eq_fintype_card]
  using congrArg Nat.cast <| card_eq_totient_of_hasEnoughRootsOfUnity R n

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : ¬a = 1
⊢ ∑ χ : DirichletCharacter R n, χ a = 0

Tactic:
exact sum_characters_eq_zero R ha

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
⊢ ∑ χ : DirichletCharacter R n, χ a = if a = 1 then ↑n.totient else 0

Tactic:
split_ifs with ha

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a = 1
⊢ ∑ χ : DirichletCharacter R n, χ a = ↑n.totient

case neg
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : ¬a = 1
⊢ ∑ χ : DirichletCharacter R n, χ a = 0
-- Mathlib/GroupTheory/Exponent.lean
theorem pow_exponent_eq_one (g : G) : g ^ exponent G = 1

Proof state:
G : Type u
inst✝ : Monoid G
g : G
⊢ g ^ exponent G = 1

Tactic:
by_cases h : ExponentExists G

Result:
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1

case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1

Proof state:
case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1

Tactic:
simp_rw [exponent, dif_neg h, pow_zero]

Result:
no goals

Proof state:
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1

Tactic:
simp_rw [exponent, dif_pos h]

Result:
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find h = 1

Proof state:
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find h = 1

Tactic:
exact (Nat.find_spec h).2 g

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem snd_unzip (as : Array (α × β)) : (Array.unzip as).snd = as.map Prod.snd

Proof state:
α : Type u_1
β : Type u_2
as : Array (α × β)
⊢ as.unzip.snd = map Prod.snd as

Tactic:
simp only [unzip]

Result:
α : Type u_1
β : Type u_2
as : Array (α × β)
⊢ (foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) as).snd = map Prod.snd as

Proof state:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ (foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) { toList := as }).snd =
    map Prod.snd { toList := as }

Tactic:
simp only [List.foldl_toArray']

Result:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ (List.foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) as).snd = map Prod.snd { toList := as }

Proof state:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ (List.foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) as).snd = map Prod.snd { toList := as }

Tactic:
rw [← List.foldl_hom (f := Prod.snd) (g₂ := fun bs x => bs.push x.2) (H := by simp), ← List.foldl_map]

Result:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ List.foldl push (#[], #[]).snd (List.map Prod.snd as) = map Prod.snd { toList := as }

Proof state:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ List.foldl push (#[], #[]).snd (List.map Prod.snd as) = map Prod.snd { toList := as }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
as : Array (α × β)
⊢ (foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) as).snd = map Prod.snd as

Tactic:
rcases as with ⟨as⟩

Result:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ (foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) { toList := as }).snd =
    map Prod.snd { toList := as }

Proof state:
α : Type u_1
β : Type u_2
as : List (α × β)
l : List (α × β)
init : Array α × Array β
⊢ ∀ (x : Array α × Array β) (y : α × β), (fun bs x => bs.push x.snd) x.snd y = (x.fst.push y.fst, x.snd.push y.snd).snd

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.equiv_refl {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) :
    hv.equiv hv (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E :=
  v.ext_linearIsometryEquiv fun i => by
    simp only [Orthonormal.equiv_apply, Equiv.coe_refl, id, LinearIsometryEquiv.coe_refl]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
i : ι
⊢ (hv.equiv hv (Equiv.refl ι)) (v i) = (LinearIsometryEquiv.refl 𝕜 E) (v i)

Tactic:
simp only [Orthonormal.equiv_apply, Equiv.coe_refl, id, LinearIsometryEquiv.coe_refl]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem Ioi_add_bij : BijOn (· + d) (Ioi a) (Ioi (a + d))

Proof state:
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ioi (a + d)
⊢ a + d + c ∈ (fun x => x + d) '' Ioi a

Tactic:
rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h

Result:
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a < a + c
⊢ a + d + c ∈ (fun x => x + d) '' Ioi a

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a < a + c
⊢ (fun x => x + d) (a + c) = a + d + c

Tactic:
rw [add_right_comm]

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d x✝ : M
h : x✝ ∈ Ioi (a + d)
⊢ x✝ ∈ (fun x => x + d) '' Ioi a

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le

Result:
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ioi (a + d)
⊢ a + d + c ∈ (fun x => x + d) '' Ioi a

Proof state:
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a < a + c
⊢ a + d + c ∈ (fun x => x + d) '' Ioi a

Tactic:
exact ⟨a + c, h, by rw [add_right_comm]⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d : M
⊢ BijOn (fun x => x + d) (Ioi a) (Ioi (a + d))

Tactic:
refine
  ⟨fun x h => add_lt_add_right (mem_Ioi.mp h) _, fun _ _ _ _ h => add_right_cancel h, fun _ h =>
    ?_⟩

Result:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a d x✝ : M
h : x✝ ∈ Ioi (a + d)
⊢ x✝ ∈ (fun x => x + d) '' Ioi a