harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertManyIfNewUnit_cons {l : List α} {k : α} :
    (insertManyIfNewUnit m (k :: l)).1 = (insertManyIfNewUnit (m.insertIfNew k ()) l).1

Proof state:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
k : α
⊢ insertListIfNewUnitₘ m [k] = insertListIfNewUnitₘ (m.insertIfNew k ()) []

Tactic:
simp [insertListIfNewUnitₘ]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
l : List α
k : α
⊢ (insertManyIfNewUnit m (k :: l)).val = (insertManyIfNewUnit (m.insertIfNew k ()) l).val

Tactic:
simp only [insertManyIfNewUnit_eq_insertListIfNewUnitₘ]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
l : List α
k : α
⊢ insertListIfNewUnitₘ m (k :: l) = insertListIfNewUnitₘ (m.insertIfNew k ()) l

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
k hd : α
tl : List α
⊢ insertListIfNewUnitₘ m (k :: hd :: tl) = insertListIfNewUnitₘ (m.insertIfNew k ()) (hd :: tl)

Tactic:
simp [insertListIfNewUnitₘ]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
l : List α
k : α
⊢ insertListIfNewUnitₘ m (k :: l) = insertListIfNewUnitₘ (m.insertIfNew k ()) l

Tactic:
cases l with
| nil => simp [insertListIfNewUnitₘ]
| cons hd tl => simp [insertListIfNewUnitₘ]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem smul_graph (f : E →ₗ.[R] F) (z : M) :
    (z • f).graph =
      f.graph.map ((LinearMap.id : E →ₗ[R] E).prodMap (z • (LinearMap.id : F →ₗ[R] F)))

Proof state:
case h.mk.mp.intro.intro
R : Type u_1
inst✝⁷ : Ring R
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_3
inst✝⁴ : AddCommGroup F
inst✝³ : Module R F
M : Type u_5
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : ↑y = (x_fst, x_snd).1
h : z • ↑f y = (x_fst, x_snd).2
⊢ ∃ y ∈ f.graph, (LinearMap.id.prodMap (z • LinearMap.id)) y = (x_fst, x_snd)

Tactic:
simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id,
  LinearMap.smul_apply, Prod.mk.inj_iff, Prod.exists, exists_exists_and_eq_and]

Result:
case h.mk.mp.intro.intro
R : Type u_1
inst✝⁷ : Ring R
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_3
inst✝⁴ : AddCommGroup F
inst✝³ : Module R F
M : Type u_5
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : ↑y = (x_fst, x_snd).1
h : z • ↑f y = (x_fst, x_snd).2
⊢ ∃ a a_1, ↑a_1 = a ∧ a = x_fst ∧ z • ↑f a_1 = x_snd
-- Mathlib/Data/List/Basic.lean
theorem dropLast_append_getLast? : ∀ {l : List α}, ∀ a ∈ l.getLast?, dropLast l ++ [a] = l
  | [], a, ha => (Option.not_mem_none a ha).elim
  | [a], _, rfl => rfl
  | a :: b :: l, c, hc => by
    rw [getLast?_cons_cons] at hc
    rw [dropLast_cons₂, cons_append, dropLast_append_getLast? _ hc]

Proof state:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (a :: b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l

Tactic:
rw [getLast?_cons_cons] at hc

Result:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l

Proof state:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l

Tactic:
rw [dropLast_cons₂, cons_append, dropLast_append_getLast? _ hc]

Result:
no goals
-- Mathlib/Algebra/CharP/Basic.lean
lemma natCast_eq_natCast : (a : R) = b ↔ a ≡ b [MOD p]

Proof state:
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

Tactic:
wlog hle : a ≤ b

Result:
case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [inst_1 : CharP R p] {a b : ℕ} [inst_2 : IsRightCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a ≡ b [MOD p])
hle : ¬a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

Proof state:
case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [inst_1 : CharP R p] {a b : ℕ} [inst_2 : IsRightCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a ≡ b [MOD p])
hle : ¬a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

Tactic:
rw [eq_comm, this R p (le_of_not_le hle), Nat.ModEq.comm]

Result:
no goals

Proof state:
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

Tactic:
rw [Nat.modEq_iff_dvd' hle, ← cast_eq_zero_iff R p (b - a),
  ← add_right_cancel_iff (G := R) (a := a) (b := b - a), zero_add, ← Nat.cast_add,
  Nat.sub_add_cancel hle, eq_comm]

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem card_finset_fin_le {n : ℕ} (s : Finset (Fin n)) : #s ≤ n

Proof state:
n : ℕ
s : Finset (Fin n)
⊢ #s ≤ n

Tactic:
simpa only [Fintype.card_fin] using s.card_le_univ

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem map_eq_bot_iff {s : AffineSubspace k P₁} : s.map f = ⊥ ↔ s = ⊥

Proof state:
case refine_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : s = ⊥
⊢ map f s = ⊥

Tactic:
rw [h, map_bot]

Result:
no goals

Proof state:
case refine_1
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : map f s = ⊥
⊢ s = ⊥

Tactic:
rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h

Result:
no goals

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
⊢ map f s = ⊥ ↔ s = ⊥

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : map f s = ⊥
⊢ s = ⊥

case refine_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
h : s = ⊥
⊢ map f s = ⊥
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem map_surjective (hf : Function.Surjective f) :
    Function.Surjective (map f : MvPolynomial σ R → MvPolynomial σ S₁) := fun p => by
  induction' p using MvPolynomial.induction_on' with i fr a b ha hb
  · obtain ⟨r, rfl⟩ := hf fr
    exact ⟨monomial i r, map_monomial _ _ _⟩
  · obtain ⟨a, rfl⟩ := ha
    obtain ⟨b, rfl⟩ := hb
    exact ⟨a + b, RingHom.map_add _ _ _⟩

Proof state:
case h1.intro
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
i : σ →₀ ℕ
r : R
⊢ ∃ a, (map f) a = (monomial i) (f r)

Tactic:
exact ⟨monomial i r, map_monomial _ _ _⟩

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
p : MvPolynomial σ S₁
⊢ ∃ a, (map f) a = p

Tactic:
induction' p using MvPolynomial.induction_on' with i fr a b ha hb

Result:
case h1
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
i : σ →₀ ℕ
fr : S₁
⊢ ∃ a, (map f) a = (monomial i) fr

case h2
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
a b : MvPolynomial σ S₁
ha : ∃ a_1, (map f) a_1 = a
hb : ∃ a, (map f) a = b
⊢ ∃ a_1, (map f) a_1 = a + b

Proof state:
case h2.intro
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
b : MvPolynomial σ S₁
hb : ∃ a, (map f) a = b
a : MvPolynomial σ R
⊢ ∃ a_1, (map f) a_1 = (map f) a + b

Tactic:
obtain ⟨b, rfl⟩ := hb

Result:
case h2.intro.intro
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
a b : MvPolynomial σ R
⊢ ∃ a_1, (map f) a_1 = (map f) a + (map f) b

Proof state:
case h1
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
i : σ →₀ ℕ
fr : S₁
⊢ ∃ a, (map f) a = (monomial i) fr

Tactic:
obtain ⟨r, rfl⟩ := hf fr

Result:
case h1.intro
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
i : σ →₀ ℕ
r : R
⊢ ∃ a, (map f) a = (monomial i) (f r)

Proof state:
case h2
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
a b : MvPolynomial σ S₁
ha : ∃ a_1, (map f) a_1 = a
hb : ∃ a, (map f) a = b
⊢ ∃ a_1, (map f) a_1 = a + b

Tactic:
obtain ⟨a, rfl⟩ := ha

Result:
case h2.intro
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
b : MvPolynomial σ S₁
hb : ∃ a, (map f) a = b
a : MvPolynomial σ R
⊢ ∃ a_1, (map f) a_1 = (map f) a + b

Proof state:
case h2.intro.intro
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
a b : MvPolynomial σ R
⊢ ∃ a_1, (map f) a_1 = (map f) a + (map f) b

Tactic:
exact ⟨a + b, RingHom.map_add _ _ _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem if_true_left [h : Decidable p] :
    ite p True q ↔ ¬p → q

Proof state:
case isTrue
p q : Prop
g : p
⊢ (if p then True else q) ↔ ¬p → q

Tactic:
simp [g]

Result:
no goals

Proof state:
p q : Prop
h : Decidable p
⊢ (if p then True else q) ↔ ¬p → q

Tactic:
cases h <;> (rename_i g; simp [g])

Result:
no goals

Proof state:
case isTrue
p q : Prop
h✝ : p
⊢ (if p then True else q) ↔ ¬p → q

Tactic:
rename_i g

Result:
case isTrue
p q : Prop
g : p
⊢ (if p then True else q) ↔ ¬p → q
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_congr {f g : α → β} (h : f =ᵐ[μ] g) : Measure.map f μ = Measure.map g μ

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f μ
⊢ map f μ = map g μ

Tactic:
have hg : ¬AEMeasurable g μ := by simpa [← aemeasurable_congr h] using hf

Result:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f μ
hg : ¬AEMeasurable g μ
⊢ map f μ = map g μ

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ map f μ = map g μ

Tactic:
simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hg]

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ (mapₗ (AEMeasurable.mk f hf)) μ = (mapₗ (AEMeasurable.mk g hg)) μ

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
⊢ map f μ = map g μ

Tactic:
have hg : AEMeasurable g μ := hf.congr h

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ map f μ = map g μ

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ (mapₗ (AEMeasurable.mk f hf)) μ = (mapₗ (AEMeasurable.mk g hg)) μ

Tactic:
exact
  mapₗ_congr hf.measurable_mk hg.measurable_mk (hf.ae_eq_mk.symm.trans (h.trans hg.ae_eq_mk))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
⊢ map f μ = map g μ

Tactic:
by_cases hf : AEMeasurable f μ

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f μ
⊢ map f μ = map g μ

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f μ
⊢ map f μ = map g μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f μ
⊢ ¬AEMeasurable g μ

Tactic:
simpa [← aemeasurable_congr h] using hf

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f μ
hg : ¬AEMeasurable g μ
⊢ map f μ = map g μ

Tactic:
simp [map_of_not_aemeasurable, hf, hg]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem le_sub_one_of_lt (h : x < y) : x ≤ y - 1

Proof state:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : x < y
⊢ x ≤ y - 1

Tactic:
rw [← pred_eq_sub_one]

Result:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : x < y
⊢ x ≤ pred y

Proof state:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : x < y
⊢ x ≤ pred y

Tactic:
exact le_pred_of_lt h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_periodic : Function.Periodic tan π

Proof state:
⊢ Function.Periodic tan ↑π

Tactic:
simpa only [tan_eq_sin_div_cos] using sin_antiperiodic.div cos_antiperiodic

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

Proof state:
o : Ordering
⊢ o.swap = lt ↔ o = gt

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem rankD_push {arr : Array UFNode} :
    rankD (arr.push ⟨arr.size, 0⟩) a = rankD arr a

Proof state:
a : Nat
arr : Array UFNode
h1 : ¬a < arr.size + 1
h2 : a < arr.size
⊢ 0 = arr[a].rank

Tactic:
cases h1 (Nat.lt_succ_of_lt h2)

Result:
no goals

Proof state:
a : Nat
arr : Array UFNode
⊢ rankD (arr.push { parent := arr.size, rank := 0 }) a = rankD arr a

Tactic:
simp [rankD]

Result:
a : Nat
arr : Array UFNode
⊢ (if h : a < arr.size + 1 then (arr.push { parent := arr.size, rank := 0 })[a].rank else 0) =
    if h : a < arr.size then arr[a].rank else 0

Proof state:
case isFalse.isFalse
a : Nat
arr : Array UFNode
h✝¹ : ¬a < arr.size + 1
h✝ : ¬a < arr.size
⊢ 0 = 0

Tactic:
simp [Array.getElem_push, *]

Result:
no goals

Proof state:
case isFalse.isTrue
a : Nat
arr : Array UFNode
h✝¹ : ¬a < arr.size + 1
h✝ : a < arr.size
⊢ 0 = arr[a].rank

Tactic:
next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)

Result:
no goals

Proof state:
a : Nat
arr : Array UFNode
⊢ (if h : a < arr.size + 1 then (arr.push { parent := arr.size, rank := 0 })[a].rank else 0) =
    if h : a < arr.size then arr[a].rank else 0

Tactic:
split <;> split <;> try simp [Array.getElem_push, *]

Result:
case isFalse.isTrue
a : Nat
arr : Array UFNode
h✝¹ : ¬a < arr.size + 1
h✝ : a < arr.size
⊢ 0 = arr[a].rank
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem normalize_idem (x : α) : normalize (normalize x) = normalize x

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
x : α
⊢ normalize (normalize x) = normalize x

Tactic:
simp [normalize_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma transpose_isTotallyUnimodular_iff (A : Matrix m n R) :
    Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
constructor <;> apply IsTotallyUnimodular.transpose

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem ofComplex_comp_toComplex : ofComplex.comp toComplex = AlgHom.id ℝ (CliffordAlgebra Q)

Proof state:
case a.h

⊢ ((ofComplex.comp toComplex).toLinearMap ∘ₗ ι Q) 1 = ((AlgHom.id ℝ (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q) 1

Tactic:
dsimp only [LinearMap.comp_apply, Subtype.coe_mk, AlgHom.id_apply, AlgHom.toLinearMap_apply,
  AlgHom.comp_apply]

Result:
case a.h

⊢ ofComplex (toComplex ((ι Q) 1)) = (ι Q) 1

Proof state:
case a.h

⊢ ofComplex (toComplex ((ι Q) 1)) = (ι Q) 1

Tactic:
rw [toComplex_ι, one_smul, ofComplex_I]

Result:
no goals

Proof state:
⊢ ofComplex.comp toComplex = AlgHom.id ℝ (CliffordAlgebra Q)

Tactic:
ext

Result:
case a.h

⊢ ((ofComplex.comp toComplex).toLinearMap ∘ₗ ι Q) 1 = ((AlgHom.id ℝ (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q) 1
-- Mathlib/Data/Real/EReal.lean
private lemma exists_lt_mul_right_of_nonneg (ha : 0 ≤ a) (hc : 0 ≤ c) (h : c < a * b) :
    ∃ b' ∈ Ico 0 b, c < a * b'

Proof state:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Ico 0 b, c < b' * a

Tactic:
exact exists_lt_mul_left_of_nonneg hb.le hc h

Result:
no goals

Proof state:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ b' ∈ Ico 0 b, c < a * b'

Tactic:
have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha

Result:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Ico 0 b, c < a * b'

Proof state:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Ico 0 b, c < a * b'

Tactic:
simp_rw [mul_comm a] at h ⊢

Result:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Ico 0 b, c < b' * a
-- Mathlib/GroupTheory/GroupAction/Basic.lean
theorem Equiv.swap_mem_stabilizer {α : Type*} [DecidableEq α] {S : Set α} {a b : α} :
    Equiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) S ↔ (a ∈ S ↔ b ∈ S)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ swap a b ∈ MulAction.stabilizer (Perm α) S ↔ (a ∈ S ↔ b ∈ S)

Tactic:
rw [MulAction.mem_stabilizer_iff, Set.ext_iff, ← swap_inv]

Result:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (∀ (x : α), x ∈ (swap a b)⁻¹ • S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
⊢ (if x✝ = a then b else if x✝ = b then a else x✝) ∈ S ↔ x✝ ∈ S

Tactic:
split_ifs <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (∀ (x : α), x ∈ (swap a b)⁻¹ • S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)

Tactic:
simp_rw [Set.mem_inv_smul_set_iff, Perm.smul_def, swap_apply_def]

Result:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (a ∈ S ↔ b ∈ S) → ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S

Tactic:
intros

Result:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
⊢ (if x✝ = a then b else if x✝ = b then a else x✝) ∈ S ↔ x✝ ∈ S

Proof state:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
h : ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S
⊢ a ∈ S ↔ b ∈ S

Tactic:
simpa [Iff.comm] using h a

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)

Tactic:
exact ⟨fun h ↦ by simpa [Iff.comm] using h a, by intros; split_ifs <;> simp [*]⟩

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_pos : 0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ (¬∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C) ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
simp only [not_forall, not_exists, not_lt, exists_prop, not_and]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
rw [pos_iff_ne_zero, Ne, einfsep_zero]

Result:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ (¬∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C) ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc]
lemma counitIso_inv_app_tensor_comp_functor_map_δ_inverse (X Y : C) :
    e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
      e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y)) =
      μ e.functor X Y ≫ e.functor.map (e.unitIso.hom.app X ⊗ e.unitIso.hom.app Y)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ δ e.functor X Y ≫
      e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
        e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y)) =
    e.functor.map (e.unitIso.hom.app X ⊗ e.unitIso.hom.app Y)

Tactic:
apply e.inverse.map_injective

Result:
case a
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ e.inverse.map
      (δ e.functor X Y ≫
        e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
          e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y))) =
    e.inverse.map (e.functor.map (e.unitIso.hom.app X ⊗ e.unitIso.hom.app Y))

Proof state:
case a
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ e.inverse.map
      (δ e.functor X Y ≫
        e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
          e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y))) =
    e.inverse.map (e.functor.map (e.unitIso.hom.app X ⊗ e.unitIso.hom.app Y))

Tactic:
simp [← cancel_epi (e.unitIso.hom.app (X ⊗ Y)), Functor.map_comp,
  unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
      e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y)) =
    μ e.functor X Y ≫ e.functor.map (e.unitIso.hom.app X ⊗ e.unitIso.hom.app Y)

Tactic:
rw [← cancel_epi (δ e.functor _ _), Monoidal.δ_μ_assoc]

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
X Y : C
⊢ δ e.functor X Y ≫
      e.counitIso.inv.app (e.functor.obj X ⊗ e.functor.obj Y) ≫
        e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y)) =
    e.functor.map (e.unitIso.hom.app X ⊗ e.unitIso.hom.app Y)
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_of_le {a b : α} (h : a ≤ b) : a ∆ b = b \ a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : a ≤ b
⊢ a ∆ b = b \ a

Tactic:
rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]

Result:
no goals