harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dot_of_left_zero (w : ∀ x, x ∈ xs → x = 0) : dot xs ys = 0

Proof state:
case cons.cons
x : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x_1 : Int), x_1 ∈ x :: xs → x_1 = 0
y : Int
ys : List Int
⊢ 0 * y + 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case cons.nil
x : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x_1 : Int), x_1 ∈ x :: xs → x_1 = 0
⊢ dot (x :: xs) [] = 0

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons.a
x✝ : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x : Int), x ∈ x✝ :: xs → x = 0
y : Int
ys : List Int
x : Int
m : x ∈ xs
⊢ x ∈ x✝ :: xs

Tactic:
exact List.mem_cons_of_mem _ m

Result:
no goals

Proof state:
case nil
ys : IntList
w : ∀ (x : Int), x ∈ [] → x = 0
⊢ dot [] ys = 0

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
x : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x_1 : Int), x_1 ∈ x :: xs → x_1 = 0
y : Int
ys : List Int
⊢ ∀ (x : Int), x ∈ xs → x = 0

Tactic:
intro x m

Result:
case cons.cons
x✝ : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x : Int), x ∈ x✝ :: xs → x = 0
y : Int
ys : List Int
x : Int
m : x ∈ xs
⊢ x = 0

Proof state:
case cons.cons
x✝ : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x : Int), x ∈ x✝ :: xs → x = 0
y : Int
ys : List Int
x : Int
m : x ∈ xs
⊢ x = 0

Tactic:
apply w

Result:
case cons.cons.a
x✝ : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x : Int), x ∈ x✝ :: xs → x = 0
y : Int
ys : List Int
x : Int
m : x ∈ xs
⊢ x ∈ x✝ :: xs

Proof state:
x : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x_1 : Int), x_1 ∈ x :: xs → x_1 = 0
y : Int
ys : List Int
⊢ x ∈ x :: xs

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
x : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x_1 : Int), x_1 ∈ x :: xs → x_1 = 0
y : Int
ys : List Int
⊢ dot (x :: xs) (y :: ys) = 0

Tactic:
rw [dot_cons₂, w x (by simp), ih]

Result:
case cons.cons
x : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x_1 : Int), x_1 ∈ x :: xs → x_1 = 0
y : Int
ys : List Int
⊢ 0 * y + 0 = 0

case cons.cons
x : Int
xs : List Int
ih : ∀ {ys : IntList}, (∀ (x : Int), x ∈ xs → x = 0) → dot xs ys = 0
w : ∀ (x_1 : Int), x_1 ∈ x :: xs → x_1 = 0
y : Int
ys : List Int
⊢ ∀ (x : Int), x ∈ xs → x = 0
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem measure_condCDF_univ (ρ : Measure (α × ℝ)) (a : α) : (condCDF ρ a).measure univ = 1

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ (condCDF ρ a).measure univ = ENNReal.ofReal (1 - 0)

Tactic:
exact StieltjesFunction.measure_univ _ (tendsto_condCDF_atBot ρ a) (tendsto_condCDF_atTop ρ a)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ (condCDF ρ a).measure univ = 1

Tactic:
rw [← ENNReal.ofReal_one, ← sub_zero (1 : ℝ)]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ (condCDF ρ a).measure univ = ENNReal.ofReal (1 - 0)
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_eq_map [RingHomSurjective τ₁₂] (f : F) : range f = map f ⊤

Proof state:
case h
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 : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
x✝ : M₂
⊢ x✝ ∈ range f ↔ x✝ ∈ map f ⊤

Tactic:
simp

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 : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
⊢ range f = map f ⊤

Tactic:
ext

Result:
case h
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 : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
x✝ : M₂
⊢ x✝ ∈ range f ↔ x✝ ∈ map f ⊤
-- Mathlib/Algebra/QuadraticDiscriminant.lean
theorem discrim_eq_zero_iff (ha : a ≠ 0) :
    discrim a b c = 0 ↔ (∃! x, a * (x * x) + b * x + c = 0)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
⊢ discrim a b c = 0 ↔ ∃! x, a * (x * x) + b * x + c = 0

Tactic:
refine ⟨fun hd => ?_, discrim_eq_zero_of_existsUnique ha⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
hd : discrim a b c = 0
⊢ ∃! x, a * (x * x) + b * x + c = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
hd : discrim a b c = 0
⊢ ∃! x, a * (x * x) + b * x + c = 0

Tactic:
simp_rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha hd, existsUnique_eq]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem imaginaryPart_smul (z : ℂ) (a : A) : ℑ (z • a) = z.re • ℑ a + z.im • ℜ a

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ℑ (z • a) = z.re • ℑ a + z.im • ℜ a

Tactic:
have := by congrm (ℑ ($((re_add_im z).symm) • a))

Result:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
this : ℑ (z • a) = ℑ ((↑z.re + ↑z.im * I) • a)
⊢ ℑ (z • a) = z.re • ℑ a + z.im • ℜ a

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
this : ℑ (z • a) = ℑ ((↑z.re + ↑z.im * I) • a)
⊢ ℑ (z • a) = z.re • ℑ a + z.im • ℜ a

Tactic:
simpa [-re_add_im, add_smul, ← smul_smul]

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ?m.175621

Tactic:
congrm (ℑ ($((re_add_im z).symm) • a))

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem sum_cramer_apply {β} (s : Finset β) (f : n → β → α) (i : n) :
    (∑ x ∈ s, cramer A (fun j => f j x) i) = cramer A (fun j : n => ∑ x ∈ s, f j x) i :=
  calc
    (∑ x ∈ s, cramer A (fun j => f j x) i) = (∑ x ∈ s, cramer A fun j => f j x) i :=
      (Finset.sum_apply i s _).symm
    _ = cramer A (fun j : n => ∑ x ∈ s, f j x) i

Proof state:
case e_M.h.e_6.h.h.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i j x✝ : n
⊢ Function.update (A j) i ((∑ x ∈ s, fun j => f j x) j) x✝ = Function.update (A j) i (∑ x ∈ s, f j x) x✝

Tactic:
congr

Result:
case e_M.h.e_6.h.h.h.e_v
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i j x✝ : n
⊢ (∑ x ∈ s, fun j => f j x) j = ∑ x ∈ s, f j x

Proof state:
case e_M.h.e_6.h.h.h.e_v
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i j x✝ : n
⊢ (∑ x ∈ s, fun j => f j x) j = ∑ x ∈ s, f j x

Tactic:
apply Finset.sum_apply

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ (A.updateCol i (∑ x ∈ s, fun j => f j x)).det = (A.updateCol i fun j => ∑ x ∈ s, f j x).det

Tactic:
simp only [updateCol]

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ (of fun i_1 => Function.update (A i_1) i ((∑ x ∈ s, fun j => f j x) i_1)).det =
    (of fun i_1 => Function.update (A i_1) i (∑ x ∈ s, f i_1 x)).det

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ (of fun i_1 => Function.update (A i_1) i ((∑ x ∈ s, fun j => f j x) i_1)).det =
    (of fun i_1 => Function.update (A i_1) i (∑ x ∈ s, f i_1 x)).det

Tactic:
congr with j

Result:
case e_M.h.e_6.h.h.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i j x✝ : n
⊢ Function.update (A j) i ((∑ x ∈ s, fun j => f j x) j) x✝ = Function.update (A j) i (∑ x ∈ s, f j x) x✝

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ (∑ x ∈ s, A.cramer fun j => f j x) i = A.cramer (fun j => ∑ x ∈ s, f j x) i

Tactic:
rw [sum_cramer, cramer_apply, cramer_apply]

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ (A.updateCol i (∑ x ∈ s, fun j => f j x)).det = (A.updateCol i fun j => ∑ x ∈ s, f j x).det
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem Nodup.isCycleOn_formPerm (h : l.Nodup) :
    l.formPerm.IsCycleOn { a | a ∈ l }

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : a ∈ {a | a ∈ l}
b : α
hb : b ∈ {a | a ∈ l}
⊢ l.formPerm.SameCycle a b

Tactic:
rw [Set.mem_setOf, ← List.idxOf_lt_length_iff] at ha hb

Result:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle a b

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l[(idxOf a l + idxOf b l) % l.length] = l[(idxOf b l + idxOf a l) % l.length]

Tactic:
rw [add_comm]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ (l.formPerm ^ (↑(idxOf b l) - ↑(idxOf a l))) l[idxOf a l] = l[idxOf b l]

Tactic:
simp only [sub_eq_neg_add, zpow_add, zpow_neg, Equiv.Perm.inv_eq_iff_eq, zpow_natCast,
  Equiv.Perm.coe_mul, List.formPerm_pow_apply_getElem _ h, Function.comp]

Result:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l[(idxOf a l + idxOf b l) % l.length] = l[(idxOf b l + idxOf a l) % l.length]

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ l.formPerm.IsCycleOn {a | a ∈ l}

Tactic:
refine ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => ?_⟩

Result:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : a ∈ {a | a ∈ l}
b : α
hb : b ∈ {a | a ∈ l}
⊢ l.formPerm.SameCycle a b

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle l[idxOf a l] l[idxOf b l]

Tactic:
refine ⟨l.idxOf b - l.idxOf a, ?_⟩

Result:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ (l.formPerm ^ (↑(idxOf b l) - ↑(idxOf a l))) l[idxOf a l] = l[idxOf b l]

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle a b

Tactic:
rw [← List.getElem_idxOf ha, ← List.getElem_idxOf hb]

Result:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle l[idxOf a l] l[idxOf b l]
-- Mathlib/Algebra/Order/GroupWithZero/Finset.lean
lemma sup_div₀ [LinearOrderedCommGroupWithZero G₀] [OrderBot G₀] {a : G₀} (ha : 0 < a)
    (s : Finset ι) (f : ι → G₀) : s.sup f / a = s.sup fun i ↦ f i / a

Proof state:
ι : Type u_1
G₀ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : OrderBot G₀
a : G₀
ha : 0 < a
s : Finset ι
f : ι → G₀
⊢ s.sup f / a = s.sup fun i => f i / a

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl
ι : Type u_1
G₀ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : OrderBot G₀
a : G₀
ha : 0 < a
f : ι → G₀
⊢ ∅.sup f / a = ∅.sup fun i => f i / a

case inr
ι : Type u_1
G₀ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : OrderBot G₀
a : G₀
ha : 0 < a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup f / a = s.sup fun i => f i / a

Proof state:
case inl
ι : Type u_1
G₀ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : OrderBot G₀
a : G₀
ha : 0 < a
f : ι → G₀
⊢ ∅.sup f / a = ∅.sup fun i => f i / a

Tactic:
simp [← show (0 : G₀) = ⊥ from bot_unique zero_le']

Result:
no goals

Proof state:
case inr
ι : Type u_1
G₀ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : OrderBot G₀
a : G₀
ha : 0 < a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup f / a = s.sup fun i => f i / a

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_div₀ (ha := ha)]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finrank.lean
theorem finrank_top : finrank R (⊤ : Submodule R M) = finrank R M

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ finrank R ↥⊤ = finrank R M

Tactic:
unfold finrank

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ toNat (Module.rank R ↥⊤) = toNat (Module.rank R M)

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ toNat (Module.rank R ↥⊤) = toNat (Module.rank R M)

Tactic:
simp [rank_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
    (rupHints : Array Nat) :
    restoreAssignments (performRupCheck f rupHints).1.assignments (performRupCheck f rupHints).2.1
      =
    f.assignments

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f' : DefaultFormula n := (f.performRupCheck rupHints).fst
f'_def : f' = (f.performRupCheck rupHints).fst
⊢ f'.assignments.size = n

Tactic:
rw [size_assignments_performRupCheck f rupHints, f_assignments_size]

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f' : DefaultFormula n := (f.performRupCheck rupHints).fst
f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : CNF.Clause (PosFin n)
derivedLits_satisfies_invariant :
  f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size derivedLits
derivedLits_arr : Array (Literal (PosFin n)) := { toList := derivedLits }
⊢ Array.foldl clearUnit f'.assignments { toList := derivedLits } = f.assignments

Tactic:
have derivedLits_arr_def : derivedLits_arr = {toList := derivedLits} := rfl

Result:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f' : DefaultFormula n := (f.performRupCheck rupHints).fst
f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : CNF.Clause (PosFin n)
derivedLits_satisfies_invariant :
  f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size derivedLits
derivedLits_arr : Array (Literal (PosFin n)) := { toList := derivedLits }
derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }
⊢ Array.foldl clearUnit f'.assignments { toList := derivedLits } = f.assignments
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive (attr := simp) abs_pos] lemma one_lt_mabs : 1 < |a|ₘ ↔ a ≠ 1

Proof state:
case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : a < 1
⊢ 1 < mabs a ↔ a ≠ 1

Tactic:
simp [mabs_of_lt_one ha, neg_pos, ha.ne, ha]

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
⊢ 1 < mabs 1 ↔ 1 ≠ 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ 1 < mabs a ↔ a ≠ 1

Tactic:
obtain ha | rfl | ha := lt_trichotomy a 1

Result:
case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : a < 1
⊢ 1 < mabs a ↔ a ≠ 1

case inr.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
⊢ 1 < mabs 1 ↔ 1 ≠ 1

case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < mabs a ↔ a ≠ 1

Proof state:
case inr.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
ha : 1 < a
⊢ 1 < mabs a ↔ a ≠ 1

Tactic:
simp [mabs_of_one_lt ha, ha, ha.ne']

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem even_odd_of_coprime (hc : Int.gcd x y = 1) :
    x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

Proof state:
case inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ False

Tactic:
obtain ⟨x0, y0, rfl, rfl⟩ : ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1 := by
  obtain ⟨x0, hx2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_sub_of_emod_eq hx)
  obtain ⟨y0, hy2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_sub_of_emod_eq hy)
  rw [sub_eq_iff_eq_add] at hx2 hy2
  exact ⟨x0, y0, hx2, hy2⟩

Result:
case inr.inr.intro.intro.intro
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ False

Proof state:
case inr.inr.intro.intro.intro
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ 2 % 4 % 4 = 2

Tactic:
decide

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma Connected.adj_union {H K : G.Subgraph}
    (Hconn : H.Connected) (Kconn : K.Connected) {u v : V} (uH : u ∈ H.verts) (vK : v ∈ K.verts)
    (huv : G.Adj u v) :
    ((⊤ : G.Subgraph).induce {u, v} ⊔ H ⊔ K).Connected

Proof state:
case refine_2
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Connected
Kconn : K.Connected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ ((⊤.induce {u, v} ⊔ H) ⊓ K).verts.Nonempty

Tactic:
exact ⟨v, by simp [vK]⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Connected
Kconn : K.Connected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ u ∈ (⊤.induce {u, v} ⊓ H).verts

Tactic:
simp [uH]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Connected
Kconn : K.Connected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (⊤.induce {u, v} ⊔ H ⊔ K).Connected

Tactic:
refine ((top_induce_pair_connected_of_adj huv).sup Hconn ?_).sup Kconn ?_

Result:
case refine_1
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Connected
Kconn : K.Connected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (⊤.induce {u, v} ⊓ H).verts.Nonempty

case refine_2
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Connected
Kconn : K.Connected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ ((⊤.induce {u, v} ⊔ H) ⊓ K).verts.Nonempty

Proof state:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Connected
Kconn : K.Connected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ v ∈ ((⊤.induce {u, v} ⊔ H) ⊓ K).verts

Tactic:
simp [vK]

Result:
no goals

Proof state:
case refine_1
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Connected
Kconn : K.Connected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (⊤.induce {u, v} ⊓ H).verts.Nonempty

Tactic:
exact ⟨u, by simp [uH]⟩

Result:
no goals
-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma ball_eq_of_mem {x y : X} {r : ℝ} (h : y ∈ ball x r) : ball x r = ball y r

Proof state:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
⊢ dist a x < r ↔ dist a y < r

Tactic:
constructor <;> intro h' <;>
exact (dist_triangle_max _ _ _).trans_lt (max_lt h' (dist_comm x _ ▸ h))

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ ball x r
⊢ ball x r = ball y r

Tactic:
ext a

Result:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ ball x r
a : X
⊢ a ∈ ball x r ↔ a ∈ ball y r

Proof state:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ ball x r
a : X
⊢ a ∈ ball x r ↔ a ∈ ball y r

Tactic:
simp_rw [mem_ball] at h ⊢

Result:
case h
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
a : X
h : dist y x < r
⊢ dist a x < r ↔ dist a y < r
-- Mathlib/Algebra/Group/Defs.lean
theorem mul_div_assoc (a b c : G) : a * b / c = a * (b / c)

Proof state:
G : Type u_1
inst✝ : DivInvMonoid G
a b c : G
⊢ a * b / c = a * (b / c)

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc _ _ _]

Result:
no goals