harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.contDiff_comp_iff (e : G ≃L[𝕜] E) :
    ContDiff 𝕜 n (f ∘ e) ↔ ContDiff 𝕜 n f

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ ContDiffOn 𝕜 n (f ∘ ⇑e) (?m.459371 ⁻¹' univ) ↔ ContDiffOn 𝕜 n f univ

𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ Type ?u.459367

𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ G → ?m.459370

Tactic:
exact e.contDiffOn_comp_iff

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ ContDiff 𝕜 n (f ∘ ⇑e) ↔ ContDiff 𝕜 n f

Tactic:
rw [← contDiffOn_univ, ← contDiffOn_univ, ← preimage_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ ContDiffOn 𝕜 n (f ∘ ⇑e) (?m.459371 ⁻¹' univ) ↔ ContDiffOn 𝕜 n f univ

𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ Type ?u.459367

𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ G → ?m.459370
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_sub_left (d) : (∫ x in a..b, f (d - x)) = ∫ x in d - b..d - a, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d - x) = ∫ (x : ℝ) in d - b..d - a, f x

Tactic:
simpa only [one_mul, one_smul, inv_one] using integral_comp_sub_mul f one_ne_zero d

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Topology.lean
lemma autEmbedding_injective : Function.Injective (autEmbedding F)

Proof state:
case h.w.h.h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
X : C
x : (F.obj X).carrier
this : Iso.app σ X = Iso.app τ X
⊢ σ.hom.app X x = τ.hom.app X x

Tactic:
rw [← Iso.app_hom, ← Iso.app_hom, this]

Result:
no goals

Proof state:
case h.w.h.h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
X : C
x : (F.obj X).carrier
⊢ σ.hom.app X x = τ.hom.app X x

Tactic:
have : σ.app X = τ.app X := congr_fun h X

Result:
case h.w.h.h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
X : C
x : (F.obj X).carrier
this : Iso.app σ X = Iso.app τ X
⊢ σ.hom.app X x = τ.hom.app X x

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ Function.Injective ⇑(autEmbedding F)

Tactic:
intro σ τ h

Result:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
⊢ σ = τ

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
⊢ σ = τ

Tactic:
ext X x

Result:
case h.w.h.h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
X : C
x : (F.obj X).carrier
⊢ σ.hom.app X x = τ.hom.app X x
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_ball_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsAddHaarMeasure μ] (x : E) (r : ℝ) : μ (ball x r) = μ (ball (0 : E) r)

Proof state:
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
⊢ ball 0 r = (fun x_1 => x + x_1) ⁻¹' ball x r

Tactic:
simp [preimage_add_ball]

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
this : ball 0 r = (fun x_1 => x + x_1) ⁻¹' ball x r
⊢ μ (ball x r) = μ (ball 0 r)

Tactic:
rw [this, measure_preimage_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_eq_size {l : Array α} : count a l = l.size ↔ ∀ b ∈ l, a = b

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ count a l = l.size ↔ ∀ (b : α), b ∈ l → a = b

Tactic:
rw [count, countP_eq_size]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ (∀ (a_1 : α), a_1 ∈ l → (a_1 == a) = true) ↔ ∀ (b : α), b ∈ l → a = b

Proof state:
case refine_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : ∀ (b : α), b ∈ l → a = b
b : α
hb : b ∈ l
⊢ (b == a) = true

Tactic:
rw [h b hb, beq_self_eq_true]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : ∀ (a_1 : α), a_1 ∈ l → (a_1 == a) = true
b : α
hb : b ∈ l
⊢ b = a

Tactic:
simpa using h b hb

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ (∀ (a_1 : α), a_1 ∈ l → (a_1 == a) = true) ↔ ∀ (b : α), b ∈ l → a = b

Tactic:
refine ⟨fun h b hb => Eq.symm ?_, fun h b hb => ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : ∀ (a_1 : α), a_1 ∈ l → (a_1 == a) = true
b : α
hb : b ∈ l
⊢ b = a

case refine_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : ∀ (b : α), b ∈ l → a = b
b : α
hb : b ∈ l
⊢ (b == a) = true
-- Mathlib/Computability/Ackermann.lean
theorem ack_strictMono_right : ∀ m, StrictMono (ack m)
  | 0, n₁, n₂, h => by simpa using h
  | m + 1, 0, n + 1, _h => by
    rw [ack_succ_zero, ack_succ_succ]
    exact ack_strictMono_right _ (one_lt_ack_succ_left m n)
  | m + 1, n₁ + 1, n₂ + 1, h => by
    rw [ack_succ_succ, ack_succ_succ]
    apply ack_strictMono_right _ (ack_strictMono_right _ _)
    rwa [add_lt_add_iff_right] at h

Proof state:
m n : ℕ
_h : 0 < n + 1
⊢ ack (m + 1) 0 < ack (m + 1) (n + 1)

Tactic:
rw [ack_succ_zero, ack_succ_succ]

Result:
m n : ℕ
_h : 0 < n + 1
⊢ ack m 1 < ack m (ack (m + 1) n)

Proof state:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack (m + 1) (n₁ + 1) < ack (m + 1) (n₂ + 1)

Tactic:
rw [ack_succ_succ, ack_succ_succ]

Result:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)

Proof state:
n₁ n₂ : ℕ
h : n₁ < n₂
⊢ ack 0 n₁ < ack 0 n₂

Tactic:
simpa using h

Result:
no goals

Proof state:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)

Tactic:
apply ack_strictMono_right _ (ack_strictMono_right _ _)

Result:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ n₁ < n₂

Proof state:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ n₁ < n₂

Tactic:
rwa [add_lt_add_iff_right] at h

Result:
no goals

Proof state:
m n : ℕ
_h : 0 < n + 1
⊢ ack m 1 < ack m (ack (m + 1) n)

Tactic:
exact ack_strictMono_right _ (one_lt_ack_succ_left m n)

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem balancedCore_eq_iInter (hs : (0 : E) ∈ s) :
    balancedCore 𝕜 s = ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ 0 ∈ balancedCoreAux 𝕜 s

Tactic:
exact balancedCore_subset_balancedCoreAux (balancedCore_zero_mem hs)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ balancedCore 𝕜 s = ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • s

Tactic:
refine balancedCore_subset_balancedCoreAux.antisymm ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ balancedCoreAux 𝕜 s ⊆ balancedCore 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ balancedCoreAux 𝕜 s ⊆ balancedCore 𝕜 s

Tactic:
refine (balancedCoreAux_balanced ?_).subset_balancedCore_of_subset (balancedCoreAux_subset s)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ 0 ∈ balancedCoreAux 𝕜 s
-- Mathlib/Topology/Bornology/Constructions.lean
theorem isBounded_pi : IsBounded (pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ i, IsBounded (S i)

Proof state:
case pos
ι : Type u_3
π : ι → Type u_4
inst✝ : (i : ι) → Bornology (π i)
S : (i : ι) → Set (π i)
hne : ∃ i, S i = ∅
⊢ IsBounded (univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

Tactic:
simp [hne, univ_pi_eq_empty_iff.2 hne]

Result:
no goals

Proof state:
case neg
ι : Type u_3
π : ι → Type u_4
inst✝ : (i : ι) → Bornology (π i)
S : (i : ι) → Set (π i)
hne : (univ.pi S).Nonempty
⊢ IsBounded (univ.pi S) ↔ ∀ (i : ι), IsBounded (S i)

Tactic:
exact isBounded_pi_of_nonempty hne

Result:
no goals

Proof state:
case neg
ι : Type u_3
π : ι → Type u_4
inst✝ : (i : ι) → Bornology (π i)
S : (i : ι) → Set (π i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (univ.pi S) ↔ ∀ (i : ι), IsBounded (S i)

Tactic:
simp only [not_exists, ← Ne.eq_def, ← nonempty_iff_ne_empty, ← univ_pi_nonempty_iff] at hne

Result:
case neg
ι : Type u_3
π : ι → Type u_4
inst✝ : (i : ι) → Bornology (π i)
S : (i : ι) → Set (π i)
hne : (univ.pi S).Nonempty
⊢ IsBounded (univ.pi S) ↔ ∀ (i : ι), IsBounded (S i)

Proof state:
case neg
ι : Type u_3
π : ι → Type u_4
inst✝ : (i : ι) → Bornology (π i)
S : (i : ι) → Set (π i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

Tactic:
simp only [hne, false_or]

Result:
case neg
ι : Type u_3
π : ι → Type u_4
inst✝ : (i : ι) → Bornology (π i)
S : (i : ι) → Set (π i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (univ.pi S) ↔ ∀ (i : ι), IsBounded (S i)

Proof state:
ι : Type u_3
π : ι → Type u_4
inst✝ : (i : ι) → Bornology (π i)
S : (i : ι) → Set (π i)
⊢ IsBounded (univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

Tactic:
by_cases hne : ∃ i, S i = ∅

Result:
case pos
ι : Type u_3
π : ι → Type u_4
inst✝ : (i : ι) → Bornology (π i)
S : (i : ι) → Set (π i)
hne : ∃ i, S i = ∅
⊢ IsBounded (univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)

case neg
ι : Type u_3
π : ι → Type u_4
inst✝ : (i : ι) → Bornology (π i)
S : (i : ι) → Set (π i)
hne : ¬∃ i, S i = ∅
⊢ IsBounded (univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem dist_div_tan_angle_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2)
    (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) : dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂

Tactic:
rw [eq_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂

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

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, norm_div_tan_angle_add_of_inner_eq_zero h h0]

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Lattice.lean
theorem biUnion_diff_biUnion_eq {s t : Set ι} {f : ι → Set α} (h : (s ∪ t).PairwiseDisjoint f) :
    ((⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i) = ⋃ i ∈ s \ t, f i

Proof state:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i, ∃ (_ : i ∈ t), a ∈ f i

Tactic:
rintro ⟨j, hj, haj⟩

Result:
case intro.intro
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ False

Proof state:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ a ∉ ⋃ x ∈ t, f x

Tactic:
rw [mem_iUnion₂]

Result:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i, ∃ (_ : i ∈ t), a ∈ f i

Proof state:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
⊢ (⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f i

Tactic:
refine
  (biUnion_diff_biUnion_subset f s t).antisymm
    (iUnion₂_subset fun i hi a ha => (mem_diff _).2 ⟨mem_biUnion hi.1 ha, ?_⟩)

Result:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ a ∉ ⋃ x ∈ t, f x

Proof state:
case intro.intro
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ False

Tactic:
exact (h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
theorem Gamma1_in_Gamma0 (N : ℕ) : Gamma1 N ≤ Gamma0 N

Proof state:
N : ℕ
x : SL(2, ℤ)
HA : ↑(↑x 0 0) = 1 ∧ ↑(↑x 1 1) = 1 ∧ ↑(↑x 1 0) = 0
⊢ ↑(↑x 1 0) = 0

Tactic:
exact HA.2.2

Result:
no goals

Proof state:
N : ℕ
⊢ Gamma1 N ≤ Gamma0 N

Tactic:
intro x HA

Result:
N : ℕ
x : SL(2, ℤ)
HA : x ∈ Gamma1 N
⊢ x ∈ Gamma0 N

Proof state:
N : ℕ
x : SL(2, ℤ)
HA : x ∈ Gamma1 N
⊢ x ∈ Gamma0 N

Tactic:
simp only [Gamma0_mem, Gamma1_mem, coe_matrix_coe, Int.coe_castRingHom, map_apply] at *

Result:
N : ℕ
x : SL(2, ℤ)
HA : ↑(↑x 0 0) = 1 ∧ ↑(↑x 1 1) = 1 ∧ ↑(↑x 1 0) = 0
⊢ ↑(↑x 1 0) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v

Proof state:
case a
w v : Nat
x : BitVec w
h : w ≤ v
⊢ (setWidth' h x).toNat = (setWidth v x).toNat

Tactic:
rw [toNat_setWidth, toNat_setWidth']

Result:
case a
w v : Nat
x : BitVec w
h : w ≤ v
⊢ x.toNat = x.toNat % 2 ^ v

Proof state:
case a
w v : Nat
x : BitVec w
h : w ≤ v
⊢ x.toNat < 2 ^ v

Tactic:
exact Nat.lt_of_lt_of_le x.isLt (Nat.pow_le_pow_right (Nat.zero_lt_two) h)

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
h : w ≤ v
⊢ setWidth' h x = setWidth v x

Tactic:
apply eq_of_toNat_eq

Result:
case a
w v : Nat
x : BitVec w
h : w ≤ v
⊢ (setWidth' h x).toNat = (setWidth v x).toNat

Proof state:
case a
w v : Nat
x : BitVec w
h : w ≤ v
⊢ x.toNat = x.toNat % 2 ^ v

Tactic:
rw [Nat.mod_eq_of_lt]

Result:
case a
w v : Nat
x : BitVec w
h : w ≤ v
⊢ x.toNat < 2 ^ v
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem le_normalizer_comap (f : N →* G) :
    H.normalizer.comap f ≤ (H.comap f).normalizer := fun x => by
  simp only [mem_normalizer_iff, mem_comap]
  intro h n
  simp [h (f n)]

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
⊢ (∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H) → ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H

Tactic:
intro h n

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
h : ∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H
n : N
⊢ f n ∈ H ↔ f (x * n * x⁻¹) ∈ H

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
⊢ x ∈ comap f H.normalizer → x ∈ (comap f H).normalizer

Tactic:
simp only [mem_normalizer_iff, mem_comap]

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
⊢ (∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H) → ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
h : ∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H
n : N
⊢ f n ∈ H ↔ f (x * n * x⁻¹) ∈ H

Tactic:
simp [h (f n)]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem twoCocycles_map_one_fst (f : twoCocycles A) (g : G) :
    f (1, g) = f (1, 1)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
⊢ f (1, g) = f (1, 1)

Tactic:
have := ((mem_twoCocycles_iff f).1 f.2 1 1 g).symm

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
this : (A.ρ 1) (f (1, g)) + f (1, 1 * g) = f (1 * 1, g) + f (1, 1)
⊢ f (1, g) = f (1, 1)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
this : (A.ρ 1) (f (1, g)) + f (1, 1 * g) = f (1 * 1, g) + f (1, 1)
⊢ f (1, g) = f (1, 1)

Tactic:
simpa only [map_one, LinearMap.one_apply, one_mul, add_right_inj, this]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
theorem cofan_inj_πSummand_eq_zero [HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A B : IndexSet Δ)
    (h : B ≠ A) : (s.cofan Δ).inj A ≫ s.πSummand B = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ ((s.cofan Δ).inj A ≫ s.desc Δ fun B_1 => if h : B_1 = B then eqToHom ⋯ else 0) = 0

Tactic:
rw [ι_desc, dif_neg h.symm]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ (s.cofan Δ).inj A ≫ s.πSummand B = 0

Tactic:
dsimp [πSummand]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ ((s.cofan Δ).inj A ≫ s.desc Δ fun B_1 => if h : B_1 = B then eqToHom ⋯ else 0) = 0
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem ofFn_take_eq_take_ofFn {α : Type*} {m : ℕ} (h : m ≤ n) (v : Fin n → α) :
    List.ofFn (take m h v) = (List.ofFn v).take m :=
  List.ext_get (by simp [h]) (fun n h1 h2 => by simp)

Proof state:
n✝ : ℕ
α : Type u_2
m : ℕ
h : m ≤ n✝
v : Fin n✝ → α
n : ℕ
h1 : n < (List.ofFn (take m h v)).length
h2 : n < (List.take m (List.ofFn v)).length
⊢ (List.ofFn (take m h v)).get ⟨n, h1⟩ = (List.take m (List.ofFn v)).get ⟨n, h2⟩

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
α : Type u_2
m : ℕ
h : m ≤ n
v : Fin n → α
⊢ (List.ofFn (take m h v)).length = (List.take m (List.ofFn v)).length

Tactic:
simp [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem cramer_transpose_row_self (i : n) : Aᵀ.cramer (A i) = Pi.single i A.det

Proof state:
case pos
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
⊢ (Aᵀ.updateCol j (A j)).det = A.det

Tactic:
simp only [updateCol_transpose, det_transpose, updateRow_eq_self]

Result:
no goals

Proof state:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ (Aᵀ.updateCol j (A i)).det = 0

Tactic:
rw [updateCol_transpose, det_transpose]

Result:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ (A.updateRow j (A i)).det = 0

Proof state:
case pos
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : j = i
⊢ (Aᵀ.updateCol j (A i)).det = A.det

Tactic:
subst h

Result:
case pos
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
⊢ (Aᵀ.updateCol j (A j)).det = A.det

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
⊢ Aᵀ.cramer (A i) = Pi.single i A.det

Tactic:
ext j

Result:
case h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ Aᵀ.cramer (A i) j = Pi.single i A.det j

Proof state:
case h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (Aᵀ.updateCol j (A i)).det = if j = i then A.det else 0

Tactic:
split_ifs with h

Result:
case pos
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : j = i
⊢ (Aᵀ.updateCol j (A i)).det = A.det

case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ (Aᵀ.updateCol j (A i)).det = 0

Proof state:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ A.updateRow j (A i) j = A.updateRow j (A i) i

Tactic:
rw [updateRow_self, updateRow_ne (Ne.symm h)]

Result:
no goals

Proof state:
case h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ Aᵀ.cramer (A i) j = Pi.single i A.det j

Tactic:
rw [cramer_apply, Pi.single_apply]

Result:
case h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (Aᵀ.updateCol j (A i)).det = if j = i then A.det else 0

Proof state:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ (A.updateRow j (A i)).det = 0

Tactic:
apply det_zero_of_row_eq h

Result:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
h : ¬j = i
⊢ A.updateRow j (A i) j = A.updateRow j (A i) i