harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem mt (h : UniqueMul A B a0 b0) :
    ∀ ⦃a b⦄, a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a * b ≠ a0 * b0 := fun _ _ ha hb k ↦ by
  contrapose! k
  exact h ha hb k

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
ha : x✝¹ ∈ A
hb : x✝ ∈ B
k : x✝¹ ≠ a0 ∨ x✝ ≠ b0
⊢ x✝¹ * x✝ ≠ a0 * b0

Tactic:
contrapose! k

Result:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
ha : x✝¹ ∈ A
hb : x✝ ∈ B
k : x✝¹ * x✝ = a0 * b0
⊢ x✝¹ = a0 ∧ x✝ = b0

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
ha : x✝¹ ∈ A
hb : x✝ ∈ B
k : x✝¹ * x✝ = a0 * b0
⊢ x✝¹ = a0 ∧ x✝ = b0

Tactic:
exact h ha hb k

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
@[simp]
lemma rightUnitor_inv_app (F : J ⥤ C) (j : J) :
    (ρ_ F).inv.app j = (ρ_ (F.obj j)).inv

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F : J ⥤ C
j : J
⊢ (ρ_ F).inv.app j = (ρ_ (F.obj j)).inv

Tactic:
rw [← cancel_mono ((ρ_ (F.obj j)).hom), Iso.inv_hom_id, ← rightUnitor_hom_app,
  Iso.inv_hom_id_app]

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/Basic.lean
theorem comp.get_mk (x : P (fun i => Q i α)) : comp.get (comp.mk x) = x

Proof state:
n m : ℕ
P : MvPFunctor.{u} n
Q : Fin2 n → MvPFunctor.{u} m
α : TypeVec.{u} m
x : ↑P fun i => ↑(Q i) α
⊢ get (mk x) = x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/InvariantForm.lean
lemma restrict_orthogonal_nondegenerate (I : LieIdeal K L) (hI : IsAtom I) :
    (Φ.restrict (orthogonal Φ hΦ_inv I)).Nondegenerate

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ (Φ.restrict (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule).Nondegenerate

Tactic:
rw [LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal hΦ_refl]

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule
    (Φ.orthogonal (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule
    (Φ.orthogonal (LieIdeal.toLieSubalgebra K L (orthogonal Φ hΦ_inv I)).toSubmodule)

Tactic:
simp only [LieIdeal.toLieSubalgebra_toSubmodule, orthogonal_toSubmodule,
  LinearMap.BilinForm.orthogonal_orthogonal hΦ_nondeg hΦ_refl]

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (Φ.orthogonal ↑I) ↑I

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl (Φ.orthogonal ↑I) ↑I

Tactic:
exact (orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI).symm

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem zneg_zneg (n : ZNum) : - -n = n

Proof state:
n : ZNum
⊢ - -n = n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- A twisted version of the relation `Λ * ↑ζ = log` in terms of complex sequences. -/
lemma convolution_twist_vonMangoldt {N : ℕ} (χ : DirichletCharacter ℂ N) :
    (↗χ * ↗Λ) ⍟ ↗χ = ↗χ * ↗Complex.log

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
⊢ (((fun n => χ ↑n) * fun n => ↑(Λ n)) ⍟ fun n => χ ↑n) = (fun n => χ ↑n) * fun n => Complex.log ↑n

Tactic:
rw [← convolution_vonMangoldt_const_one, ← χ.mul_convolution_distrib, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insertIfNew k v).1.size ≤ m.1.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ (m.insertIfNew k v).val.size ≤ m.val.size + 1

Tactic:
simp_to_model [insertIfNew] using List.length_insertEntryIfNew_le

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem coe_inj (H : (f : V₁ → V₂) = g) : f = g

Proof state:
case mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
g : NormedAddGroupHom V₁ V₂
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H : ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = ⇑g
⊢ { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = g

Tactic:
cases g

Result:
case mk.mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
toFun✝¹ : V₁ → V₂
map_add'✝¹ : ∀ (v₁ v₂ : V₁), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : V₁), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H :
  ⇑{ toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }

Proof state:
case mk.mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
toFun✝¹ : V₁ → V₂
map_add'✝¹ : ∀ (v₁ v₂ : V₁), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : V₁), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H :
  ⇑{ toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }

Tactic:
congr

Result:
no goals

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
H : ⇑f = ⇑g
⊢ f = g

Tactic:
cases f

Result:
case mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
g : NormedAddGroupHom V₁ V₂
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H : ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = ⇑g
⊢ { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = g
-- Mathlib/Data/Complex/Norm.lean
theorem sq_norm_sub_sq_re (z : ℂ) : ‖z‖ ^ 2 - z.re ^ 2 = z.im ^ 2

Proof state:
z : ℂ
⊢ ‖z‖ ^ 2 - z.re ^ 2 = z.im ^ 2

Tactic:
rw [Complex.sq_norm, normSq_apply, ← sq, ← sq, add_sub_cancel_left]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_ulift : finrank R (ULift M) = finrank R M

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ finrank R (ULift.{u_2, v} M) = finrank R M

Tactic:
simp_rw [finrank, rank_ulift, toNat_lift]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_le_mk_mul_of_mk_preimage_le {c : Cardinal} (f : α → β) (hf : ∀ b : β, #(f ⁻¹' {b}) ≤ c) :
    #α ≤ #β * c

Proof state:
α β : Type u
c : Cardinal.{u}
f : α → β
hf : ∀ (b : β), #↑(f ⁻¹' {b}) ≤ c
⊢ #α ≤ #β * c

Tactic:
simpa only [← mk_congr (@Equiv.sigmaFiberEquiv α β f), mk_sigma, ← sum_const'] using
  sum_le_sum _ _ hf

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem restrict_restrict_eq {R₁ R₂ : Set α} (M : Matroid α) (hR : R₂ ⊆ R₁) :
    (M ↾ R₁) ↾ R₂ = M ↾ R₂

Proof state:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ M ↾ R₁ ↾ R₂ = M ↾ R₂

Tactic:
refine ext_indep rfl ?_

Result:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ ∀ ⦃I : Set α⦄, I ⊆ (M ↾ R₁ ↾ R₂).E → ((M ↾ R₁ ↾ R₂).Indep I ↔ (M ↾ R₂).Indep I)

Proof state:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ ∀ ⦃I : Set α⦄, I ⊆ R₂ → I ⊆ R₂ → M.Indep I → I ⊆ R₁

Tactic:
exact fun _ h _ _ ↦ h.trans hR

Result:
no goals

Proof state:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ ∀ ⦃I : Set α⦄, I ⊆ (M ↾ R₁ ↾ R₂).E → ((M ↾ R₁ ↾ R₂).Indep I ↔ (M ↾ R₂).Indep I)

Tactic:
simp only [restrict_ground_eq, restrict_indep_iff, and_congr_left_iff, and_iff_left_iff_imp]

Result:
α : Type u_1
R₁ R₂ : Set α
M : Matroid α
hR : R₂ ⊆ R₁
⊢ ∀ ⦃I : Set α⦄, I ⊆ R₂ → I ⊆ R₂ → M.Indep I → I ⊆ R₁
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.zero_beq_xor_iff (a b : BitVec w) : (0#w == a ^^^ b) = (a == b)

Proof state:
w : Nat
a b : BitVec w
⊢ (0#w == a ^^^ b) = (a == b)

Tactic:
rw [Bool.eq_iff_iff, beq_iff_eq, Eq.comm]

Result:
w : Nat
a b : BitVec w
⊢ a ^^^ b = 0#w ↔ (a == b) = true

Proof state:
w : Nat
a b : BitVec w
⊢ a ^^^ b = 0#w ↔ (a == b) = true

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem get!_eq_getValueCast! [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.1)
    {a : α} [Inhabited (β a)] : m.get! a = getValueCast! a (toListModel m.1.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
inst✝ : Inhabited (β a)
⊢ m.get! a = getValueCast! a (toListModel m.val.buckets)

Tactic:
rw [get!_eq_get!ₘ, get!ₘ_eq_getValueCast! hm]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem centroid_singleton (p : ι → P) (i : ι) : ({i} : Finset ι).centroid k p = p i

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
⊢ centroid k {i} p = p i

Tactic:
simp [centroid_def, affineCombination_apply]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_submatrix_sum_swap_left (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α)
    (D : Matrix o m α) (f : p → l ⊕ m) :
    (fromBlocks A B C D).submatrix Sum.swap f = (fromBlocks C D A B).submatrix id f

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
⊢ (fromBlocks A B C D).submatrix Sum.swap f = (fromBlocks C D A B).submatrix id f

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
i : o ⊕ n
j : p
⊢ (fromBlocks A B C D).submatrix Sum.swap f i j = (fromBlocks C D A B).submatrix id f i j

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
i : o ⊕ n
j : p
⊢ (fromBlocks A B C D).submatrix Sum.swap f i j = (fromBlocks C D A B).submatrix id f i j

Tactic:
cases i <;> dsimp <;> cases f j <;> rfl

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Basic.lean
theorem liftCover_restrict {i : ι} : (liftCover S φ hφ hS).restrict (S i) = φ i

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
i : ι
⊢ restrict (S i) (liftCover S φ hφ hS) = φ i

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
i : ι
a✝ : ↑(S i)
⊢ (restrict (S i) (liftCover S φ hφ hS)) a✝ = (φ i) a✝

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
i : ι
a✝ : ↑(S i)
⊢ (restrict (S i) (liftCover S φ hφ hS)) a✝ = (φ i) a✝

Tactic:
simp only [coe_restrict, Function.comp_apply, liftCover_coe]

Result:
no goals
-- Mathlib/CategoryTheory/Monad/Comonadicity.lean
theorem comparisonAdjunction_counit_f
    [∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a)
      (adj.unit.app (G.obj A.A))]
    (A : adj.toComonad.Coalgebra) :
    ((comparisonAdjunction adj).counit.app A).f = (beckEqualizer A).lift (counitFork A)

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A : adj.toComonad.Coalgebra
⊢ ((comparisonAdjunction adj).counit.app A).f = (beckEqualizer A).lift (counitFork A)

Tactic:
simp [Adjunction.homEquiv_counit]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem or_right_comm : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b

Proof state:
a b c : Prop
⊢ (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b

Tactic:
rw [or_assoc, or_assoc, @or_comm b]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem inv_subset : s⁻¹ ⊆ t ↔ s ⊆ t⁻¹

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
s t : Set α
⊢ s⁻¹ ⊆ t ↔ s ⊆ t⁻¹

Tactic:
rw [← inv_subset_inv, inv_inv]

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem nodup_reverse {l : List α} : Nodup (reverse l) ↔ Nodup l :=
  pairwise_reverse.trans <| by simp only [Nodup, Ne, eq_comm]

Proof state:
α : Type u
l : List α
⊢ Pairwise (fun a b => b ≠ a) l ↔ l.Nodup

Tactic:
simp only [Nodup, Ne, eq_comm]

Result:
no goals
-- Mathlib/Analysis/Complex/Angle.lean
lemma angle_div_right_eq_angle_mul_left (a x y : ℂ) : angle x (y / a) = angle (x * a) y

Proof state:
a x y : ℂ
⊢ angle x (y / a) = angle (x * a) y

Tactic:
rw [angle_comm, angle_div_left_eq_angle_mul_right, angle_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem castSucc_eq_zero_iff {a : Fin (n + 1)} : a.castSucc = 0 ↔ a = 0

Proof state:
n : Nat
a : Fin (n + 1)
⊢ a.castSucc = 0 ↔ a = 0

Tactic:
simp [Fin.ext_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_flatten (l : Array (Array α)) :
    countP p l.flatten = (l.map (countP p)).sum

Proof state:
case of
α : Type u_1
p : α → Bool
xss✝ : List (List α)
⊢ countP p (List.map List.toArray xss✝).toArray.flatten = (map (countP p) (List.map List.toArray xss✝).toArray).sum

Tactic:
simp [List.countP_flatten, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array (Array α)
⊢ countP p l.flatten = (map (countP p) l).sum

Tactic:
cases l using array₂_induction

Result:
case of
α : Type u_1
p : α → Bool
xss✝ : List (List α)
⊢ countP p (List.map List.toArray xss✝).toArray.flatten = (map (countP p) (List.map List.toArray xss✝).toArray).sum
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma prod_add (f g : ι → α) : ∏ a, (f a + g a) = ∑ t, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a

Proof state:
ι : Type u_7
α : Type u_9
inst✝² : Fintype ι
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
⊢ ∏ a : ι, (f a + g a) = ∑ t : Finset ι, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a

Tactic:
simpa [compl_eq_univ_sdiff] using Finset.prod_add f g univ

Result:
no goals
-- Mathlib/Combinatorics/Digraph/Orientation.lean
@[simp]
lemma toSimpleGraphInclusive_top : (⊤ : Digraph V).toSimpleGraphInclusive = ⊤

Proof state:
V : Type u_1
⊢ ⊤.toSimpleGraphInclusive = ⊤

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝

Tactic:
exact ⟨And.left, fun h ↦ ⟨h.ne, Or.inl trivial⟩⟩

Result:
no goals
-- Mathlib/Data/List/Zip.lean
theorem revzip_map_fst (l : List α) : (revzip l).map Prod.fst = l

Proof state:
α : Type u
l : List α
⊢ map Prod.fst l.revzip = l

Tactic:
rw [← unzip_fst, unzip_revzip]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_rotate (l : List α) (n m : ℕ) : (l.rotate n).rotate m = l.rotate (n + m)

Proof state:
α : Type u
l : List α
n m : ℕ
⊢ (l.rotate n).rotate m = l.rotate (n + m)

Tactic:
rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem of_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.toPoly = C P.c * X + C P.d

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ P.toPoly = C P.c * X + C P.d

Tactic:
rw [of_a_eq_zero ha, hb, C_0, zero_mul, zero_add]

Result:
no goals
-- Mathlib/Data/Multiset/Basic.lean
theorem sizeOf_lt_sizeOf_of_mem [SizeOf α] {x : α} {s : Multiset α} (hx : x ∈ s) :
    SizeOf.sizeOf x < SizeOf.sizeOf s

Proof state:
α : Type u_1
inst✝ : SizeOf α
x : α
s : Multiset α
hx : x ∈ s
⊢ sizeOf x < sizeOf s

Tactic:
induction' s using Quot.inductionOn with l a b

Result:
case h
α : Type u_1
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ sizeOf x < sizeOf (Quot.mk (⇑(isSetoid α)) l)

Proof state:
case h
α : Type u_1
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ sizeOf x < sizeOf (Quot.mk (⇑(isSetoid α)) l)

Tactic:
exact List.sizeOf_lt_sizeOf_of_mem hx

Result:
no goals
-- Mathlib/ModelTheory/ElementaryMaps.lean
theorem map_fun (φ : M ↪ₑ[L] N) {n : ℕ} (f : L.Functions n) (x : Fin n → M) :
    φ (funMap f x) = funMap f (φ ∘ x)

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : funMap f (⇑φ ∘ x) = φ (funMap f x) ↔ funMap f x = funMap f x
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)

Tactic:
rw [eq_comm, h]

Result:
no goals

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)

Tactic:
have h := φ.map_formula (Formula.graph f) (Fin.cons (funMap f x) x)

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : (Formula.graph f).Realize (⇑φ ∘ Fin.cons (funMap f x) x) ↔ (Formula.graph f).Realize (Fin.cons (funMap f x) x)
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : (Formula.graph f).Realize (⇑φ ∘ Fin.cons (funMap f x) x) ↔ (Formula.graph f).Realize (Fin.cons (funMap f x) x)
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)

Tactic:
rw [Formula.realize_graph, Fin.comp_cons, Formula.realize_graph] at h

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h : funMap f (⇑φ ∘ x) = φ (funMap f x) ↔ funMap f x = funMap f x
⊢ φ (funMap f x) = funMap f (⇑φ ∘ x)
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma MemHolder.nsmul [Module ℝ Y] [BoundedSMul ℝ Y] (n : ℕ) (hf : MemHolder r f) :
    MemHolder r (n • f)

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : MetricSpace X
inst✝² : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
inst✝¹ : Module ℝ Y
inst✝ : BoundedSMul ℝ Y
n : ℕ
hf : MemHolder r f
⊢ MemHolder r (n • f)

Tactic:
simp [← Nat.cast_smul_eq_nsmul (R := ℝ), hf.smul]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sUnion_prod_const {C : Set (Set α)} {t : Set β} :
    ⋃₀ C ×ˢ t = ⋃₀ ((fun s : Set α => s ×ˢ t) '' C)

Proof state:
α : Type u_1
β : Type u_2
C : Set (Set α)
t : Set β
⊢ ⋃₀ C ×ˢ t = ⋃₀ ((fun s => s ×ˢ t) '' C)

Tactic:
simp only [sUnion_eq_biUnion, iUnion₂_prod_const, biUnion_image]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_X_pow (k n : ℕ) : coeff (X ^ k : R[X]) n = if n = k then 1 else 0

Proof state:
R : Type u
inst✝ : Semiring R
k n : ℕ
⊢ (X ^ k).coeff n = if n = k then 1 else 0

Tactic:
simp only [one_mul, RingHom.map_one, ← coeff_C_mul_X_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_sub_left_of_add_le {a b c : Int} (h : a + b ≤ c) : b ≤ c - a

Proof state:
a b c : Int
h✝ : a + b ≤ c
h : a + b + -a ≤ c + -a
⊢ b ≤ c - a

Tactic:
rwa [Int.add_comm a b, Int.add_neg_cancel_right] at h

Result:
no goals

Proof state:
a b c : Int
h : a + b ≤ c
⊢ b ≤ c - a

Tactic:
have h := Int.add_le_add_right h (-a)

Result:
a b c : Int
h✝ : a + b ≤ c
h : a + b + -a ≤ c + -a
⊢ b ≤ c - a
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem oangle_add_oangle_add_oangle_eq_pi [Module.Oriented ℝ V (Fin 2)]
    [Fact (Module.finrank ℝ V = 2)] {p₁ p₂ p₃ : P} (h21 : p₂ ≠ p₁) (h32 : p₃ ≠ p₂)
    (h13 : p₁ ≠ p₃) : ∡ p₁ p₂ p₃ + ∡ p₂ p₃ p₁ + ∡ p₃ 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
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h21 : p₂ ≠ p₁
h32 : p₃ ≠ p₂
h13 : p₁ ≠ p₃
⊢ ∡ p₁ p₂ p₃ + ∡ p₂ p₃ p₁ + ∡ p₃ p₁ p₂ = ↑π

Tactic:
simpa only [neg_vsub_eq_vsub_rev] using
  positiveOrientation.oangle_add_cyc3_neg_left (vsub_ne_zero.mpr h21) (vsub_ne_zero.mpr h32)
    (vsub_ne_zero.mpr h13)

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem symm (h : PythagoreanTriple x y z) : PythagoreanTriple y x z

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
⊢ PythagoreanTriple y x z

Tactic:
rwa [pythagoreanTriple_comm]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem SeparatedNhds.of_isCompact_isCompact [T2Space X] {s t : Set X} (hs : IsCompact s)
    (ht : IsCompact t) (hst : Disjoint s t) : SeparatedNhds s t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
hst : Disjoint s t
⊢ SeparatedNhds s t

Tactic:
simp only [SeparatedNhds, prod_subset_compl_diagonal_iff_disjoint.symm] at hst ⊢

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
hst : s ×ˢ t ⊆ (diagonal X)ᶜ
⊢ ∃ U V, IsOpen U ∧ IsOpen V ∧ s ⊆ U ∧ t ⊆ V ∧ U ×ˢ V ⊆ (diagonal X)ᶜ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
hst : s ×ˢ t ⊆ (diagonal X)ᶜ
⊢ ∃ U V, IsOpen U ∧ IsOpen V ∧ s ⊆ U ∧ t ⊆ V ∧ U ×ˢ V ⊆ (diagonal X)ᶜ

Tactic:
exact generalized_tube_lemma hs ht isClosed_diagonal.isOpen_compl hst

Result:
no goals